From f8faf0c9395047032e6fe9d0db5f45205cd4da06 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 20 Sep 2021 18:10:13 +0200 Subject: vauto is now complete w.r.t. symmetry of equality (but may be exponential in some cases) --- src/QInst.v | 131 +++++++++------------------------------ unit-tests/Tests_verit_tactics.v | 37 +++++++++++ 2 files changed, 67 insertions(+), 101 deletions(-) diff --git a/src/QInst.v b/src/QInst.v index 26430f1..c2cca4a 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -27,7 +27,6 @@ Proof. installed when we compile SMTCoq. *) Qed. -Hint Resolve impl_split. (** verit silently transforms an into a or into a when instantiating such a quantified theorem *) @@ -90,86 +89,30 @@ 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. apply eqb_sym2. 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 *) +(* Strategy: change or not the order of each equality + Complete but exponential in some cases *) 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 := - repeat match T with - | context [ (?A =? ?B)%Z] => - change (A =? B)%Z with (hidden_eq_Z A B) in T - end; - repeat match T with - | context [ @eqb_of_compdec ?A ?HA ?a ?b ] => - change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in T - end; - repeat match T with - | context [ hidden_eq_Z ?A ?B] => - replace (hidden_eq_Z A B) with (B =? A)%Z in T; - [ | now rewrite Z.eqb_sym] - end; - repeat match T with - | context [ hidden_eq_U ?A ?HA ?a ?b] => - replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a) in T; - [ | now rewrite eqb_of_compdec_sym] - end. -Ltac apply_sym_goal := - repeat match goal with - | [ |- context [ (?A =? ?B)%Z] ] => - change (A =? B)%Z with (hidden_eq_Z A B) - end; - repeat match goal with - | [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] => - change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) - end; - repeat match goal with - | [ |- context [ hidden_eq_Z ?A ?B] ] => - replace (hidden_eq_Z A B) with (B =? A)%Z; - [ | now rewrite Z.eqb_sym] - end; - repeat match goal with - | [ |- context [ hidden_eq_U ?A ?HA ?a ?b] ] => - 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 +Ltac apply_sym_hyp H := + let TH := type of H in + lazymatch TH with + | context [ (?A =? ?B)%Z ] => + first [ change (A =? B)%Z with (hidden_eq_Z A B) in H; apply_sym_hyp H + | replace (A =? B)%Z with (hidden_eq_Z B A) in H; [apply_sym_hyp H | now rewrite Z.eqb_sym] ] + | context [ @eqb_of_compdec ?A ?HA ?a ?b ] => + first [ change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in H; apply_sym_hyp H + | replace (eqb_of_compdec HA a b) with (hidden_eq_U A HA b a) in H; [apply_sym_hyp H | now rewrite eqb_of_compdec_sym] ] + | _ => apply H end. -Ltac strategy2 H := - match goal with - | [ |- ?g ] => - let TH := type of H in - order_equalities g TH; - apply H +Ltac apply_sym H := + lazymatch goal with + | [ |- context [ (?A =? ?B)%Z ] ] => + first [ change (A =? B)%Z with (hidden_eq_Z A B); apply_sym H + | replace (A =? B)%Z with (hidden_eq_Z B A); [apply_sym H | now rewrite Z.eqb_sym] ] + | [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] => + first [ change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b); apply_sym H + | replace (eqb_of_compdec HA a b) with (hidden_eq_U A HA b a); [apply_sym H | now rewrite eqb_of_compdec_sym] ] + | _ => apply_sym_hyp H end. @@ -178,33 +121,19 @@ Ltac vauto := try (unfold is_true; let H := fresh "H" in intro H; - first [ strategy1 H - | strategy2 H + first [ apply_sym 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 ] - | eapply eqb_sym_or_split_right; - first [ strategy1 H - | strategy2 H ] - | eapply eqb_sym_or_split_left; - first [ strategy1 H - | strategy2 H ] - | eapply eqb_or_split_right; - first [ strategy1 H - | strategy2 H ] - | eapply eqb_or_split_left; - first [ strategy1 H - | strategy2 H ] + first [ eapply impl_split; apply_sym H + | eapply impl_or_split_right; apply_sym H + | eapply impl_or_split_left; apply_sym H + | eapply eqb_sym_or_split_right; apply_sym H + | eapply eqb_sym_or_split_left; apply_sym H + | eapply eqb_or_split_right; apply_sym H + | eapply eqb_or_split_left; apply_sym H ] | [ |- (negb ?A || ?B || ?C) = true ] => - eapply eqb_or_split; - first [ strategy1 H - | strategy2 H ] + eapply eqb_or_split; apply_sym H end ] ); diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 34b5dfd..2bdc520 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1369,3 +1369,40 @@ Section PropToBool. Goal (forall (x x0 : bool) (x1 x2 : list bool), x :: x1 = x0 :: x2 -> x = x0) -> true. Proof. verit. Qed. End PropToBool. + + +Section EqSym. + Variable A : Type. + Variable HA : CompDec A. + Variable H8 : forall (h : list A) (l : list (list A)), tl (h :: l) = l. + Variable H12_A : forall (h : A) (l : list A), tl (h :: l) = l. + Variable H9 : forall (h : option A) (l : list (option A)), tl (h :: l) = l. + Variable H12 : @tl (list A) nil = nil. + Variable H13_A : @tl A nil = nil. + Variable H14 : @tl (option A) nil = nil. + Variable H13 : forall (h : list A) (l : list (list A)), hd_error (h :: l) = Some h. + Variable H10_A : forall (h : A) (l : list A), hd_error (h :: l) = Some h. + Variable H15 : forall (h : option A) (l : list (option A)), hd_error (h :: l) = Some h. + Variable H10 : @hd_error (list A) nil = None. + Variable H11_A : @hd_error A nil = None. + Variable H16 : @hd_error (option A) nil = None. + Variable H11 : forall x : list A, Some x = None -> False. + Variable H7_A : forall x : A, Some x = None -> False. + Variable H17 : forall x : option A, Some x = None -> False. + Variable H7 : forall x x0 : list A, Some x = Some x0 -> x = x0. + Variable H6_A : forall x x0 : A, Some x = Some x0 -> x = x0. + Variable H18 : forall x x0 : option A, Some x = Some x0 -> x = x0. + Variable H4 : forall (x : list A) (x0 : list (list A)), nil = x :: x0 -> False. + Variable H3_A : forall (x : A) (x0 : list A), nil = x :: x0 -> False. + Variable H5 : forall (x : option A) (x0 : list (option A)), nil = x :: x0 -> False. + Variable H3 : forall (x x0 : list A) (x1 x2 : list (list A)), x :: x1 = x0 :: x2 -> x = x0. + Variable H2_A : forall (x x0 : A) (x1 x2 : list A), x :: x1 = x0 :: x2 -> x = x0. + Variable H6 : forall (x x0 : option A) (x1 x2 : list (option A)), x :: x1 = x0 :: x2 -> x = x0. + Variable x : A. + Variable xs : list A. + Variable a : A. + Variable r : list A. + + Goal hd_error (x :: xs) = Some a /\ tl (x :: xs) = r <-> x :: xs = a :: r. + Proof. verit. Qed. +End EqSym. -- cgit