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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.TypeInversion.
Require Import Crypto.Reflection.Equality.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.PartiallyReifiedProp.
Require Import Crypto.Util.HProp.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.FixedWordSizesEquality.
Require Import Crypto.Util.NatUtil.
Global Instance dec_eq_base_type : DecidableRel (@eq base_type)
:= base_type_eq_dec.
Global Instance dec_eq_flat_type : DecidableRel (@eq (flat_type base_type)) := _.
Global Instance dec_eq_type : DecidableRel (@eq (type base_type)) := _.
Definition base_type_eq_semidec_transparent (t1 t2 : base_type)
: option (t1 = t2)
:= match base_type_eq_dec t1 t2 with
| left pf => Some pf
| right _ => None
end.
Lemma base_type_eq_semidec_is_dec t1 t2 : base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2.
Proof.
unfold base_type_eq_semidec_transparent; break_match; congruence.
Qed.
Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
:= match f, g return bool with
| OpConst TZ v, OpConst TZ v' => Z.eqb v v'
| OpConst _ _, _ => false
| Add T1, Add T2
| Sub T1, Sub T2
| Mul T1, Mul T2
| Shl T1, Shl T2
| Shr T1, Shr T2
| Land T1, Land T2
| Lor T1, Lor T2
| Cmovne T1, Cmovne T2
| Cmovle T1, Cmovle T2
=> base_type_beq T1 T2
| Neg T1 n, Neg T2 m
=> base_type_beq T1 T2 && Z.eqb n m
| Cast T1 T2, Cast T1' T2'
=> base_type_beq T1 T1' && base_type_beq T2 T2'
| Add _, _ => false
| Sub _, _ => false
| Mul _, _ => false
| Shl _, _ => false
| Shr _, _ => false
| Land _, _ => false
| Lor _, _ => false
| Neg _ _, _ => false
| Cmovne _, _ => false
| Cmovle _, _ => false
| Cast _ _, _ => false
end%bool.
Definition op_beq t1 tR (f g : op t1 tR) : bool
:= Eval cbv [op_beq_hetero] in op_beq_hetero f g.
Definition op_beq_hetero_type_eq {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1' /\ tR = tR'.
Proof.
destruct f, g;
repeat match goal with
| _ => progress unfold op_beq_hetero in *
| _ => simpl; intro; exfalso; assumption
| _ => solve [ repeat constructor ]
| _ => progress destruct_head base_type
| [ |- context[reified_Prop_of_bool ?b] ]
=> let H := fresh in destruct (Sumbool.sumbool_of_bool b) as [H|H]; rewrite H
| [ H : nat_beq _ _ = true |- _ ] => apply internal_nat_dec_bl in H; subst
| [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_bl in H; subst
| [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_hetero_bl in H; destruct H; subst
| [ H : andb ?x ?y = true |- _ ]
=> assert (x = true /\ y = true) by (destruct x, y; simpl in *; repeat constructor; exfalso; clear -H; abstract congruence);
clear H
| [ H : and _ _ |- _ ] => destruct H
| [ H : false = true |- _ ] => exfalso; clear -H; abstract congruence
| [ H : true = false |- _ ] => exfalso; clear -H; abstract congruence
end.
Defined.
Definition op_beq_hetero_type_eqs {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1'
:= fun H => let (p, q) := @op_beq_hetero_type_eq t1 tR t1' tR' f g H in p.
Definition op_beq_hetero_type_eqd {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> tR = tR'
:= fun H => let (p, q) := @op_beq_hetero_type_eq t1 tR t1' tR' f g H in q.
Definition op_beq_hetero_eq {t1 tR t1' tR'} f g
: forall pf : to_prop (@op_beq_hetero t1 tR t1' tR' f g),
eq_rect
_ (fun src => op src tR')
(eq_rect _ (fun dst => op t1 dst) f _ (op_beq_hetero_type_eqd f g pf))
_ (op_beq_hetero_type_eqs f g pf)
= g.
Proof.
destruct f, g;
repeat match goal with
| _ => solve [ intros [] ]
| _ => reflexivity
| [ H : False |- _ ] => exfalso; assumption
| _ => intro
| [ |- context[op_beq_hetero_type_eqd ?f ?g ?pf] ]
=> generalize (op_beq_hetero_type_eqd f g pf), (op_beq_hetero_type_eqs f g pf)
| _ => intro
| _ => progress eliminate_hprop_eq
| _ => progress inversion_flat_type
| _ => progress unfold op_beq_hetero in *
| _ => progress simpl in *
| [ H : context[andb ?x ?y] |- _ ]
=> destruct x eqn:?, y eqn:?; simpl in H
| [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
| [ H : to_prop (reified_Prop_of_bool ?b) |- _ ] => destruct b eqn:?; compute in H
| _ => progress subst
| _ => progress break_match_hyps
| [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_bl in H; subst
| [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_hetero_bl in H; destruct H; subst
| _ => congruence
end.
Qed.
Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y.
Proof.
intros ?? f g H.
pose proof (op_beq_hetero_eq f g H) as H'.
generalize dependent (op_beq_hetero_type_eqd f g H).
generalize dependent (op_beq_hetero_type_eqs f g H).
intros; eliminate_hprop_eq; simpl in *; assumption.
Qed.
|
