aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-22 11:20:12 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-22 11:20:12 +0200
commit32415df7e24d4d79a00fae95a5f619980b006c61 (patch)
tree49921e061f7ea2c118dc15b767742842530d7863
parent405355a46292aff2ba2e034cbaee56ccf245b54d (diff)
parent90dc381743087d83b2a9edc7f6666e9b1b7baa13 (diff)
Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' of the Reference Manual.
-rw-r--r--doc/sphinx/proof-engine/detailed-tactic-examples.rst643
1 files changed, 313 insertions, 330 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 84810ddba..78719c1ef 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -25,7 +25,7 @@ argument an hypothesis to generalize. It uses the JMeq datatype
defined in Coq.Logic.JMeq, hence we need to require it before. For
example, revisiting the first example of the inversion documentation:
-.. coqtop:: in
+.. coqtop:: in reset
Require Import Coq.Logic.JMeq.
@@ -63,6 +63,10 @@ to use an heterogeneous equality to relate the new hypothesis to the
old one (which just disappeared here). However, the tactic works just
as well in this case, e.g.:
+.. coqtop:: none
+
+ Abort.
+
.. coqtop:: in
Variable Q : forall (n m : nat), Le n m -> Prop.
@@ -80,7 +84,7 @@ to recover the needed equalities. Also, some subgoals should be
directly solved because of inconsistent contexts arising from the
constraints on indexes. The nice thing is that we can make a tactic
based on discriminate, injection and variants of substitution to
-automatically do such simplifications (which may involve the K axiom).
+automatically do such simplifications (which may involve the axiom K).
This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality``
does. For example, we might simplify the previous goals considerably:
@@ -101,9 +105,9 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or
simply case analysis on the generalized hypothesis. For example we can
redo what we’ve done manually with dependent destruction:
-.. coqtop:: in
+.. coqtop:: none
- Require Import Coq.Program.Equality.
+ Abort.
.. coqtop:: in
@@ -122,9 +126,9 @@ destructed hypothesis actually appeared in the goal, the tactic would
still be able to invert it, contrary to dependent inversion. Consider
the following example on vectors:
-.. coqtop:: in
+.. coqtop:: none
- Require Import Coq.Program.Equality.
+ Abort.
.. coqtop:: in
@@ -167,7 +171,7 @@ predicates on a real example. We will develop an example application
to the theory of simply-typed lambda-calculus formalized in a
dependently-typed style:
-.. coqtop:: in
+.. coqtop:: in reset
Inductive type : Type :=
| base : type
@@ -226,11 +230,15 @@ name. A term is either an application of:
Once we have this datatype we want to do proofs on it, like weakening:
-.. coqtop:: in undo
+.. coqtop:: in
Lemma weakening : forall G D tau, term (G ; D) tau ->
forall tau', term (G , tau' ; D) tau.
+.. coqtop:: none
+
+ Abort.
+
The problem here is that we can’t just use induction on the typing
derivation because it will forget about the ``G ; D`` constraint appearing
in the instance. A solution would be to rewrite the goal as:
@@ -241,6 +249,10 @@ in the instance. A solution would be to rewrite the goal as:
forall G D, (G ; D) = G' ->
forall tau', term (G, tau' ; D) tau.
+.. coqtop:: none
+
+ Abort.
+
With this proper separation of the index from the instance and the
right induction loading (putting ``G`` and ``D`` after the inducted-on
hypothesis), the proof will go through, but it is a very tedious
@@ -252,6 +264,7 @@ back automatically. Indeed we can simply write:
.. coqtop:: in
Require Import Coq.Program.Tactics.
+ Require Import Coq.Program.Equality.
.. coqtop:: in
@@ -308,17 +321,14 @@ it can be used directly.
apply weak, IHterm.
-If there is an easy first-order solution to these equations as in this
-subgoal, the ``specialize_eqs`` tactic can be used instead of giving
-explicit proof terms:
-
-.. coqtop:: all
+Now concluding this subgoal is easy.
- specialize_eqs IHterm.
+.. coqtop:: in
-This concludes our example.
+ constructor; apply IHterm; reflexivity.
-See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics.
+.. seealso::
+ The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics.
autorewrite
@@ -331,79 +341,83 @@ involves conditional rewritings and shows how to deal with them using
the optional tactic of the ``Hint Rewrite`` command.
-Example 1: Ackermann function
+.. example::
+ Ackermann function
-.. coqtop:: in
+ .. coqtop:: in reset
- Reset Initial.
+ Require Import Arith.
-.. coqtop:: in
+ .. coqtop:: in
- Require Import Arith.
+ Variable Ack : nat -> nat -> nat.
-.. coqtop:: in
+ .. coqtop:: in
- Variable Ack : nat -> nat -> nat.
+ Axiom Ack0 : forall m:nat, Ack 0 m = S m.
+ Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
+ Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
-.. coqtop:: in
+ .. coqtop:: in
- Axiom Ack0 : forall m:nat, Ack 0 m = S m.
- Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
- Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
+ Hint Rewrite Ack0 Ack1 Ack2 : base0.
-.. coqtop:: in
+ .. coqtop:: all
- Hint Rewrite Ack0 Ack1 Ack2 : base0.
+ Lemma ResAck0 : Ack 3 2 = 29.
-.. coqtop:: all
+ .. coqtop:: all
- Lemma ResAck0 : Ack 3 2 = 29.
+ autorewrite with base0 using try reflexivity.
-.. coqtop:: all
+.. example::
+ MacCarthy function
- autorewrite with base0 using try reflexivity.
+ .. coqtop:: in reset
-Example 2: Mac Carthy function
+ Require Import Omega.
-.. coqtop:: in
+ .. coqtop:: in
- Require Import Omega.
+ Variable g : nat -> nat -> nat.
-.. coqtop:: in
+ .. coqtop:: in
- Variable g : nat -> nat -> nat.
+ Axiom g0 : forall m:nat, g 0 m = m.
+ Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
+ Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
-.. coqtop:: in
+ .. coqtop:: in
- Axiom g0 : forall m:nat, g 0 m = m.
- Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
- Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
+ Hint Rewrite g0 g1 g2 using omega : base1.
+ .. coqtop:: in
-.. coqtop:: in
+ Lemma Resg0 : g 1 110 = 100.
- Hint Rewrite g0 g1 g2 using omega : base1.
+ .. coqtop:: out
-.. coqtop:: in
+ Show.
- Lemma Resg0 : g 1 110 = 100.
+ .. coqtop:: all
-.. coqtop:: out
+ autorewrite with base1 using reflexivity || simpl.
- Show.
+ .. coqtop:: none
-.. coqtop:: all
+ Qed.
- autorewrite with base1 using reflexivity || simpl.
+ .. coqtop:: all
-.. coqtop:: all
+ Lemma Resg1 : g 1 95 = 91.
- Lemma Resg1 : g 1 95 = 91.
+ .. coqtop:: all
-.. coqtop:: all
+ autorewrite with base1 using reflexivity || simpl.
- autorewrite with base1 using reflexivity || simpl.
+ .. coqtop:: none
+ Qed.
.. _quote:
@@ -419,7 +433,7 @@ the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``.
Here is an example:
-.. coqtop:: in
+.. coqtop:: in reset
Require Import Quote.
@@ -461,16 +475,11 @@ corresponding left-hand side and call yourself recursively on sub-
terms. If there is no match, we are at a leaf: return the
corresponding constructor (here ``f_const``) applied to the term.
-
-Error messages:
-
-
-#. quote: not a simple fixpoint
+.. exn:: quote: not a simple fixpoint
Happens when ``quote`` is not able to perform inversion properly.
-
Introducing variables map
~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -553,7 +562,13 @@ example, this is the case for the :tacn:`ring` tactic. Then one must provide to
is ``[O S]`` then closed natural numbers will be considered as constants
and other terms as variables.
-Example:
+.. coqtop:: in reset
+
+ Require Import Quote.
+
+.. coqtop:: in
+
+ Parameters A B C : Prop.
.. coqtop:: in
@@ -594,8 +609,9 @@ Example:
quote interp_f [ B C iff ].
-Warning: Since function inversion is undecidable in general case,
-don’t expect miracles from it!
+.. warning::
+ Since functional inversion is undecidable in the general case,
+ don’t expect miracles from it!
.. tacv:: quote @ident in @term using @tactic
@@ -607,25 +623,28 @@ don’t expect miracles from it!
Same as above, but will use the additional ``ident`` list to chose
which subterms are constants (see above).
-See also: comments of source file ``plugins/quote/quote.ml``
+.. seealso::
+ Comments from the source file ``plugins/quote/quote.ml``
-See also: the :tacn:`ring` tactic.
+.. seealso::
+ The :tacn:`ring` tactic.
-Using the tactical language
+Using the tactic language
---------------------------
About the cardinality of the set of natural numbers
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A first example which shows how to use pattern matching over the
-proof contexts is the proof that natural numbers have more than two
-elements. The proof of such a lemma can be done as follows:
+The first example which shows how to use pattern matching over the
+proof context is a proof of the fact that natural numbers have more
+than two elements. This can be done as follows:
-.. coqtop:: in
+.. coqtop:: in reset
- Lemma card_nat : ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
+ Lemma card_nat :
+ ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
Proof.
.. coqtop:: in
@@ -637,8 +656,8 @@ elements. The proof of such a lemma can be done as follows:
elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
match goal with
- | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
- cut (b = c); [ discriminate | transitivity a; auto ]
+ | _ : ?a = ?b, _ : ?a = ?c |- _ =>
+ cut (b = c); [ discriminate | transitivity a; auto ]
end.
.. coqtop:: in
@@ -651,16 +670,14 @@ solved by a match goal structure and, in particular, with only one
pattern (use of non-linear matching).
-Permutation on closed lists
+Permutations of lists
~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Another more complex example is the problem of permutation on closed
-lists. The aim is to show that a closed list is a permutation of
-another one.
-
-First, we define the permutation predicate as shown here:
+A more complex example is the problem of permutations of
+lists. The aim is to show that a list is a permutation of
+another list.
-.. coqtop:: in
+.. coqtop:: in reset
Section Sort.
@@ -670,205 +687,179 @@ First, we define the permutation predicate as shown here:
.. coqtop:: in
- Inductive permut : list A -> list A -> Prop :=
- | permut_refl : forall l, permut l l
- | permut_cons : forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
- | permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
- | permut_trans : forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
+ Inductive perm : list A -> list A -> Prop :=
+ | perm_refl : forall l, perm l l
+ | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
+ | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
+ | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
.. coqtop:: in
End Sort.
-A more complex example is the problem of permutation on closed lists.
-The aim is to show that a closed list is a permutation of another one.
First, we define the permutation predicate as shown above.
-
.. coqtop:: none
Require Import List.
-.. coqtop:: all
-
- Ltac Permut n :=
- match goal with
- | |- (permut _ ?l ?l) => apply permut_refl
- | |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
- let newn := eval compute in (length l1) in
- (apply permut_cons; Permut newn)
- | |- (permut ?A (?a :: ?l1) ?l2) =>
- match eval compute in n with
- | 1 => fail
- | _ =>
- let l1' := constr:(l1 ++ a :: nil) in
- (apply (permut_trans A (a :: l1) l1' l2);
- [ apply permut_append | compute; Permut (pred n) ])
- end
- end.
-
-
-.. coqtop:: all
-
- Ltac PermutProve :=
- match goal with
- | |- (permut _ ?l1 ?l2) =>
- match eval compute in (length l1 = length l2) with
- | (?n = ?n) => Permut n
- end
- end.
-
-Next, we can write naturally the tactic and the result can be seen
-above. We can notice that we use two top level definitions
-``PermutProve`` and ``Permut``. The function to be called is
-``PermutProve`` which computes the lengths of the two lists and calls
-``Permut`` with the length if the two lists have the same
-length. ``Permut`` works as expected. If the two lists are equal, it
-concludes. Otherwise, if the lists have identical first elements, it
-applies ``Permut`` on the tail of the lists. Finally, if the lists
-have different first elements, it puts the first element of one of the
-lists (here the second one which appears in the permut predicate) at
-the end if that is possible, i.e., if the new first element has been
-at this place previously. To verify that all rotations have been done
-for a list, we use the length of the list as an argument for Permut
-and this length is decremented for each rotation down to, but not
-including, 1 because for a list of length ``n``, we can make exactly
-``n−1`` rotations to generate at most ``n`` distinct lists. Here, it
-must be noticed that we use the natural numbers of Coq for the
-rotation counter. In :ref:`ltac-syntax`, we can
-see that it is possible to use usual natural numbers but they are only
-used as arguments for primitive tactics and they cannot be handled, in
-particular, we cannot make computations with them. So, a natural
-choice is to use Coq data structures so that Coq makes the
-computations (reductions) by eval compute in and we can get the terms
-back by match.
-
-With ``PermutProve``, we can now prove lemmas as follows:
-
.. coqtop:: in
- Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+ Ltac perm_aux n :=
+ match goal with
+ | |- (perm _ ?l ?l) => apply perm_refl
+ | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
+ let newn := eval compute in (length l1) in
+ (apply perm_cons; perm_aux newn)
+ | |- (perm ?A (?a :: ?l1) ?l2) =>
+ match eval compute in n with
+ | 1 => fail
+ | _ =>
+ let l1' := constr:(l1 ++ a :: nil) in
+ (apply (perm_trans A (a :: l1) l1' l2);
+ [ apply perm_append | compute; perm_aux (pred n) ])
+ end
+ end.
-.. coqtop:: in
+Next we define an auxiliary tactic ``perm_aux`` which takes an argument
+used to control the recursion depth. This tactic behaves as follows. If
+the lists are identical (i.e. convertible), it concludes. Otherwise, if
+the lists have identical heads, it proceeds to look at their tails.
+Finally, if the lists have different heads, it rotates the first list by
+putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the
+number of performed rotations using the argument ``n``. We do this by
+decrementing ``n`` each time we perform a rotation. It works because
+for a list of length ``n`` we can make exactly ``n - 1`` rotations
+to generate at most ``n`` distinct lists. Notice that we use the natural
+numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know
+that it is possible to use the usual natural numbers, but they are only
+used as arguments for primitive tactics and they cannot be handled, so,
+in particular, we cannot make computations with them. Thus the natural
+choice is to use Coq data structures so that Coq makes the computations
+(reductions) by ``eval compute in`` and we can get the terms back by match.
+
+.. coqtop:: in
+
+ Ltac solve_perm :=
+ match goal with
+ | |- (perm _ ?l1 ?l2) =>
+ match eval compute in (length l1 = length l2) with
+ | (?n = ?n) => perm_aux n
+ end
+ end.
- Proof. PermutProve. Qed.
+The main tactic is ``solve_perm``. It computes the lengths of the two lists
+and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they
+aren't, the lists cannot be permutations of each other). Using this tactic we
+can now prove lemmas as follows:
.. coqtop:: in
- Lemma permut_ex2 : permut nat
- (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
- (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
-
- Proof. PermutProve. Qed.
+ Lemma solve_perm_ex1 :
+ perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+ Proof. solve_perm. Qed.
+.. coqtop:: in
+ Lemma solve_perm_ex2 :
+ perm nat
+ (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+ (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+ Proof. solve_perm. Qed.
Deciding intuitionistic propositional logic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. _decidingintuitionistic1:
-
-.. coqtop:: all
-
- Ltac Axioms :=
- match goal with
- | |- True => trivial
- | _:False |- _ => elimtype False; assumption
- | _:?A |- ?A => auto
- end.
-
-.. _decidingintuitionistic2:
-
-.. coqtop:: all
-
- Ltac DSimplif :=
- repeat
- (intros;
- match goal with
- | id:(~ _) |- _ => red in id
- | id:(_ /\ _) |- _ =>
- elim id; do 2 intro; clear id
- | id:(_ \/ _) |- _ =>
- elim id; intro; clear id
- | id:(?A /\ ?B -> ?C) |- _ =>
- cut (A -> B -> C);
- [ intro | intros; apply id; split; assumption ]
- | id:(?A \/ ?B -> ?C) |- _ =>
- cut (B -> C);
- [ cut (A -> C);
- [ intros; clear id
- | intro; apply id; left; assumption ]
- | intro; apply id; right; assumption ]
- | id0:(?A -> ?B),id1:?A |- _ =>
- cut B; [ intro; clear id0 | apply id0; assumption ]
- | |- (_ /\ _) => split
- | |- (~ _) => red
- end).
-
-.. coqtop:: all
-
- Ltac TautoProp :=
- DSimplif;
- Axioms ||
- match goal with
- | id:((?A -> ?B) -> ?C) |- _ =>
- cut (B -> C);
- [ intro; cut (A -> B);
- [ intro; cut C;
- [ intro; clear id | apply id; assumption ]
- | clear id ]
- | intro; apply id; intro; assumption ]; TautoProp
- | id:(~ ?A -> ?B) |- _ =>
- cut (False -> B);
- [ intro; cut (A -> False);
- [ intro; cut B;
- [ intro; clear id | apply id; assumption ]
- | clear id ]
- | intro; apply id; red; intro; assumption ]; TautoProp
- | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
- end.
-
-The pattern matching on goals allows a complete and so a powerful
-backtracking when returning tactic values. An interesting application
-is the problem of deciding intuitionistic propositional logic.
-Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:cite:`Dyc92`, it is quite natural to code such a tactic
-using the tactic language as shown on figures: :ref:`Deciding
-intuitionistic propositions (1) <decidingintuitionistic1>` and
-:ref:`Deciding intuitionistic propositions (2)
-<decidingintuitionistic2>`. The tactic ``Axioms`` tries to conclude
-using usual axioms. The tactic ``DSimplif`` applies all the reversible
-rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the
-main tactic to be called) simplifies with ``DSimplif``, tries to
-conclude with ``Axioms`` and tries several paths using the
-backtracking rules (one of the four Dyckhoff’s rules for the left
-implication to get rid of the contraction and the right or).
-
-For example, with ``TautoProp``, we can prove tautologies like those:
-
-.. coqtop:: in
-
- Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
+Pattern matching on goals allows a powerful backtracking when returning tactic
+values. An interesting application is the problem of deciding intuitionistic
+propositional logic. Considering the contraction-free sequent calculi LJT* of
+Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
+tactic language as shown below.
-.. coqtop:: in
-
- Proof. TautoProp. Qed.
-
-.. coqtop:: in
+.. coqtop:: in reset
- Lemma tauto_ex2 :
- forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+ Ltac basic :=
+ match goal with
+ | |- True => trivial
+ | _ : False |- _ => contradiction
+ | _ : ?A |- ?A => assumption
+ end.
.. coqtop:: in
- Proof. TautoProp. Qed.
+ Ltac simplify :=
+ repeat (intros;
+ match goal with
+ | H : ~ _ |- _ => red in H
+ | H : _ /\ _ |- _ =>
+ elim H; do 2 intro; clear H
+ | H : _ \/ _ |- _ =>
+ elim H; intro; clear H
+ | H : ?A /\ ?B -> ?C |- _ =>
+ cut (A -> B -> C);
+ [ intro | intros; apply H; split; assumption ]
+ | H: ?A \/ ?B -> ?C |- _ =>
+ cut (B -> C);
+ [ cut (A -> C);
+ [ intros; clear H
+ | intro; apply H; left; assumption ]
+ | intro; apply H; right; assumption ]
+ | H0 : ?A -> ?B, H1 : ?A |- _ =>
+ cut B; [ intro; clear H0 | apply H0; assumption ]
+ | |- _ /\ _ => split
+ | |- ~ _ => red
+ end).
+
+.. coqtop:: in
+
+ Ltac my_tauto :=
+ simplify; basic ||
+ match goal with
+ | H : (?A -> ?B) -> ?C |- _ =>
+ cut (B -> C);
+ [ intro; cut (A -> B);
+ [ intro; cut C;
+ [ intro; clear H | apply H; assumption ]
+ | clear H ]
+ | intro; apply H; intro; assumption ]; my_tauto
+ | H : ~ ?A -> ?B |- _ =>
+ cut (False -> B);
+ [ intro; cut (A -> False);
+ [ intro; cut B;
+ [ intro; clear H | apply H; assumption ]
+ | clear H ]
+ | intro; apply H; red; intro; assumption ]; my_tauto
+ | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
+ end.
+
+The tactic ``basic`` tries to reason using simple rules involving truth, falsity
+and available assumptions. The tactic ``simplify`` applies all the reversible
+rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
+tactic to be called) simplifies with ``simplify``, tries to conclude with
+``basic`` and tries several paths using the backtracking rules (one of the
+four Dyckhoff’s rules for the left implication to get rid of the contraction
+and the right ``or``).
+
+Having defined ``my_tauto``, we can prove tautologies like these:
+
+.. coqtop:: in
+
+ Lemma my_tauto_ex1 :
+ forall A B : Prop, A /\ B -> A \/ B.
+ Proof. my_tauto. Qed.
+
+.. coqtop:: in
+
+ Lemma my_tauto_ex2 :
+ forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+ Proof. my_tauto. Qed.
Deciding type isomorphisms
~~~~~~~~~~~~~~~~~~~~~~~~~~
-A more tricky problem is to decide equalities between types and modulo
+A more tricky problem is to decide equalities between types modulo
isomorphisms. Here, we choose to use the isomorphisms of the simply
typed λ-calculus with Cartesian product and unit type (see, for
example, :cite:`RC95`). The axioms of this λ-calculus are given below.
@@ -915,112 +906,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below.
End Iso_axioms.
+.. coqtop:: in
+ Ltac simplify_type ty :=
+ match ty with
+ | ?A * ?B * ?C =>
+ rewrite <- (Ass A B C); try simplify_type_eq
+ | ?A * ?B -> ?C =>
+ rewrite (Cur A B C); try simplify_type_eq
+ | ?A -> ?B * ?C =>
+ rewrite (Dis A B C); try simplify_type_eq
+ | ?A * unit =>
+ rewrite (P_unit A); try simplify_type_eq
+ | unit * ?B =>
+ rewrite (Com unit B); try simplify_type_eq
+ | ?A -> unit =>
+ rewrite (AR_unit A); try simplify_type_eq
+ | unit -> ?B =>
+ rewrite (AL_unit B); try simplify_type_eq
+ | ?A * ?B =>
+ (simplify_type A; try simplify_type_eq) ||
+ (simplify_type B; try simplify_type_eq)
+ | ?A -> ?B =>
+ (simplify_type A; try simplify_type_eq) ||
+ (simplify_type B; try simplify_type_eq)
+ end
+ with simplify_type_eq :=
+ match goal with
+ | |- ?A = ?B => try simplify_type A; try simplify_type B
+ end.
-.. _typeisomorphism1:
-
-.. coqtop:: all
-
- Ltac DSimplif trm :=
- match trm with
- | (?A * ?B * ?C) =>
- rewrite <- (Ass A B C); try MainSimplif
- | (?A * ?B -> ?C) =>
- rewrite (Cur A B C); try MainSimplif
- | (?A -> ?B * ?C) =>
- rewrite (Dis A B C); try MainSimplif
- | (?A * unit) =>
- rewrite (P_unit A); try MainSimplif
- | (unit * ?B) =>
- rewrite (Com unit B); try MainSimplif
- | (?A -> unit) =>
- rewrite (AR_unit A); try MainSimplif
- | (unit -> ?B) =>
- rewrite (AL_unit B); try MainSimplif
- | (?A * ?B) =>
- (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
- | (?A -> ?B) =>
- (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
- end
- with MainSimplif :=
- match goal with
- | |- (?A = ?B) => try DSimplif A; try DSimplif B
- end.
-
-.. coqtop:: all
+.. coqtop:: in
- Ltac Length trm :=
- match trm with
- | (_ * ?B) => let succ := Length B in constr:(S succ)
- | _ => constr:(1)
- end.
+ Ltac len trm :=
+ match trm with
+ | _ * ?B => let succ := len B in constr:(S succ)
+ | _ => constr:(1)
+ end.
-.. coqtop:: all
+.. coqtop:: in
Ltac assoc := repeat rewrite <- Ass.
+.. coqtop:: in
-.. _typeisomorphism2:
-
-.. coqtop:: all
-
- Ltac DoCompare n :=
- match goal with
- | [ |- (?A = ?A) ] => reflexivity
- | [ |- (?A * ?B = ?A * ?C) ] =>
- apply Cons; let newn := Length B in
- DoCompare newn
- | [ |- (?A * ?B = ?C) ] =>
- match eval compute in n with
- | 1 => fail
- | _ =>
- pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
- end
- end.
-
-.. coqtop:: all
+ Ltac solve_type_eq n :=
+ match goal with
+ | |- ?A = ?A => reflexivity
+ | |- ?A * ?B = ?A * ?C =>
+ apply Cons; let newn := len B in solve_type_eq newn
+ | |- ?A * ?B = ?C =>
+ match eval compute in n with
+ | 1 => fail
+ | _ =>
+ pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n)
+ end
+ end.
- Ltac CompareStruct :=
- match goal with
- | [ |- (?A = ?B) ] =>
- let l1 := Length A
- with l2 := Length B in
- match eval compute in (l1 = l2) with
- | (?n = ?n) => DoCompare n
- end
- end.
+.. coqtop:: in
-.. coqtop:: all
+ Ltac compare_structure :=
+ match goal with
+ | |- ?A = ?B =>
+ let l1 := len A
+ with l2 := len B in
+ match eval compute in (l1 = l2) with
+ | ?n = ?n => solve_type_eq n
+ end
+ end.
- Ltac IsoProve := MainSimplif; CompareStruct.
+.. coqtop:: in
+ Ltac solve_iso := simplify_type_eq; compare_structure.
-The tactic to judge equalities modulo this axiomatization can be
-written as shown on these figures: :ref:`type isomorphism tactic (1)
-<typeisomorphism1>` and :ref:`type isomorphism tactic (2)
-<typeisomorphism2>`. The algorithm is quite simple. Types are reduced
-using axioms that can be oriented (this done by ``MainSimplif``). The
-normal forms are sequences of Cartesian products without Cartesian
-product in the left component. These normal forms are then compared
-modulo permutation of the components (this is done by
-``CompareStruct``). The main tactic to be called and realizing this
-algorithm isIsoProve.
+The tactic to judge equalities modulo this axiomatization is shown above.
+The algorithm is quite simple. First types are simplified using axioms that
+can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
+The normal forms are sequences of Cartesian products without Cartesian product
+in the left component. These normal forms are then compared modulo permutation
+of the components by the tactic ``compare_structure``. If they have the same
+lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
+The main tactic that puts all these components together is called ``solve_iso``.
-Here are examples of what can be solved by ``IsoProve``.
+Here are examples of what can be solved by ``solve_iso``.
.. coqtop:: in
- Lemma isos_ex1 :
- forall A B:Set, A * unit * B = B * (unit * A).
+ Lemma solve_iso_ex1 :
+ forall A B : Set, A * unit * B = B * (unit * A).
Proof.
- intros; IsoProve.
+ intros; solve_iso.
Qed.
.. coqtop:: in
- Lemma isos_ex2 :
- forall A B C:Set,
- (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+ Lemma solve_iso_ex2 :
+ forall A B C : Set,
+ (A * unit -> B * (C * unit)) =
+ (A * unit -> (C -> unit) * C) * (unit -> A -> B).
Proof.
- intros; IsoProve.
+ intros; solve_iso.
Qed.