blob: 8ad557b091dcf7b3549eb96aea9955df55cc8522 (
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
|
(*
* CoqUp: Verified high-level synthesis.
* Copyright (C) 2019-2020 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/>.
*)
From Coq Require Export
String
ZArith
Znumtheory
List
Bool.
Require Import Lia.
From coqup Require Import Show.
(* Depend on CompCert for the basic library, as they declare and prove some
useful theorems. *)
From compcert.lib Require Export Coqlib.
From compcert Require Import Integers.
Local Open Scope Z_scope.
Ltac unfold_rec c := unfold c; fold c.
Ltac solve_by_inverts n :=
match goal with | H : ?T |- _ =>
match type of T with Prop =>
inversion H;
match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end
end
end.
Ltac solve_by_invert := solve_by_inverts 1.
Ltac invert x := inversion x; subst; clear x.
Ltac destruct_match :=
match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
Ltac clear_obvious :=
repeat match goal with
| [ H : ex _ |- _ ] => invert H
| [ H : Some _ = Some _ |- _ ] => invert H
| [ H : _ /\ _ |- _ ] => invert H
end.
Ltac nicify_goals :=
repeat match goal with
| [ |- _ /\ _ ] => split
| [ |- Some _ = Some _ ] => f_equal
| [ |- S _ = S _ ] => f_equal
end.
Ltac kill_bools :=
repeat match goal with
| [ H : _ && _ = true |- _ ] => apply andb_prop in H
| [ H : _ || _ = false |- _ ] => apply orb_false_elim in H
| [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H
| [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H
| [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H
| [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H
| [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H
| [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H
| [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H
| [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H
end.
Ltac unfold_constants :=
repeat match goal with
| [ |- context[Integers.Ptrofs.modulus] ] =>
replace Integers.Ptrofs.modulus with 4294967296 by reflexivity
| [ H : context[Integers.Ptrofs.modulus] |- _ ] =>
replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity
| [ |- context[Integers.Ptrofs.min_signed] ] =>
replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity
| [ H : context[Integers.Ptrofs.min_signed] |- _ ] =>
replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity
| [ |- context[Integers.Ptrofs.max_signed] ] =>
replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity
| [ H : context[Integers.Ptrofs.max_signed] |- _ ] =>
replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity
| [ |- context[Integers.Ptrofs.max_unsigned] ] =>
replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity
| [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] =>
replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity
| [ |- context[Integers.Int.modulus] ] =>
replace Integers.Int.modulus with 4294967296 by reflexivity
| [ H : context[Integers.Int.modulus] |- _ ] =>
replace Integers.Int.modulus with 4294967296 in H by reflexivity
| [ |- context[Integers.Int.min_signed] ] =>
replace Integers.Int.min_signed with (-2147483648) by reflexivity
| [ H : context[Integers.Int.min_signed] |- _ ] =>
replace Integers.Int.min_signed with (-2147483648) in H by reflexivity
| [ |- context[Integers.Int.max_signed] ] =>
replace Integers.Int.max_signed with 2147483647 by reflexivity
| [ H : context[Integers.Int.max_signed] |- _ ] =>
replace Integers.Int.max_signed with 2147483647 in H by reflexivity
| [ |- context[Integers.Int.max_unsigned] ] =>
replace Integers.Int.max_unsigned with 4294967295 by reflexivity
| [ H : context[Integers.Int.max_unsigned] |- _ ] =>
replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity
| [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] =>
match (eval compute in (0 <=? x)) with
| true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x))
with x by reflexivity
| false => idtac
end
end.
Ltac simplify := intros; unfold_constants; simpl in *;
repeat (clear_obvious; nicify_goals; kill_bools);
simpl in *.
Infix "==nat" := eq_nat_dec (no associativity, at level 50).
Infix "==Z" := Z.eq_dec (no associativity, at level 50).
Ltac liapp :=
match goal with
| [ |- (?x | ?y) ] =>
match (eval compute in (Z.rem y x ==Z 0)) with
| left _ => let q := (eval compute in (Z.div y x)) in exists q; reflexivity
| _ => idtac
end
| _ => idtac
end.
Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
Global Opaque Nat.div.
Global Opaque Z.mul.
(* Definition const (A B : Type) (a : A) (b : B) : A := a.
Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
Module Option.
Definition default {T : Type} (x : T) (u : option T) : T :=
match u with
| Some y => y
| _ => x
end.
Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
match u with
| Some y => Some (f y)
| _ => None
end.
Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T :=
match a with
| Some x => map (f x) b
| _ => None
end.
Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
match f with
| Some a => g a
| _ => None
end.
Definition join {A : Type} (a : option (option A)) : option A :=
match a with
| None => None
| Some a' => a'
end.
Module Notation.
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
End Notation.
End Option.
Parameter debug_print : string -> unit.
Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=
let unused := debug_print (show a) in b.
Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B :=
let unused := debug_print (s ++ show a) in b.
|
