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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.NArith.BinNat.
Require Import Coq.Arith.Arith.
Require Import Bedrock.Word.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Util.WordUtil.
Require Import Crypto.Util.Tactics.BreakMatch.
Definition wordT_beq_hetero {logsz1 logsz2} : wordT logsz1 -> wordT logsz2 -> bool
:= match logsz1 return wordT logsz1 -> wordT logsz2 -> bool with
| 5 as logsz1' | 6 as logsz1' | 7 as logsz1'
| _ as logsz1'
=> match logsz2 return wordT logsz1' -> wordT logsz2 -> bool with
| 5 as logsz2' | 6 as logsz2' | 7 as logsz2'
| _ as logsz2'
=> @Word.weqb_hetero (2^logsz1') (2^logsz2')
end
end.
(* transparent so the equality proof can compute away *)
Lemma pow2_inj_helper x y : 2^x = 2^y -> x = y.
Proof.
destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ].
intro H; exfalso.
abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; omega).
Defined.
Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl.
Proof.
induction x; simpl; [ reflexivity | ].
etransitivity; [ | exact (f_equal (fun p => f_equal S p) (IHx eq_refl)) ]; clear IHx.
unfold pow2_inj_helper in *; simpl.
pose proof (NatUtil.nat_eq_dec_S x x).
do 2 edestruct NatUtil.nat_eq_dec; try assumption; try (exfalso; assumption).
match goal with
| [ H : ?x <> ?x |- _ ] => exfalso; clear -H; exact (H eq_refl)
end.
Defined.
Lemma pow2_inj_helper_eq_rect x y P v v'
: (exists pf : 2^x = 2^y, eq_rect _ P v _ pf = v')
-> (exists pf : x = y, eq_rect _ (fun e => P (2^e)) v _ pf = v').
Proof.
intros [pf H]; exists (pow2_inj_helper x y pf); subst v'.
destruct (NatUtil.nat_eq_dec x y) as [H|H];
[ | exfalso; clear -pf H;
abstract (apply pow2_inj_helper in pf; omega) ].
subst; rewrite pow2_inj_helper_refl; simpl.
pose proof (NatUtil.UIP_nat_transparent _ _ pf eq_refl); subst pf.
reflexivity.
Defined.
Definition wordT_beq_lb logsz1
: forall x y : wordT logsz1, x = y -> wordT_beq_hetero x y = true
:= match logsz1 return forall x y : wordT logsz1, x = y -> wordT_beq_hetero x y = true with
| 5 as logsz1' | 6 as logsz1' | 7 as logsz1'
| _ as logsz1'
=> fun x y pf => proj2 (@Word.weqb_hetero_true_iff (2^logsz1') x (2^logsz1') y) (ex_intro _ eq_refl pf)
end.
Definition wordT_beq_hetero_lb {logsz1 logsz2}
: forall x y, (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y) -> wordT_beq_hetero x y = true.
Proof.
intros x y [pf H]; subst logsz2; revert x y H; simpl.
apply wordT_beq_lb.
Defined.
Definition wordT_beq_bl logsz
: forall x y : wordT logsz, wordT_beq_hetero x y = true -> x = y
:= match logsz return forall x y : wordT logsz, wordT_beq_hetero x y = true -> x = y with
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7
| _
=> fun x y pf => proj1 (Word.weqb_hetero_homo_true_iff _ x y) pf
end.
Lemma wordT_beq_hetero_type_lb_false logsz1 logsz2 x y : logsz1 <> logsz2 -> @wordT_beq_hetero logsz1 logsz2 x y = false.
Proof.
destruct (wordT_beq_hetero x y) eqn:H; [ | reflexivity ].
revert H.
repeat (try destruct logsz1 as [|logsz1];
try destruct logsz2 as [|logsz2];
try (intros; omega);
try (intro H'; apply Word.weqb_hetero_true_iff in H'; destruct H' as [pf H']; pose proof (pow2_inj_helper _ _ pf); try omega)).
Qed.
Definition wordT_beq_hetero_bl {logsz1 logsz2}
: forall x y, wordT_beq_hetero x y = true -> (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y).
Proof.
refine match logsz1, logsz2 return forall x y, wordT_beq_hetero x y = true -> (exists pf : logsz1 = logsz2, eq_rect _ wordT x _ pf = y) with
| 0, 0 | 1, 1 | 2, 2 | 3, 3 | 4, 4 | 5, 5 | 6, 6
| 7, 7
=> fun x y pf => ex_intro _ eq_refl (@wordT_beq_bl _ x y pf)
| S (S (S (S (S (S (S (S a))))))), S (S (S (S (S (S (S (S b)))))))
=> match NatUtil.nat_eq_dec a b with
| left pf
=> match pf with
| eq_refl => fun x y pf => ex_intro _ eq_refl (@wordT_beq_bl _ x y pf)
end
| right n => fun x y pf => match _ : False with end
end
| _, _
=> fun x y pf => match _ : False with end
end;
try abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence).
Defined.
|
