aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Bool/Reflect.v
blob: 7fac6d11a82a9dc27c34b1de461aa39fe45480c0 (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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(** * Some lemmas about [Bool.reflect] *)
Require Import Coq.Classes.CMorphisms.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith_dec.
Require Import Coq.NArith.BinNat.
Require Import Crypto.Util.HProp.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.Sum.
Require Import Crypto.Util.Comparison.
Require Import Crypto.Util.Tactics.DestructHead.
Require Crypto.Util.PrimitiveProd.

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_brel {A R Rb} (bl : forall a a' : A, Rb a a' = true -> (R a a' : Prop))
      (lb : forall a a' : A, R a a' -> Rb a a' = true)
  : forall x y, reflect (R x y) (Rb x y).
Proof.
  intros x y; specialize (bl x y); specialize (lb x y).
  destruct (Rb x y); constructor; intuition congruence.
Qed.

Lemma reflect_to_brel {A R Rb} (H : forall x y : A, reflect (R x y) (Rb x y))
  : (forall a a' : A, Rb a a' = true -> R a a')
    /\ (forall a a' : A, R a a' -> Rb a a' = true).
Proof.
  split; intros x y; specialize (H x y); destruct H; intuition congruence.
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. apply reflect_of_brel; assumption. Qed.

Lemma reflect_to_beq {A beq} (H : forall x y : A, reflect (x = y) (beq x y))
  : (forall a a' : A, beq a a' = true -> a = a')
    /\ (forall a a' : A, a = a' -> beq a a' = true).
Proof. apply reflect_to_brel; assumption. 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.

Existing Class reflect.
Definition decb (P : Prop) {b : bool} {H : reflect P b} := b.
Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
Definition decb_rel {A B} (P : A -> B -> Prop) {b : A -> B -> bool} {H : reflect_rel P b} := b.

Lemma decb_true_iff P {b} {H : reflect P b} : @decb P b H = true <-> P.
Proof. symmetry; apply reflect_iff, H. Qed.
Lemma decb_bp P {b} {H : reflect P b} : @decb P b H = true -> P.
Proof. apply decb_true_iff. Qed.
Lemma decb_pb P {b} {H : reflect P b} : P -> @decb P b H = true.
Proof. apply decb_true_iff. Qed.
Lemma decb_false_iff P {b} {H : reflect P b} : @decb P b H = false <-> ~P.
Proof. generalize (decb P), (decb_true_iff P); clear; intros []; intros; intuition congruence. Qed.
Lemma decb_false_bp P {b} {H : reflect P b} : @decb P b H = false -> ~P.
Proof. apply decb_false_iff. Qed.
Lemma decb_false_pb P {b} {H : reflect P b} : ~P -> @decb P b H = false.
Proof. apply decb_false_iff. Qed.

Global Instance dec_of_reflect P {b} {H : reflect P b} : Decidable P | 15
  := (if b as b return reflect P b -> Decidable P
      then fun H => left (decb_bp P eq_refl)
      else fun H => right (decb_false_bp P eq_refl)) H.

Global Instance eq_decb_hprop {A} {x y : A} {hp : IsHProp A} : reflect (@eq A x y) true | 5.
Proof. left; auto. Qed.

Ltac solve_reflect_step :=
  first [ match goal with
          | [ H : reflect _ ?b |- _ ] => tryif is_var b then destruct H else (inversion H; clear H)
          | [ |- reflect _ _ ] => constructor
          | [ |- reflect (?R ?x ?y) (?Rb ?x ?y) ] => apply (@reflect_of_brel _ R Rb)
          | [ H : forall x y, reflect (?R x y) (?Rb x y) |- _ ] => apply (@reflect_to_brel _ R Rb) in H
          end
        | progress destruct_head'_and
        | progress intros
        | progress subst
        | solve [ eauto
                | firstorder (auto; try discriminate) ]
            (*
          | [ H :
          | [ H : forall x y : ?A, reflect (x = y) _, x0 : ?A, y0 : ?A  |- _ ]
            => no_equalities_about x0 y0; let H' := fresh in pose proof (H x0 y0) as H'; inversion H'; clear H'
          | [ H : forall a0 (x y : _), reflect (x = y) _, x0 : ?A, y0 : ?A  |- _ ]
            => no_equalities_about x0 y0; let H' := fresh in pose proof (H _ x0 y0) as H'; inversion H'; clear H'
          | [ H : true = ?x |- context[?x] ] => rewrite <- H
          | [ H : false = ?x |- context[?x] ] => rewrite <- H
          end
        | progress intros
        | split
        | progress inversion_sigma
        | progress inversion_prod
        | progress pre_decide_destruct_sigma
        | progress destruct_head'_bool
        | progress destruct_head'_prod
        | progress subst
        | progress cbn in *
        | progress hnf
        | progress pre_hprop
        | solve [ left; firstorder (auto; try discriminate)
                | right; firstorder (auto; try discriminate)
                | firstorder (auto; try discriminate) ] *) ].


Ltac solve_reflect := repeat solve_reflect_step.

Hint Constructors reflect : typeclass_instances.

Local Hint Resolve -> Bool.eqb_true_iff : core.
Local Hint Resolve <- Bool.eqb_true_iff : core.
Local Hint Resolve internal_prod_dec_bl internal_prod_dec_lb
      PrimitiveProd.Primitive.prod_dec_bl PrimitiveProd.Primitive.prod_dec_lb
      internal_option_dec_bl internal_option_dec_lb
      internal_list_dec_bl internal_list_dec_lb
      internal_sum_dec_bl internal_sum_dec_lb
      sigT_dec_bl sigT_dec_lb
      sigT_dec_bl_hprop sigT_dec_lb_hprop
      sig_dec_bl sig_dec_lb
      sig_dec_bl_hprop sig_dec_lb_hprop
      internal_comparison_dec_bl internal_comparison_dec_lb
  : core.

Local Hint Extern 0 => solve [ solve_reflect ] : typeclass_instances.
Local Hint Extern 1 => progress inversion_sigma : core.

Global Instance reflect_True : reflect True true | 10 := ReflectT _ I.
Global Instance reflect_False : reflect False false | 10 := ReflectF _ (fun x => x).
Global Instance reflect_or {A B a b} `{reflect A a, reflect B b} : reflect (A \/ B) (orb a b) | 10. exact _. Qed.
Global Instance reflect_and {A B a b} `{reflect A a, reflect B b} : reflect (A /\ B) (andb a b) | 10. exact _. Qed.
Global Instance reflect_impl_or {A B bona} `{reflect (B \/ ~A) bona} : reflect (A -> B) bona | 15. exact _. Qed.
Global Instance reflect_impl {A B a b} `{reflect A a, reflect B b} : reflect (A -> B) (implb a b) | 10. exact _. Qed.
Global Instance reflect_iff {A B a b} `{reflect A a, reflect B b} : reflect (A <-> B) (Bool.eqb a b) | 10. exact _. Qed.
Lemma reflect_not {A a} `{reflect A a} : reflect (~A) (negb a).
Proof. exact _. Qed.

(** Disallow infinite loops of reflect_not *)
Hint Extern 0 (reflect (~?A) _) => eapply (@reflect_not A) : typeclass_instances.
Hint Extern 0 (reflect _ (negb ?b)) => eapply (@reflect_not _ b) : typeclass_instances.

Global Instance reflect_eq_unit : reflect_rel (@eq unit) (fun _ _ => true) | 10. exact _. Qed.
Global Instance reflect_eq_bool : reflect_rel (@eq bool) Bool.eqb | 10. exact _. Qed.
Global Instance reflect_eq_Empty_set : reflect_rel (@eq Empty_set) (fun _ _ => true) | 10. exact _. Qed.
Global Instance reflect_eq_prod {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A * B)) (prod_beq A B eqA eqB) | 10. exact _. Qed.
Global Instance reflect_eq_option {A eqA} `{reflect_rel (@eq A) eqA} : reflect_rel (@eq (option A)) (option_beq eqA) | 10. exact _. Qed.
Global Instance reflect_eq_list {A eqA} `{reflect_rel (@eq A) eqA} : reflect_rel (@eq (list A)) (list_beq A eqA) | 10. exact _. Qed.
Global Instance reflect_eq_list_nil_r {A eqA} {ls} : reflect (ls = @nil A) (list_beq A eqA ls (@nil A)) | 10.
Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Qed.
Global Instance reflect_eq_list_nil_l {A eqA} {ls} : reflect (@nil A = ls) (list_beq A eqA (@nil A) ls) | 10.
Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Qed.
Global Instance reflect_eq_sum {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A + B)) (sum_beq A B eqA eqB) | 10. exact _. Qed.
Global Instance reflect_eq_sigT_hprop {A P eqA} `{reflect_rel (@eq A) eqA, forall a : A, IsHProp (P a)} : reflect_rel (@eq (@sigT A P)) (sigT_beq eqA (fun _ _ _ _ => true)) | 10. exact _. Qed.
Global Instance reflect_eq_sig_hprop {A eqA} {P : A -> Prop} `{reflect_rel (@eq A) eqA, forall a : A, IsHProp (P a)} : reflect_rel (@eq (@sig A P)) (sig_beq eqA (fun _ _ _ _ => true)) | 10. exact _. Qed.
Global Instance reflect_eq_comparison : reflect_rel (@eq comparison) comparison_beq | 10. exact _. Qed.

Module Export Primitive.
  Import PrimitiveProd.
  Import PrimitiveProd.Primitive.
  Global Instance reflect_eq_prod {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A * B)) (@Primitive.prod_beq A B eqA eqB) | 10. exact _. Qed.
End Primitive.

Module Nat.
  Definition geb_spec0 : reflect_rel ge (fun x y => Nat.leb y x) := fun _ _ => Nat.leb_spec0 _ _.
  Definition gtb_spec0 : reflect_rel gt (fun x y => Nat.ltb y x) := fun _ _ => Nat.ltb_spec0 _ _.
End Nat.
Global Existing Instance Nat.eqb_spec | 10.
Global Existing Instances Nat.leb_spec0 Nat.ltb_spec0 Nat.geb_spec0 Nat.gtb_spec0.

Module N.
  Lemma geb_spec0 : reflect_rel N.ge (fun x y => N.leb y x).
  Proof. intros x y; generalize (N.leb_spec0 y x); intro H; destruct H; constructor; rewrite N.ge_le_iff; assumption. Qed.
  Lemma gtb_spec0 : reflect_rel N.gt (fun x y => N.ltb y x).
  Proof. intros x y; generalize (N.ltb_spec0 y x); intro H; destruct H; constructor; rewrite N.gt_lt_iff; assumption. Qed.
End N.
Global Existing Instance N.eqb_spec | 10.
Global Existing Instances N.leb_spec0 N.ltb_spec0 N.geb_spec0 N.gtb_spec0.

Module Z.
  Lemma geb_spec0 : reflect_rel Z.ge Z.geb.
  Proof. intros x y; generalize (Z.leb_spec0 y x); rewrite Z.geb_leb; intro H; destruct H; constructor; rewrite Z.ge_le_iff; assumption. Qed.
  Lemma gtb_spec0 : reflect_rel Z.gt Z.gtb.
  Proof. intros x y; generalize (Z.ltb_spec0 y x); rewrite Z.gtb_ltb; intro H; destruct H; constructor; rewrite Z.gt_lt_iff; assumption. Qed.
End Z.
Global Existing Instance Z.eqb_spec | 10.
Global Existing Instances Z.leb_spec0 Z.ltb_spec0 Z.geb_spec0 Z.gtb_spec0.

Module Pos.
  Lemma geb_spec0 : reflect_rel Pos.ge (fun x y => Pos.leb y x).
  Proof. intros x y; generalize (Pos.leb_spec0 y x); intro H; destruct H; constructor; rewrite Pos.ge_le_iff; assumption. Qed.
  Lemma gtb_spec0 : reflect_rel Pos.gt (fun x y => Pos.ltb y x).
  Proof. intros x y; generalize (Pos.ltb_spec0 y x); intro H; destruct H; constructor; rewrite Pos.gt_lt_iff; assumption. Qed.
End Pos.
Global Existing Instance Pos.eqb_spec | 10.
Global Existing Instances Pos.leb_spec0 Pos.ltb_spec0 Pos.geb_spec0 Pos.gtb_spec0.

Global Instance reflect_Forall {A P Pb} {HD : forall x : A, reflect (P x) (Pb x)} {ls}
  : reflect (List.Forall P ls) (List.forallb Pb ls) | 10.
Proof.
  induction ls as [|x xs IHxs]; cbn [List.forallb]; [ left | destruct (HD x), IHxs; [ left | right.. ] ];
    [ constructor; assumption | constructor; assumption | intro Hn.. ];
    clear HD;
    try abstract (inversion Hn; subst; tauto).
Qed.
Global Instance reflect_Exists {A P Pb} {HD : forall x : A, reflect (P x) (Pb x)} {ls}
  : reflect (List.Exists P ls) (List.existsb Pb ls) | 10.
Proof.
  induction ls as [|x xs IHxs]; cbn [List.existsb]; [ right | destruct (HD x), IHxs; [ left.. | right ] ];
    [ intro Hn | constructor; assumption.. | intro Hn ];
    clear HD;
    try abstract (inversion Hn; subst; tauto).
Qed.

Global Instance reflect_match_pair {A B} {P : A -> B -> Prop} {Pb : A -> B -> bool} {x : A * B}
       {HD : reflect (P (fst x) (snd x)) (Pb (fst x) (snd x))}
  : reflect (let '(a, b) := x in P a b) (let '(a, b) := x in Pb a b) | 1.
Proof. edestruct (_ : _ * _); assumption. Qed.

Definition reflect_if_bool {x : bool} {A B a b} {HA : reflect A a} {HB : reflect B b}
  : reflect (if x then A else B) (if x then a else b)
  := if x return reflect (if x then A else B) (if x then a else b)
     then HA
     else HB.

Hint Extern 1 (reflect _ (match ?x with true => ?a | false => ?b end))
=> eapply (@reflect_if_bool x _ _ a b) : typeclass_instances.
Hint Extern 1 (reflect (match ?x with true => ?A | false => ?B end) _)
=> eapply (@reflect_if_bool x A B) : typeclass_instances.

Global Instance reflect_ex_forall_not : forall T (P:T->Prop) (exPb:bool) {d:reflect (exists b, P b) exPb}, reflect (forall b, ~ P b) (negb exPb).
Proof.
  intros T P exPb d; destruct d; constructor; firstorder.
Qed.

Global Polymorphic Instance reflect_Proper_iff
  : Proper (iff ==> eq ==> iffT) reflect | 10.
Proof.
  intros A B H b b' ?; subst b'; split; intro H'; destruct H, H'; constructor; auto.
Qed.

Global Polymorphic Instance reflect_Proper_arrow
  : Proper (iff ==> eq ==> arrow) reflect | 10.
Proof.
  repeat intro; eapply reflect_Proper_iff; try eassumption; easy.
Qed.

Global Polymorphic Instance reflect_Proper_flip_arrow
  : Proper (iff ==> eq ==> flip arrow) reflect | 10.
Proof.
  repeat intro; eapply reflect_Proper_iff; try eassumption; easy.
Qed.

Lemma reflect_bool : forall {P b} {Preflect:reflect P b}, b = true -> P.
Proof. intros P b Preflect; destruct Preflect; solve [ auto | discriminate ]. Qed.

Ltac vm_reflect_no_check := apply reflect_bool; vm_cast_no_check (eq_refl true).
Ltac lazy_reflect_no_check := apply reflect_bool; exact_no_check (eq_refl true).

Ltac vm_reflect := abstract vm_reflect_no_check.
Ltac lazy_reflect := abstract lazy_reflect_no_check.