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
|
(*|
..
Vericert: Verified high-level synthesis.
Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
====================
Decidable Equalities
====================
|*)
Require compcert.backend.RTL.
Require Import compcert.common.AST.
Require Import compcert.lib.Maps.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Floats.
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.Gible.
Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
Proof.
decide equality.
Defined.
Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
Proof.
generalize comparison_eq; intro.
generalize Int.eq_dec; intro.
generalize Int64.eq_dec; intro.
decide equality.
Defined.
Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
Proof.
generalize Int.eq_dec; intro.
generalize AST.ident_eq; intro.
generalize Z.eq_dec; intro.
generalize Ptrofs.eq_dec; intro.
decide equality.
Defined.
Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
Proof.
decide equality.
Defined.
Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
Proof.
generalize Int.eq_dec; intro.
generalize Int64.eq_dec; intro.
generalize Float.eq_dec; intro.
generalize Float32.eq_dec; intro.
generalize AST.ident_eq; intro.
generalize condition_eq; intro.
generalize addressing_eq; intro.
generalize typ_eq; intro.
decide equality.
Defined.
Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
Proof.
decide equality.
Defined.
Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
Proof.
generalize typ_eq; intro.
decide equality.
Defined.
Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
Proof.
generalize typ_eq; intro.
decide equality.
Defined.
Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
Proof.
repeat decide equality.
Defined.
Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
Proof.
generalize operation_eq; intro.
decide equality.
Defined.
Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}.
Proof.
generalize Pos.eq_dec; intros.
decide equality.
Defined.
Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
Proof.
repeat decide equality.
Defined.
Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
Proof.
generalize Pos.eq_dec; intro.
generalize typ_eq; intro.
generalize Int.eq_dec; intro.
generalize Ptrofs.eq_dec; intro.
generalize Int64.eq_dec; intro.
generalize Float.eq_dec; intro.
generalize Float32.eq_dec; intro.
generalize memory_chunk_eq; intro.
generalize addressing_eq; intro.
generalize operation_eq; intro.
generalize condition_eq; intro.
generalize signature_eq; intro.
generalize list_operation_eq; intro.
generalize list_pos_eq; intro.
generalize AST.ident_eq; intro.
repeat decide equality.
Defined.
Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
Proof.
generalize Pos.eq_dec; intro.
generalize typ_eq; intro.
generalize Int.eq_dec; intro.
generalize Int64.eq_dec; intro.
generalize Float.eq_dec; intro.
generalize Float32.eq_dec; intro.
generalize Ptrofs.eq_dec; intro.
generalize memory_chunk_eq; intro.
generalize addressing_eq; intro.
generalize operation_eq; intro.
generalize condition_eq; intro.
generalize signature_eq; intro.
generalize list_operation_eq; intro.
generalize list_pos_eq; intro.
generalize AST.ident_eq; intro.
repeat decide equality.
Defined.
Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
if eqd a b then true else false.
|
