diff options
author | Jason Gross <jgross@mit.edu> | 2018-09-27 16:49:51 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-09-27 16:52:03 -0400 |
commit | 1bb26e27d97aa102a94751047b309da4b2f75a67 (patch) | |
tree | d24dc98434092b377398283cbb8f02dc8b17c639 /src/Util | |
parent | e89a4297bb1acf6f72c2fb68f3b9cd126f5ce28b (diff) |
Add more reflect tactics
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Bool/Reflect.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index 0baefa0e4..73364c3e2 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -8,3 +8,30 @@ Qed. Lemma reflect_to_dec {P b1 b2} : reflect P b1 -> (b1 = b2) -> (if b2 then P else ~P). Proof. intro; apply reflect_to_dec_iff; assumption. Qed. + +Lemma reflect_of_dec {P} {b1 b2 : bool} : reflect P b1 -> (if b2 then P else ~P) -> (b1 = b2). +Proof. intro; apply reflect_to_dec_iff; assumption. Qed. + +Lemma reflect_of_beq {A beq} (bl : forall a a' : A, beq a a' = true -> a = a') + (lb : forall a a' : A, a = a' -> beq a a' = true) + : forall x y, reflect (x = y) (beq x y). +Proof. + intros x y; specialize (bl x y); specialize (lb x y). + destruct (beq x y); constructor; intuition congruence. +Qed. + +Definition mark {T} (v : T) := v. + +Ltac beq_to_eq beq bl lb := + let lem := constr:(@reflect_of_beq _ beq bl lb) in + repeat match goal with + | [ |- context[bl ?x ?y ?pf] ] => generalize dependent (bl x y pf); try clear pf; intros + | [ H : beq ?x ?y = true |- _ ] => apply (@reflect_to_dec _ _ true (lem x y)) in H; cbv beta iota in H + | [ H : beq ?x ?y = false |- _ ] => apply (@reflect_to_dec _ _ false (lem x y)) in H; cbv beta iota in H + | [ |- beq ?x ?y = true ] => refine (@reflect_of_dec _ _ true (lem x y) _) + | [ |- beq ?x ?y = false ] => refine (@reflect_of_dec _ _ false (lem x y) _) + | [ H : beq ?x ?y = true |- ?G ] + => change (mark G); generalize dependent (bl x y H); clear H; + intros; cbv beta delta [mark] + | [ H : context[beq ?x ?x] |- _ ] => rewrite (lb x x eq_refl) in H + end. |