From 38227d031b7b5d22fd1dfba0c250d9d176659d44 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 20 Sep 2021 19:24:45 +0200 Subject: Simplify apply_sym --- src/QInst.v | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/QInst.v b/src/QInst.v index c2cca4a..16a4d5f 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -89,21 +89,10 @@ 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. -(* Strategy: change or not the order of each equality +(* Strategy: change or not the order of each equality in the goal 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 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 apply_sym H := lazymatch goal with | [ |- context [ (?A =? ?B)%Z ] ] => @@ -112,7 +101,7 @@ Ltac apply_sym H := | [ |- 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 + | _ => apply H end. -- cgit