Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

2 files changed, 42 insertions, 28 deletions

diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v
index feb1d7e..a948e06 100644
--- a/unit-tests/Tests_lfsc_tactics.v
+++ b/unit-tests/Tests_lfsc_tactics.v
@@ -727,32 +727,51 @@ End A_BV_EUF_LIA_PR.
 
 (* Example of the webpage *)
 
-Section group.
-  Variable e : Z.
-  Variable inv : Z -> Z.
-  Variable op : Z -> Z -> Z.
-
+Section Group.
+  Variable G : Type.
+  (* We suppose that G has a decidable equality *)
+  Variable HG : CompDec G.
+  Variable op : G -> G -> G.
+  Variable inv : G -> G.
+  Variable e : G.
+
+  Local Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60).
+
+  (* We can prove automatically that we have a group if we only have the
+     "left" versions of the axioms of a group *)
   Hypothesis associative :
-    forall a b c, op a (op b c) =? op (op a b) c.
-  Hypothesis identity : forall a, (op e a =? a).
-  Hypothesis inverse : forall a, (op (inv a) a =? e).
-
-  Add_lemmas associative identity inverse.
-
+    forall a b c : G, op a (op b c) ==? op (op a b) c.
+  Hypothesis inverse :
+    forall a : G, op (inv a) a ==? e.
+  Hypothesis identity :
+    forall a : G, op e a ==? a.
+  Add_lemmas associative inverse identity.
+
+  (* The "right" version of inverse *)
   Lemma inverse' :
-    forall a : Z, (op a (inv a) =? e).
-  Proof using associative identity inverse. smt. Qed.
+    forall a : G, op a (inv a) ==? e.
+  Proof. smt. Qed.
 
+  (* The "right" version of identity *)
   Lemma identity' :
-    forall a : Z, (op a e =? a).
-  Proof using associative identity inverse. smt inverse'. Qed.
+    forall a : G, op a e ==? a.
+  Proof. smt inverse'. Qed.
 
+  (* Some other interesting facts about groups *)
   Lemma unique_identity e':
-    (forall z, op e' z =? z) -> e' =? e.
-  Proof using associative identity inverse. intros pe'; smt pe'. Qed.
+    (forall z, op e' z ==? z) -> e' ==? e.
+  Proof. intros pe'; smt pe'. Qed.
+
+  Lemma simplification_right x1 x2 y:
+      op x1 y ==? op x2 y -> x1 ==? x2.
+  Proof. intro H. smt_no_check H inverse'. Qed.
+
+  Lemma simplification_left x1 x2 y:
+      op y x1 ==? op y x2 -> x1 ==? x2.
+  Proof. intro H. smt_no_check H inverse'. Qed.
 
   Clear_lemmas.
-End group.
+End Group.
 
 
 Section EqualityOnUninterpretedType1.
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 2121ba2..83acc45 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1071,32 +1071,27 @@ End EqualityOnUninterpretedType3.
 
 
 Section AppliedPolymorphicTypes2.
-  Variable list : Type -> Type.
-  Variable append : forall A : Type, list A -> list A -> list A.
-  Arguments append {A} _ _.
-  Local Notation "l1 +++ l2" := (append l1 l2) (at level 60).
-
   Variable B : Type.
   Variable HlB : CompDec (list B).
 
   Goal forall l1 l2 l3 l4 : list B,
-      l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)).
+      l1 ++ (l2 ++ (l3 ++ l4)) = l1 ++ (l2 ++ (l3 ++ l4)).
   Proof. verit. Qed.
 
   Hypothesis append_assoc_B :
-    forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 +++ (l2 +++ l3)) ((l1 +++ l2) +++ l3) = true.
+    forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 ++ (l2 ++ l3)) ((l1 ++ l2) ++ l3) = true.
   (* TODO: make it possible to apply prop2bool to hypotheses *)
   (* Hypothesis append_assoc_B : *)
-  (*   forall l1 l2 l3 : list B, l1 +++ (l2 +++ l3) = (l1 +++ l2) +++ l3. *)
+  (*   forall l1 l2 l3 : list B, l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. *)
 
   (* The hypothesis is not used *)
   Goal forall l1 l2 l3 l4 : list B,
-      l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)).
+      l1 ++ (l2 ++ (l3 ++ l4)) = l1 ++ (l2 ++ (l3 ++ l4)).
   Proof. verit append_assoc_B. Qed.
 
   (* The hypothesis is used *)
   Goal forall l1 l2 l3 l4 : list B,
-      l1 +++ (l2 +++ (l3 +++ l4)) = ((l1 +++ l2) +++ l3) +++ l4.
+      l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
   Proof. verit append_assoc_B. Qed.
 End AppliedPolymorphicTypes2.