diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 92 |
4 files changed, 82 insertions, 49 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index d77690458d..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -295,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 437b8e557e..933f07674a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1924,9 +1924,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1961,7 +1962,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. @@ -1978,11 +1979,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ec97377128..0bcca0fe56 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2762,14 +2762,14 @@ typeclass inference. Goal True. -+ .. coqtop:: in undo + .. coqdoc:: have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ .. coqdoc:: + .. coqdoc:: have foo : ty := . @@ -2778,13 +2778,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. -+ .. coqtop:: in undo + .. coqdoc:: have foo : ty := t. No inference for ``ty`` and ``t``. -+ .. coqtop:: in undo + .. coqdoc:: have foo := t. @@ -4586,13 +4586,18 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all undo + .. coqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all undo + .. coqtop:: none + + Abort. + Lemma test a : P (a || a) -> True. + + .. coqtop:: all move/P2Q=> HQa. @@ -4890,11 +4895,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all undo + .. coqtop:: all case: (@andE b1 b2). - .. coqtop:: all undo + .. coqtop:: none + + Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). + + .. coqtop:: all case: (@andP b1 b2). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e280ab0f34..6f57cc53a9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -755,33 +755,49 @@ Applying theorems A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all undo + .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: in apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: in apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: all apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: all undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: all apply Rtrans with (2 := Rmp). @@ -789,6 +805,10 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. + .. coqtop:: none + + Abort. Goal R n p. + .. coqtop:: all eapply Rtrans. @@ -2332,6 +2352,7 @@ and an explanation of the underlying technique. where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident + :name: inversion_clear This behaves as :n:`inversion` and then erases :n:`@ident` from the context. @@ -2490,47 +2511,54 @@ and an explanation of the underlying technique. *Non-dependent inversion*. - Let us consider the relation Le over natural numbers and the following - variables: + Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: all reset + .. coqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Let us consider the following goal: .. coqtop:: none + Section Section. + Variable P : nat -> nat -> Prop. + Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. intros. - .. coqtop:: all + .. coqtop:: out Show. - To prove the goal, we may need to reason by cases on H and to derive - that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to proving that the - only possible constructor of (Le (S n) m) isLeS and that we can invert - the-> in the type of LeS. This inversion is possible because Le is the - smallest set closed by the constructors LeO and LeS. + To prove the goal, we may need to reason by cases on :g:`H` and to derive + that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that + :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only + possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert + the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` + is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: undo all + .. coqtop:: all inversion_clear H. - Note that m has been substituted in the goal for (S m0) and that the - hypothesis (Le n m0) has been added to the context. + Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the + hypothesis :g:`(Le n m0)` has been added to the context. - Sometimes it is interesting to have the equality m=(S m0) in the - context to use it after. In that case we can use inversion that does + Sometimes it is interesting to have the equality :g:`m = (S m0)` in the + context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: undo all + .. coqtop:: none + + Abort. + Goal forall n m, Le (S n) m -> P n m. + intros. + + .. coqtop:: all inversion H. @@ -2540,31 +2568,27 @@ and an explanation of the underlying technique. Let us consider the following goal: - .. coqtop:: reset none + .. coqtop:: none - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. intros. - .. coqtop:: all + .. coqtop:: out Show. - As H occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute H by + As :g:`H` occurs in the goal, we may want to reason by cases on its + structure and so, we would like inversion tactics to substitute :g:`H` by the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :n:`inversion_clear` do such a substitution. To have such a behavior we + :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all dependent inversion_clear H. - Note that H has been substituted by (LeS n m0 l) andm by (S m0). + Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. .. example:: |