From 1cd1e8d4e3399a582c2f5b8de203ba59cd3f8010 Mon Sep 17 00:00:00 2001 From: ckeller Date: Mon, 26 Apr 2021 16:25:57 +0200 Subject: Take hypotheses from the local context (#91) * The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context * `prop2bool_hyps` also apply to hypotheses not in the local context * Second strategy for vauto (still incomplete) --- src/PropToBool.v | 13 +++- src/QInst.v | 74 +++++++++++++++--- src/trace/coqTerms.ml | 4 +- src/versions/standard/Tactics_standard.v | 127 ++++++++++++++++++++++++++++--- unit-tests/Tests_lfsc_tactics.v | 10 +-- unit-tests/Tests_verit_tactics.v | 98 +++++++++++------------- 6 files changed, 241 insertions(+), 85 deletions(-) diff --git a/src/PropToBool.v b/src/PropToBool.v index 25662ad..64d88cf 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -26,7 +26,11 @@ Ltac prop2bool := match goal with | [ |- forall _ : ?t, _ ] => lazymatch type of t with - | Prop => fail + | Prop => + match t with + | forall _ : _, _ => intro + | _ => fail + end | _ => intro end @@ -197,7 +201,7 @@ Ltac prop2bool_hyp H := [ bool2prop; apply H | ]; (* Replace the Prop version with the bool version *) - clear H; assert (H:=H'); clear H' + try clear H; let H := fresh H in assert (H:=H'); clear H' ]. Ltac prop2bool_hyps Hs := @@ -220,11 +224,14 @@ Section Test. prop2bool_hyp basic. prop2bool_hyp no_eq. prop2bool_hyp uninterpreted_type. + admit. + prop2bool_hyp plus_n_O. Abort. Goal True. Proof. - prop2bool_hyps (basic, no_eq, uninterpreted_type). + prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, plus_O_n). + admit. Abort. End Test. diff --git a/src/QInst.v b/src/QInst.v index bb2cfd1..4ebdcc9 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -45,8 +45,11 @@ Proof. destruct a; destruct c; intuition. Qed. -(* verit considers equality modulo its symmetry, so we have to recover the - right direction in the instances of the theorems *) +(** verit considers equality modulo its symmetry, so we have to recover the + right direction in the instances of the theorems *) +(* TODO: currently incomplete *) + +(* An auxiliary lemma to rewrite an eqb_of_compdec into its the symmetrical version *) Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) : eqb_of_compdec HA b a = eqb_of_compdec HA a b. Proof. @@ -58,6 +61,10 @@ Proof. intro H1. elim H. symmetry. now rewrite compdec_eq_eqb. Qed. +(* First strategy: change the order of all equalities in the goal or the + hypotheses + Incomplete: all or none of the equalities are changed, whereas we may + need to change some of them but not all of them *) Definition hidden_eq_Z (a b : Z) := (a =? b)%Z. Definition hidden_eq_U (A:Type) (HA:CompDec A) (a b : A) := eqb_of_compdec HA a b. Ltac apply_sym_hyp T := @@ -98,20 +105,63 @@ Ltac apply_sym_goal := replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a); [ | now rewrite eqb_of_compdec_sym] end. +Ltac strategy1 H := + first [ apply H + | apply_sym_goal; apply H + | apply_sym_hyp H; apply H + | apply_sym_goal; apply_sym_hyp H; apply H + ]. + +(* Second strategy: find the order of equalities + Incomplete: does not work if the lemma is quantified *) +Ltac order_equalities g TH := + match g with + | eqb_of_compdec ?HC ?a1 ?b1 => + match TH with + | eqb_of_compdec _ ?a2 _ => + first [ constr_eq a1 a2 | replace (eqb_of_compdec HC a1 b1) with (eqb_of_compdec HC b1 a1) by now rewrite eqb_of_compdec_sym ] + | _ => idtac + end + | Z.eqb ?a1 ?b1 => + match TH with + | Z.eqb ?a2 _ => + first [ constr_eq a1 a2 | replace (Z.eqb a1 b1) with (Z.eqb b1 a1) by now rewrite Z.eqb_sym ] + | _ => idtac + end + | ?f1 ?t1 => + match TH with + | ?f2 ?t2 => order_equalities f1 f2; order_equalities t1 t2 + | _ => idtac + end + | _ => idtac + end. +Ltac strategy2 H := + match goal with + | [ |- ?g ] => + let TH := type of H in + order_equalities g TH; + apply H + end. + (* An automatic tactic that takes into account all those transformations *) Ltac vauto := - try (let H := fresh "H" in + try (unfold is_true; + let H := fresh "H" in intro H; - try apply H; - try (apply_sym_goal; apply H); - try (apply_sym_hyp H; apply H); - try (apply_sym_goal; apply_sym_hyp H; apply H); - match goal with - | [ |- is_true (negb ?A || ?B) ] => - try (eapply impl_or_split_right; apply H); - eapply impl_or_split_left; apply H - end + first [ strategy1 H + | strategy2 H + | match goal with + | [ |- (negb ?A || ?B) = true ] => + first [ eapply impl_or_split_right; + first [ strategy1 H + | strategy2 H ] + | eapply impl_or_split_left; + first [ strategy1 H + | strategy2 H ] + ] + end + ] ); auto. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index ca5f3cc..6cbdbc0 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -452,7 +452,9 @@ let list_of_constr_tuple = let c, args = Structures.decompose_app t in if c = Lazy.force cpair then match args with - | [_;_;t;l] -> list_of_constr_tuple (l::acc) t + | [_;_;t1;t2] -> + let acc' = list_of_constr_tuple acc t1 in + list_of_constr_tuple acc' t2 | _ -> assert false else t::acc diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index 6ddf5a5..468de7a 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -17,11 +17,74 @@ Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances Declare ML Module "smtcoq_plugin". -Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto. -Tactic Notation "verit_bool" := verit_bool_base (@None nat); vauto. +(** Collect all the hypotheses from the context *) -Tactic Notation "verit_bool_no_check" constr(h) := verit_bool_no_check_base (Some h); vauto. -Tactic Notation "verit_bool_no_check" := verit_bool_no_check_base (@None nat); vauto. +Ltac get_hyps_acc acc k := + match goal with + | [ H : ?P |- _ ] => + let T := type of P in + match T with + | Prop => + lazymatch P with + | id _ => fail + | _ => + change P with (id P) in H; + match acc with + | Some ?t => get_hyps_acc (Some (H, t)) k + | None => get_hyps_acc (Some H) k + end + end + | _ => fail + end + | _ => k acc + end. + +Ltac eliminate_id := + repeat match goal with + | [ H : ?P |- _ ] => + lazymatch P with + | id ?Q => change P with Q in H + | _ => fail + end + end. + +Ltac get_hyps k := get_hyps_acc (@None nat) ltac:(fun Hs => eliminate_id; k Hs). + + +Section Test. + Variable A : Type. + Hypothesis H1 : forall a:A, a = a. + Variable n : Z. + Hypothesis H2 : n = 17%Z. + + Goal True. + Proof. + (* get_hyps ltac:(fun acc => idtac acc). *) + Abort. +End Test. + + +(** Tactics in bool *) + +Tactic Notation "verit_bool" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_base (Some (h, Hs)) + | None => verit_bool_base (Some h) + end; + vauto). +Tactic Notation "verit_bool" := + get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto). + +Tactic Notation "verit_bool_no_check" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_no_check_base (Some (h, Hs)) + | None => verit_bool_no_check_base (Some h) + end; + vauto). +Tactic Notation "verit_bool_no_check" := + get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto). (** Tactics in Prop **) @@ -29,18 +92,58 @@ Tactic Notation "verit_bool_no_check" := verit_bool_no_check_base (@No Ltac zchaff := prop2bool; zchaff_bool; bool2prop. Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. -Tactic Notation "verit" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool h; bool2prop ] ]. -Tactic Notation "verit" := prop2bool; [ .. | verit_bool ; bool2prop ]. -Tactic Notation "verit_no_check" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool_no_check h; bool2prop ] ]. -Tactic Notation "verit_no_check" := prop2bool; [ .. | verit_bool_no_check ; bool2prop ]. +Tactic Notation "verit" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base (Some (h, Hs)) ] + | None => verit_bool_base (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base (Some Hs) ] + | None => verit_bool_base (@None nat) + end; vauto) + ]. +Tactic Notation "verit_no_check" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base (Some (h, Hs)) ] + | None => verit_bool_no_check_base (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit_no_check" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base (Some Hs) ] + | None => verit_bool_no_check_base (@None nat) + end; vauto) + ]. Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. -Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool h ]); cvc4_bool; try (prop2bool_hyps h; [ .. | verit_bool h ]); bool2prop ]). -Tactic Notation "smt" := (prop2bool; [ .. | try verit_bool ; cvc4_bool; try verit_bool ; bool2prop ]). -Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); cvc4_bool_no_check; try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); bool2prop]). -Tactic Notation "smt_no_check" := (prop2bool; [ .. | try verit_bool_no_check ; cvc4_bool_no_check; try verit_bool_no_check ; bool2prop]). +Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try verit h; cvc4_bool; try verit h; bool2prop ]). +Tactic Notation "smt" := (prop2bool; [ .. | try verit ; cvc4_bool; try verit ; bool2prop ]). +Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try verit_no_check h; cvc4_bool_no_check; try verit_no_check h; bool2prop]). +Tactic Notation "smt_no_check" := (prop2bool; [ .. | try verit_no_check ; cvc4_bool_no_check; try verit_no_check ; bool2prop]). diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index eb9744b..280ed17 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -714,13 +714,13 @@ Section A_BV_EUF_LIA_PR. Goal forall (x: bitvector 1), bv_subt x #b|0| = x. Proof using. smt. - Admitted. + Abort. (* The original issue (invalid) *) Goal forall (x: bitvector 1), bv_subt (bv_shl #b|0| x) #b|0| = #b|0|. Proof using. smt. - Admitted. + Abort. End A_BV_EUF_LIA_PR. @@ -760,15 +760,15 @@ Section Group. (* Some other interesting facts about groups *) Lemma unique_identity e': (forall z, op e' z ==? z) -> e' ==? e. - Proof. intros pe'; smt pe'. Qed. + Proof. smt. Qed. Lemma simplification_right x1 x2 y: op x1 y ==? op x2 y -> x1 ==? x2. - Proof. intro H. smt_no_check (H, inverse'). Qed. + Proof. smt_no_check 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. + Proof. smt_no_check inverse'. Qed. Clear_lemmas. End Group. diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 59c40a1..a270fdd 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -30,9 +30,7 @@ Qed. Lemma fun_const2 : forall f (g : Z -> Z -> bool), (forall x, g (f x) 2) -> g (f 3) 2. -Proof using. - intros f g Hf. verit Hf. -Qed. +Proof using. verit. Qed. (* Simple connectives *) @@ -531,140 +529,140 @@ Qed. Lemma taut1_bool : forall f, f 2 =? 0 -> f 2 =? 0. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma taut1 : forall f, f 2 = 0 -> f 2 = 0. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma taut2_bool : forall f, 0 =? f 2 -> 0 =? f 2. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma taut2 : forall f, 0 = f 2 -> 0 = f 2. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma taut3_bool : forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0. -Proof using. intros f p1 p2. verit (p1, p2). Qed. +Proof using. verit. Qed. Lemma taut3 : forall f, f 2 = 0 -> f 3 = 5 -> f 2 = 0. -Proof using. intros f p1 p2. verit (p1, p2). Qed. +Proof using. verit. Qed. Lemma taut4_bool : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. -Proof using. intros f p1 p2. verit (p1, p2). Qed. +Proof using. verit. Qed. Lemma taut4 : forall f, f 3 = 5 -> f 2 = 0 -> f 2 = 0. -Proof using. intros f p1 p2. verit (p1, p2). Qed. +Proof using. verit. Qed. Lemma test_eq_sym a b : implb (a =? b) (b =? a). Proof using. verit. Qed. Lemma taut5_bool : forall f, 0 =? f 2 -> f 2 =? 0. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma taut5 : forall f, 0 = f 2 -> f 2 = 0. -Proof using. intros f p. verit p. Qed. +Proof using. verit. Qed. Lemma fun_const_Z_bool : forall f , (forall x, f x =? 2) -> f 3 =? 2. -Proof using. intros f Hf. verit Hf. Qed. +Proof using. verit. Qed. Lemma fun_const_Z : forall f , (forall x, f x = 2) -> f 3 = 2. -Proof using. intros f Hf. verit Hf. Qed. +Proof using. verit. Qed. Lemma lid (A : bool) : A -> A. -Proof using. intro a. verit a. Qed. +Proof using. verit. Qed. Lemma lpartial_id A : (xorb A A) -> (xorb A A). -Proof using. intro xa. verit xa. Qed. +Proof using. verit. Qed. Lemma llia1_bool X Y Z: (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) -> (X + Y <=? 10) || (X + Z <=? 12). -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia1 X Y Z: (X <= 3) /\ ((Y <= 7) \/ (Z <= 9)) -> (X + Y <= 10) \/ (X + Z <= 12). -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia2_bool X: X - 3 =? 7 -> X >=? 10. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia2 X: X - 3 = 7 -> X >= 10. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia3_bool X Y: X >? Y -> Y + 1 <=? X. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia3 X Y: X > Y -> Y + 1 <= X. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia6_bool X: andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma llia6 X: ((X - 3) <= 7) /\ (7 <= (X - 3)) -> X >= 10. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma even_odd b1 b2 x1 x2: (ifb b1 (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) -> ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma lcongr1_bool (a b : Z) (P : Z -> bool) f: (f a =? b) -> (P (f a)) -> P b. -Proof using. intros eqfab pfa. verit (eqfab, pfa). Qed. +Proof using. verit. Qed. Lemma lcongr1 (a b : Z) (P : Z -> bool) f: (f a = b) -> (P (f a)) -> P b. -Proof using. intros eqfab pfa. verit (eqfab, pfa). Qed. +Proof using. verit. Qed. Lemma lcongr2_bool (f:Z -> Z -> Z) x y z: x =? y -> f z x =? f z y. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma lcongr2 (f:Z -> Z -> Z) x y z: x = y -> f z x = f z y. -Proof using. intro p. verit p. Qed. +Proof using. verit. Qed. Lemma lcongr3_bool (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. -Proof using. intros eqxy pzx. verit (eqxy, pzx). Qed. +Proof using. verit. Qed. Lemma lcongr3 (P:Z -> Z -> bool) x y z: x = y -> P z x -> P z y. -Proof using. intros eqxy pzx. verit (eqxy, pzx). Qed. +Proof using. verit. Qed. Lemma test20_bool : forall x, (forall a, a 0 <=? x = false. -Proof using. intros x H. verit H. Qed. +Proof using. verit. Qed. Lemma test20 : forall x, (forall a, a < x) -> ~ (0 <= x). -Proof using. intros x H. verit H. Qed. +Proof using. verit. Qed. Lemma test21_bool : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). -Proof using. intros x H. verit H. Qed. +Proof using. verit. Qed. Lemma test21 : forall x, (forall a, ~ (x <= a)) -> ~ (0 <= x). -Proof using. intros x H. verit H. Qed. +Proof using. verit. Qed. Lemma un_menteur_bool (a b c d : Z) dit: dit a =? c -> @@ -673,7 +671,7 @@ Lemma un_menteur_bool (a b c d : Z) dit: (a =? c) || (a =? d) -> (b =? c) || (b =? d) -> a =? d. -Proof using. intros H1 H2 H3 H4 H5. verit (H1, H2, H3, H4, H5). Qed. +Proof using. verit. Qed. Lemma un_menteur (a b c d : Z) dit: dit a = c -> @@ -682,19 +680,19 @@ Lemma un_menteur (a b c d : Z) dit: (a = c) \/ (a = d) -> (b = c) \/ (b = d) -> a = d. -Proof using. intros H1 H2 H3 H4 H5. verit (H1, H2, H3, H4, H5). Qed. +Proof using. verit. Qed. Lemma const_fun_is_eq_val_0_bool : forall f : Z -> Z, (forall a b, f a =? f b) -> forall x, f x =? f 0. -Proof using. intros f Hf. verit Hf. Qed. +Proof using. verit. Qed. Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, (forall a b, f a = f b) -> forall x, f x = f 0. -Proof using. intros f Hf. verit Hf. Qed. +Proof using. verit. Qed. (* You can use to permanently add the lemmas H1 .. Hn to the environment. You should use when you do not @@ -899,15 +897,15 @@ Section GroupZ. Lemma unique_identity_Z e': (forall z, op e' z =? z) -> e' =? e. - Proof using associative identity inverse. intros pe'. verit pe'. Qed. + Proof using associative identity inverse. verit. Qed. Lemma simplification_right_Z x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof using associative identity inverse. intro H. verit H. Qed. + Proof using associative identity inverse. verit. Qed. Lemma simplification_left_Z x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof using associative identity inverse. intro H. verit H. Qed. + Proof using associative identity inverse. verit. Qed. Clear_lemmas. End GroupZ. @@ -932,15 +930,15 @@ Section GroupBool. Lemma unique_identity_bool e': (forall z, op e' z ==? z) -> e' ==? e. - Proof using associative identity inverse. intros pe'. verit pe'. Qed. + Proof using associative identity inverse. verit. Qed. Lemma simplification_right_bool x1 x2 y: op x1 y ==? op x2 y -> x1 ==? x2. - Proof using associative identity inverse. intro H. verit H. Qed. + Proof using associative identity inverse. verit. Qed. Lemma simplification_left_bool x1 x2 y: op y x1 ==? op y x2 -> x1 ==? x2. - Proof using associative identity inverse. intro H. verit H. Qed. + Proof using associative identity inverse. verit. Qed. Clear_lemmas. End GroupBool. @@ -972,15 +970,13 @@ Section Group. Lemma simplification_right x1 x2 y: op x1 y = op x2 y -> x1 = x2. Proof using associative identity inverse HG. - intro H. - verit (associative, identity, inverse, H). + verit (associative, identity, inverse). Qed. Lemma simplification_left x1 x2 y: op y x1 = op y x2 -> x1 = x2. Proof using associative identity inverse HG. - intro H. - verit (associative, identity, inverse, H). + verit (associative, identity, inverse). Qed. Clear_lemmas. @@ -1144,14 +1140,12 @@ Qed. Goal forall (x : positive), Zpos x <=? Zpos x. Proof using. - intros. verit. Qed. Goal forall (x : positive) (a : Z), (Z.eqb a a) || negb (Zpos x