Repair proofs for latest version of CoqHammer

AExp.v

@@ -34,7 +34,7 @@ Fixpoint asimp_const (e : aexpr) :=
 
 Lemma lem_aval_asimp_const : forall s e, aval s (asimp_const e) = aval s e.
 Proof.
-  induction e; sauto.
+  induction e; hauto q: on.
 Qed.
 
 Fixpoint plus (e1 e2 : aexpr) :=
@@ -58,8 +58,5 @@ Fixpoint asimp (e : aexpr) :=
 
 Lemma lem_aval_asimp : forall s e, aval s (asimp e) = aval s e.
 Proof.
-  induction e; sauto.
-  Reconstr.htrivial Reconstr.AllHyps
-                    (@lem_aval_plus)
-                    Reconstr.Empty.
+  induction e; hauto use: lem_aval_plus.
 Qed.

ASM.v

@@ -41,7 +41,5 @@ Fixpoint comp (a : aexpr) : list instr :=
 
 Lemma lem_exec_comp : forall a s stk, exec (comp a) s stk = aval s a :: stk.
 Proof.
-  induction a; sauto.
-  (* CoqHammer 1.0.7 can't solve the subgoal *)
-  repeat rewrite lem_exec_append; scrush.
+  induction a; hauto q: on use: lem_exec_append.
 Qed.

BExp.v

@@ -55,22 +55,15 @@ Qed.
 
 Lemma lem_bval_and : forall s e1 e2, bval s (and e1 e2) = bval s e1 && bval s e2.
 Proof.
-  induction e1; sauto.
+  induction e1; hauto lqb: on.
 Qed.
 
 Lemma lem_bval_less : forall s a1 a2, bval s (less a1 a2) = (aval s a1 <? aval s a2).
 Proof.
-  induction a1; sauto.
+  induction a1; sauto lq: on rew: off.
 Qed.
 
 Lemma lem_bval_bsimp : forall s e, bval s (bsimp e) = bval s e.
 Proof.
-  induction e; sauto.
-  Reconstr.htrivial Reconstr.AllHyps
-                    (@lem_bval_not)
-                    Reconstr.Empty.
-  Reconstr.htrivial Reconstr.AllHyps
-                    (@lem_bval_and)
-                    Reconstr.Empty.
-  scrush.
+  induction e; sauto lq: on use: lem_bval_not, lem_bval_and.
 Qed.

Big_Step.v

@@ -51,11 +51,10 @@ Qed.
 
 Lemma lem_triv_if : forall b c, If b c c ~~ c.
 Proof.
-  unfold equiv_com; sauto.
-  - scrush.
-  - destruct (bval s b) eqn:?.
-    + eauto using IfTrue.
-    + eauto using IfFalse.
+  unfold equiv_com; try sauto.
+  - intros. destruct (bval s b) eqn:?.
+    + sauto lq: on rew: off.
+    + sauto lq: on rew: off.
 Qed.
 
 
@@ -76,13 +75,9 @@ Proof.
   assert (forall p s', p ==> s' -> forall b c c' s,
               p = (While b c, s) -> c ~~ c' -> (While b c', s) ==> s'); [idtac | scrush].
   intros p s' H.
-  induction H; sauto.
-  - Reconstr.hobvious Reconstr.AllHyps
-		      (@WhileFalse)
-		      Reconstr.Empty.
-  - Reconstr.hsimple (@IHbig_step2, @H0, @H3, @H)
-		(@WhileTrue)
-		(@equiv_com).
+  induction H; try scongruence.
+  - sauto lq: on.
+  - hauto lq: on use: WhileTrue unfold: equiv_com.
 Qed.
 
 Lemma lem_while_cong : forall b c c', c ~~ c' -> While b c ~~ While b c'.
@@ -112,7 +107,5 @@ Lemma lem_big_step_deterministic :
 Proof.
   intros c s s1 s2 H.
   revert s2.
-  induction H; try yelles 1.
-  - scrush.
-  - intros s0 H2; inversion H2; scrush.
+  induction H; try sauto.
 Qed.

Compiler.v

@@ -54,14 +54,10 @@ Qed.
 Lemma lem_n_succ_znth :
   forall {A} n (a : A) xs x, 0 <= n -> znth (n + 1) (a :: xs) x = znth n xs x.
 Proof.
-  induction n; sauto.
-  - Reconstr.htrivial Reconstr.AllHyps
-                      (@Coq.PArith.Pnat.Pos2Nat.inj_succ, @Coq.PArith.BinPos.Pos.add_1_r)
-                      Reconstr.Empty.
-  - Reconstr.htrivial Reconstr.AllHyps
-                      (@Coq.PArith.BinPos.Pos.add_1_r, @Coq.PArith.Pnat.Pos2Nat.inj_succ,
-                       @Coq.ZArith.Znat.Z2Nat.inj_pos, @Coq.Init.Peano.eq_add_S)
-                      (@znth).
+  induction n.
+  - hauto lq:on.
+  - hauto lq: on use: list, Pnat.Pos2Nat.inj_succ, PArith.BinPos.Pos.add_1_r unfold: znth.
+  - sfirstorder.
 Qed.
 
 Lemma lem_znth_app :
@@ -90,13 +86,10 @@ Lemma lem_size_succ :
   forall a xs, size (a :: xs) = size xs + 1.
 Proof.
   assert (forall n a xs, n = size xs -> size (a :: xs) = n + 1); [idtac | scrush].
-  induction n; sauto.
-  - scrush.
-  - Reconstr.htrivial Reconstr.AllHyps
-                      (@Coq.PArith.BinPos.Pplus_one_succ_r, @Coq.ZArith.Znat.Zpos_P_of_succ_nat,
-                       @Coq.ZArith.BinInt.Pos2Z.inj_succ)
-                      (@Coq.ZArith.BinIntDef.Z.succ, @size).
-  - scrush.
+  induction n.
+  - sauto.
+  - sfirstorder unfold: size.
+  - sauto q: on.
 Qed.
 
 Lemma lem_nth_append :
@@ -105,38 +98,30 @@ Lemma lem_nth_append :
                     (if i <? size xs then znth i xs x else znth (i - size xs) ys x).
 Proof.
   induction xs.
-  - sauto.
-    + Reconstr.hcrush Reconstr.AllHyps
-                  (@Coq.ZArith.BinInt.Z.ltb_ge)
-                  Reconstr.Empty.
-    + scrush.
+  - hauto use: app_nil_l, Z.le_ngt, Z.sub_0_r unfold: negb, BinIntDef.Z.of_nat, length, Z.lt, BinIntDef.Z.ltb, size inv: bool.
   - intros.
     assert (HH: i = 0 \/ exists i', i = i' + 1 /\ 0 <= i') by
         Reconstr.hcrush Reconstr.AllHyps
                         (@Coq.ZArith.BinInt.Z.lt_le_pred, @Coq.ZArith.BinInt.Z.lt_eq_cases,
                          @Coq.ZArith.BinInt.Z.succ_pred)
                         (@Coq.ZArith.BinIntDef.Z.succ).
     destruct HH as [ ? | HH ].
-    scrush.
+    sfirstorder.
     destruct HH as [ i' HH ].
     destruct HH.
     subst; simpl.
     repeat rewrite lem_n_succ_znth by scrush.
     repeat rewrite lem_size_succ.
-    sauto.
-    + assert ((i' <? size xs) = true).
-      Reconstr.hcrush Reconstr.AllHyps
-                      (@Coq.ZArith.BinInt.Z.le_gt_cases, @Coq.Bool.Bool.diff_true_false,
-                       @Coq.ZArith.BinInt.Z.ltb_ge, @Coq.ZArith.Zbool.Zlt_is_lt_bool,
-                       @Coq.ZArith.BinInt.Z.add_le_mono_r)
-                      (@size).
-      scrush.
-    + assert ((i' <? size xs) = false).
-      Reconstr.heasy Reconstr.AllHyps
-                     (@Coq.ZArith.BinInt.Z.ltb_nlt, @Coq.ZArith.BinInt.Z.add_lt_mono_r)
-                     (@size).
-      assert (i' + 1 - (size xs + 1) = i' - size xs) by auto with zarith.
-      scrush.
+    replace (i' + 1 <? size xs + 1) with (i' <? size xs).
+    replace (i' + 1 - (size xs + 1)) with (i' - size xs) by auto with zarith.
+    hauto l: on.
+    sdestruct (i' <? size xs).
+    symmetry.
+    rewrite Z.ltb_lt.
+    auto with zarith.
+    symmetry.
+    rewrite Z.ltb_ge.
+    auto with zarith.
 Qed.
 
 Lemma lem_size_app : forall xs ys, size (xs ++ ys) = size xs + size ys.
@@ -204,7 +189,8 @@ Proof.
   intros P P' c c' H.
   induction H.
   - scrush.
-  - pose @star_step; pose lem_exec1_appendR; scrush.
+  - pose proof @star_step; pose proof lem_exec1_appendR.
+    sauto lq: on rew: off.
 Qed.
 
 Lemma lem_exec1_appendL :
@@ -246,7 +232,7 @@ Proof.
   - intros; simp_hyps; subst.
     destruct y as [ p stk0 ].
     destruct p as [ i0 s0 ].
-    pose @star_step; pose lem_exec1_appendL; scrush.
+    pose proof @star_step; pose proof lem_exec1_appendL; qauto l: on.
 Qed.
 
 Lemma lem_exec_Cons_1 :
@@ -261,7 +247,8 @@ Proof.
   rewrite HH; clear HH.
   assert (HH: 1 = size (ins :: nil) + 0) by scrush.
   rewrite HH; clear HH.
-  pose lem_exec_appendL; scrush.
+  pose proof lem_exec_appendL.
+  hauto l: on.
 Qed.
 
 Lemma lem_exec_appendL_if :
@@ -276,7 +263,7 @@ Proof.
                         (@Coq.ZArith.BinInt.Zplus_minus)
                         (@k).
   rewrite HH; clear HH.
-  pose lem_exec_appendL; scrush.
+  pose proof lem_exec_appendL; hauto l: on.
 Qed.
 
 Lemma lem_exec_append_trans :
@@ -291,7 +278,7 @@ Proof.
       (apply lem_exec_appendL_if with (j := i''); sauto).
   assert (exec (P ++ P') (0,s,stk) (i',s',stk')) by
       (apply lem_exec_appendR; sauto).
-  pose @lem_star_trans; scrush.
+  pose proof @lem_star_trans; hauto l: on.
 Qed.
 
 Ltac escrush := unfold exec; pose @star_step; pose @star_refl; scrush.
@@ -300,7 +287,7 @@ Ltac exec_tac :=
   match goal with
   | [ |- exec ?A (?i, ?s, ?stk) ?B ] =>
     assert (exec1 A (i, s, stk) B) by
-        (unfold exec1; exists i; exists s; exists stk; sauto);
+        (unfold exec1; exists i; exists s; exists stk; hfcrush);
     escrush
   end.
 
@@ -356,20 +343,27 @@ Fixpoint acomp (a : aexpr) : list instr :=
 Lemma lem_acomp_correct :
   forall a s stk, exec (acomp a) (0, s, stk) (size(acomp a), s, aval s a :: stk).
 Proof.
-  induction a; sauto.
+  induction a; ssimpl.
   - exec_tac.
   - exec_tac.
   - assert (exec (acomp a1 ++ acomp a2) (0,s,stk)
                  (size(acomp a1 ++ acomp a2),s,aval s a2 :: aval s a1 :: stk)) by exec_append_tac.
     assert (exec (ADD :: nil) (0,s,aval s a2 :: aval s a1 :: stk) (1,s,(aval s a1 + aval s a2) :: stk)) by
         exec_tac.
-    assert (forall l, size l - size l = 0) by (intro; omega);
+    assert (forall l, size l - size l = 0).
+    { hauto l: on. }
+
     assert (HH: exec ((acomp a1 ++ acomp a2) ++ ADD :: nil) (0, s, stk)
-                     (size ((acomp a1 ++ acomp a2) ++ ADD :: nil), s, aval s a1 + aval s a2 :: stk)) by
-        (apply lem_exec_append_trans with
-         (i' := size(acomp a1 ++ acomp a2)) (s' := s) (stk' := aval s a2 :: aval s a1 :: stk) (i'' := 1);
-         solve [ sauto | ycrush | rewrite lem_size_app; scrush ]).
-    clear -HH; scrush.
+                  (size ((acomp a1 ++ acomp a2) ++ ADD :: nil), s, aval s a1 + aval s a2 :: stk)).
+    {
+      apply lem_exec_append_trans with
+        (i' := size(acomp a1 ++ acomp a2)) (s' := s) (stk' := aval s a2 :: aval s a1 :: stk) (i'' := 1).
+      - hauto lq: on.
+      - hecrush.
+      - hauto lq: on.
+      - hauto lq: on use: Zpos_P_of_succ_nat, lem_size_succ, lem_size_app unfold: length, BinPosDef.Pos.of_succ_nat, BinIntDef.Z.succ, size.
+    }
+    hauto q: on use: app_assoc, Z.add_assoc, lem_size_app.
 Qed.
 
 Lemma lem_acomp_append :

Small_Step.v

@@ -37,19 +37,17 @@ Proof.
                                                (Seq c1 c2, s) -->* (Seq c1' c2, s')); [idtac|scrush].
   intros p1 p2 H.
   induction H; sauto.
-  destruct y; sauto.
-  pose @star_step; pose SeqSemS2; scrush.
 Qed.
 
 Lemma lem_seq_comp : forall c1 c2 s1 s2 s3, (c1, s1) -->* (Skip, s2) -> (c2, s2) -->* (Skip, s3) ->
                                             (Seq c1 c2, s1) -->* (Skip, s3).
 Proof.
   intros c1 c2 s1 s2 s3 H1 H2.
   assert ((Seq c1 c2, s1) -->* (Seq Skip c2, s2)).
-  pose lem_star_seq2; scrush.
-  assert ((Seq Skip c2, s2) -->* (c2, s2)).
-  pose @star_step; scrush.
-  pose @lem_star_trans; scrush.
+  pose proof lem_star_seq2.
+  srun eauto.
+  assert ((Seq Skip c2, s2) -->* (c2, s2)) by (sauto lq: on).
+  pose proof @lem_star_trans; sauto lq: on.
 Qed.
 
 Lemma lem_big_to_small : forall p s', p ==> s' -> p -->* (Skip, s').
@@ -66,36 +64,29 @@ Proof.
     Reconstr.hobvious Reconstr.AllHyps
 		      (@lem_star_seq2)
 		      Reconstr.Empty.
-    pose @lem_star_trans; pose @star_step; pose SeqSemS1; scrush.
+    eapply (lem_star_trans) with (y := (Seq c (While b c), s1)).
+    auto.
+    strivial use: lem_seq_comp.
 Qed.
 
 Lemma lem_small1_big_continue : forall p p', p --> p' -> forall s, p' ==> s -> p ==> s.
 Proof.
   intros p p' H.
-  induction H; try yelles 1.
-  - sauto; Reconstr.hobvious Reconstr.AllHyps
-		             (@Big_Step.SeqSem)
-		             Reconstr.Empty.
-  - Reconstr.htrivial Reconstr.Empty
-		      (@Big_Step.lem_while_unfold, @Big_Step.SkipSem)
-		      (@Big_Step.equiv_com).
+  induction H; sauto lq:on.
 Qed.
 
 Lemma lem_small_to_big : forall p s, p -->* (Skip, s) -> p ==> s.
 Proof.
   assert (forall p p', p -->* p' -> forall s, p' = (Skip, s) -> p ==> s); [idtac|scrush].
   intros p p' H.
-  induction H; sauto.
-  Reconstr.hsimple Reconstr.AllHyps
-		   (@lem_small1_big_continue)
-		   Reconstr.Empty.
+  induction H.
+  - hauto l:on.
+  - srun sauto use: SeqSemS1, lem_small1_big_continue, SkipSem.
 Qed.
 
 Corollary cor_big_iff_small : forall p s, p ==> s <-> p -->* (Skip, s).
 Proof.
-  Reconstr.htrivial Reconstr.Empty
-		    (@lem_small_to_big, @lem_big_to_small)
-		    Reconstr.Empty.
+  srun sauto use: lem_small_to_big, lem_big_to_small.
 Qed.
 
 (* Final configurations and infinite reductions *)
@@ -105,14 +96,18 @@ Definition final (cs : com * state) := ~(exists cs', cs --> cs').
 Lemma lem_nonfinal_dec_0 :
   forall c s, (exists cs', (c, s) --> cs') \/ (~(exists cs', (c, s) --> cs') /\ c = Skip).
 Proof.
-  induction c; sauto.
-  - pose @SeqSemS2; scrush.
-  - destruct (bval s b) eqn:?; pose @IfTrueS; pose @IfFalseS; scrush.
+  induction c.
+  - sauto lq:on.
+  - sauto lq:on.
+  - ecrush.
+  - intros s. destruct (bval s b) eqn:?; pose @IfTrueS; pose @IfFalseS; sauto lq: on rew: off.
+  - sauto lq:on.
 Qed.
 
 Lemma lem_nonfinal_dec : forall cs, (exists cs', cs --> cs') \/ ~(exists cs', cs --> cs').
 Proof.
-  pose lem_nonfinal_dec_0; scrush.
+  pose proof lem_nonfinal_dec_0.
+  hauto lq:on.
 Qed.
 
 Lemma lem_finalD : forall c s, final (c, s) -> c = Skip.
@@ -125,15 +120,16 @@ Qed.
 Lemma lem_final_iff_SKIP : forall c s, final (c, s) <-> c = Skip.
 Proof.
   split.
-  - pose lem_finalD; scrush.
-  - unfold final; scrush.
+  - pose proof lem_finalD; hauto l: on.
+  - intros H; subst.
+    sauto lq:on unfold: final.
 Qed.
 
 Lemma lem_big_iff_small_termination :
   forall cs, (exists s, cs ==> s) <-> (exists cs', cs -->* cs' /\ final cs').
 Proof.
   split.
-  - pose cor_big_iff_small; pose lem_final_iff_SKIP; scrush.
+  - pose proof cor_big_iff_small; pose proof lem_final_iff_SKIP; hauto l: on.
   - intro H; destruct H as [cs']; destruct cs'.
-    pose cor_big_iff_small; pose lem_final_iff_SKIP; scrush.
+    pose proof cor_big_iff_small; pose proof lem_final_iff_SKIP; sauto lq: on rew: off.
 Qed.