Module mathcomp.classical.contra

# Contraposition This file provides tactics to reason by contraposition and contradiction. ## Tactics ``` assume_not == add a goal negation assumption. The tactic also works for goals in Type, simplifies the added assumption, and exposes its top-level constructive content. absurd_not == proof by contradiction. Same as assume_not, but the goal is erased and replaced by False. Caveat: absurd_not cannot be used as a move/ view because its conclusion is indeterminate. The more general notP can be used instead. contra == proof by contraposition. Change a goal of the form assumption -> conclusion to ~ conclusion -> ~ assumption. As with assume_not, contra allows both assumption and conclusion to be in Type, simplifies the negation of both assumption and conclusion, and exposes the constructive contents of the negated conclusion. The contra tactic also supports a limited form of the ':' discharge pseudo tactical, whereby contra: <d-items> means move: <d-items>; contra. The only <d-items> allowed are one term, possibly preceded by a clear switch. absurd == proof by contradiction. The defective form of the tactic simply replaces the entire goal with False (just as the Ltac exfalso), leaving the user to derive a contradiction from the assumptions. The ':' form absurd: <d-items> replaces the goal with the negation of the (single) <d-item> (as with contra:, a clear switch is also allowed. Finally the Ltac absurd term form is also supported. ```

A wrapper for view lemmas with an indeterminate conclusion (of the form forall ... T ..., pattern -> T), and for which the intended view pattern may fail to match some assumptions. This wrapper ensures that such views are only used in the forward direction (as in move/), and only with the appropriate move_viewP hint, preventing its application to an arbitrary assumption A by the instatiation to A -> T' of its indeterminate conclusion T. This is similar to the implies wrapper, except move_viewP is *NOT* declared as a coercion---it must be used explicitly to apply the view manually to an assumption (as in, move_viewP my_view some_assumption).

## Type-level equivalence

A generic Forall "constructor" for the Gallina forall quantifier, i.e., ``` \Forall x, P := Forall (fun x => P) := forall x, P. ``` The main use of Forall is to apply congruence to a forall equality: ``` congr1 Forall : forall P Q, P = Q -> Forall P = Forall Q. ``` in particular in a classical setting with function extensionality, where we can have (forall x, P x = Q x) -> (forall x, P x) = (forall x, Q x). We use a forallSort structure to factor the ad hoc PTS product formation rules; forallSort is keyed on the type of the entire forall expression, or (up to subsumption) the type of the forall body---this is always a sort. This implementation has two important limitations: 1. It cannot handle the SProp sort and its typing rules. However, its main application is extensionality, which is not compatible with SProp because an (A : SProp) -> B "function" is not a generic (A : Type) -> B function as SProp is not included in Type. 2. The Forall constructor can't be inserted by a straightforward unfold (as in, rewrite -[forall x, _]/(Forall _)) because of the way Coq unification handles Type constraints. The ForallI tactic mitigates this issue, but there are additional issues with its implementation---see below.

We define specialized copies of the wrapped structure of ssrfun for Prop and Type, as we need more than two alternative rules (indeed, 3 for Prop and 4 for Type). We need separate copies for Prop and Type as universe polymorphism cannot instantiate Type with Prop.

A set of tools (tactics, views, and rewrite rules) to facilitate the handling of classical negation. The core functionality of these tools is implemented by three sets of canonical structures that provide for the simplification of negation statements (e.g., using de Morgan laws), the conversion from constructive statements in Type to purely logical ones in Prop (equivalently, expansion rules for the statement inhabited T), and conversely extraction of constructive contents from logical statements. Except for bool predicates and operators, all definitions are treated transparently when matching statements for either simplification or conversion; this is achieved by using the wrapper telescope pattern, first delegating the matching of specific logical connectives, predicates, or type constructors to an auxiliary structure that *FAILS* to match unknown operators, thus triggers the expansion of defined constants. If this ultimately fails then the wrapper is expanded, and the primary structure instance for the expanded wrapper provides an alternative default rule: not simplifying ~ P, not expanding inhabited T, or not extracting any contents from a proposition P, respectively. Additional rules, for intermediate wrapper instances, are used to handle forall statements (for which canonical instances are not yet supported), as well as addiitonal simplifications, such as inhabited P = P :> Prop. Finally various tertiary structures are used to match deeper patterns, such as bounded forall statements of the form forall x, P x -> Q x, or inequalites x != y (i.e., is_true (~~ (x == y))). As mentioned above, tertiary rules for bool subexpressions do not try to expand definitions, as this would lead to the undesirable expansion of some standard definitions. This is simply achieved by *NOT* using the wrapper telescope pattern, and just having a default instance alongside those for specific predicates and connectives.

The negatedProp structure provides simplification of the Prop negation (~ _) for standard connectives and predicates. The instances below cover the pervasive and ssrbool Prop connectives, decidable equality, as well as bool propositions (i.e., the is_true predicate), together with a few bool connectives and predicates: negation ~~, equality ==, and nat <= and <. Others can be added (e.g., Order.le/lt) by declaring appropriate instances of bool_negation and bool_affirmation, while other Prop connectives and predicates can be added by declaring instances of proper_negatedProp.

The implementation follows the wrapper telescope pattern outlined above: negatedProp instances match on the wrappedProp wrapper to try three generic matching rules, in succession: - Rule 1: match a specific connective or predicate with an instance of the properNegatedProp secondary structure, expanding definitions if needed, but failing if no proper match is found. - Rule 2: match a forall statement (including (T : Type) -> P statements). - Rule 3: match any Prop but return the trivial simplification. The simplified proposition is returned as a projection parameter nP rather than a Structure member, so that applying the corresponding views or rewrite rules doesn't expose the inferred structures; properNegatedProp does similarly. Also, negatedProp similarly returns a 'trivial' bool flag that is set when Rule 3 is used, but this is actually used in the reverse direction: views notP and rewrite rule notE force trivial := false, thus excluding trivial instances.

User views and rewrite rules. The plain versions (notP, notE and notI) do not match trivial instances; lax_XXX versions allow them. In addition, the negation introduction rewrite rule notI does not match forall or -> statements---lax_notI must be used for these.

The andRHS tertiary structure used to simplify (~ (P -> False)) to P, both here for the imply_nProp instance and for bounded_forall_nProp below. Because the andRHS instances match the Prop RETURNED by negatedProp they do not need to expand definitions, hence do not need to use the wrapper telescope pattern.

Rule 2: forall negation, including (T : Type) -> P statements. We use tertiary structures to recognize bounded foralls and simplify, e.g., ~ forall x, P -> Q to exists2 x, P & ~ Q, or even exists x, P when Q := False (as above for imply). As forall_body_nProp and forall_body_proper_nProp are telescopes over negatedProp and properNegatedProp, respectively, their instances match instances declared above without the need to expand definitions, hence do not need to use the wrapper telescope idiom.

The explicit argument to fun_if is a workaround for a bug in the Coq unification code that prevents default instances from ever matching match constructs. Furthermore rewriting with ifE would not work here, because the if_expr definition would be expanded by the eta expansion needed to match the exists_nProp rule.

The properNegatedProp instance that handles boolean statements. We use two tertiary structures to handle positive and negative boolean statements so that the contra tactic below will mostly subsume the collection of contraXX lemmas in ssrbool and eqtype. We only match manifest ~~ connectives, the true and false constants, and the ==, <=%N, and <%N predicates. In particular we do not use de Morgan laws to push boolean negation into connectives, as we did above for Prop connectives. It will be up to the user to use rewriting to put the negated statement in its desired shape.

We use a tertiary structure to handle the negation of nat comparisons, and simplify ~ m <= n to n < m, and ~ m < n to n <= m. As m < n is merely notation for m.+1 <= n, we need to dispatch on the left hand side of the comparison to perform the latter simplification.

We use two tertiary structures to simplify negation of boolean constant and decidable equalities, simplifying b <> true to ~~ b, b <> false to b, x <> y to x != y, and ~ x != y to x = y. We do need to use the wrapper telescope pattern here, as we want to simplify instances of x <> y when y evaluates to true or false. Since we only need two rules (true/false RHS or generic eqType RHS) we can use the generic wrapped type from ssrfun. The actual matching of the true and false RHS is delegated to a fourth level bool_eq_negation_rhs structure. Finally observe that the ~ x != y to x = y simplification can be handled by a bool_affirmation instance.

The witnessedType structure provides conversion between Type and Prop in goals; the conversion is mostly used in the Type-to-Prop direction, e.g., as a preprocessing step preceding proof by contradiction (see absurd_not below), but the Prop-to-Type direction is required for contraposition. Thus witnessedType associates to a type T a "witness" proposition P equivalent to the existence of an x of type T. As in a `{classical_logic} context inhabited T is such a proposition, witnessedType can be understood as providing simplification for inhabited T, much like negatedProp provides simplification for ~ P for standard connectives and predicates.

Similarly to negatedProp, witnessedType returns the witness proposition via a projection argument P, but does not need to signal "trivial" instances as the default value for P is nontrivial (namely, inhabited T), while the "trivial" case where P = T is actually desireable and handled by an extra top-priority rule.

The witnessProp structure provides for conversion of some Prop assumptions to Type values with some constructive contents, e.g., convert a P \/ Q assumption to a {P} + {Q} sumbool value. This is not the same as the forward direction of witnessedType, because instances here match the Prop statement: witness_Prop find a T such that P -> T while witnessedType finds a P such that P -> T (and T -> P for the converse direction).

The implementation follows the wrapper telescope pattern similarly to negatedProp, with three rules, one for Prop constructors with proper constructive contents, one for forall propositions (also with proper constructive contents) and one default rule that just returns P : Prop as is (thus, with no other contents except the provability of P). The witnessProp structure also uses projection parameters to return the inferred Type T together with a bool 'trivial' flag that is set when the trivial rule is used. Here, however, this flag is used in both directions: the 'witness' view forces it to false to prevent trivial instances, but the flag is also used to fine tune the choice of T, selecting between sum, sumor, and sumbool, between sig and sigT, and sig2 and sigT2. This relies on the fact that the tactic engine will eagerly iota reduce the returned type, so that the user will never see the conditionals specified in the proper_witness_Prop instances. However, it would not be possible to construct the specialised types for trivial witnesses (e.g., {P} + {Q}) using the types returned by witnessProp instances, since thes are in Type, and the information that they are actully in Prop has been lost. This is solved by returning an additional Prop P0 that is a copy of the matched Prop P when trivial = true. (We put P0 = True when trivial = false, as we only need to ensure P -> P0.) Caveat: although P0 should in principle be the last parameter of witness_Prop, and we use this order for the wProp and wPred projector local notation, it is important to put P0 _BEFORE_ T, to circumvent an incompleteness in Coq's implementation of higher-order pattern unification that would cause the trivial rule to fail for the body of an exists. In such a case the rule needs to unify (1) ?P0 x ~ ?P and (2) ?T x ~ ?P for some type A some x : A in the context of ?P, but not ?P0 nor ?T. This succeeds easily if (1) is performed before (2), setting ?P := ?P0 x and ?T := ?P0, but if (2) is attempted first Coq tries to perform ?P := ?T x, which fails Type/Prop universe constraints, and then fails outright, instead of using pattern unification to solve (2) as ?P := ?Q x, ?T := ?Q for a fresh ?Q : A -> Prop.

Conjunctions P /\ Q are a little delicate to handle, as we should not produce a proper instance (and thus fail) if neither P nor Q is proper. We use a tertiary structure for this : nand_bool b, which has instances only for booleans b0 such that ~~ (b0 && b). We allow the witness_Prop instance for P to return an arbitrary 'trivial' flag s, but then force the 'trivial' flag for Q to be an instance of nand_bool s.