blob: 73364c3e20617ef93f4775b0a2e95d722c23a570 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(** * Some lemmas about [Bool.reflect] *)
Require Import Coq.Bool.Bool.
Lemma reflect_to_dec_iff {P b1 b2} : reflect P b1 -> (b1 = b2) <-> (if b2 then P else ~P).
Proof.
intro H; destruct H, b2; split; intuition congruence.
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.
|
