Skip to content

Commit f5e4fa7

Browse files
lastlandlastland
committed
Fix some proofs for Coq 8.20.
1 parent 39728de commit f5e4fa7

File tree

26 files changed

+1533
-1114
lines changed

26 files changed

+1533
-1114
lines changed

‎.github/workflows/hs-to-coq.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -64,8 +64,8 @@ jobs:
6464
strategy:
6565
matrix:
6666
os: [ubuntu-latest]
67-
ocaml: [4.07.1]
68-
coq: [8.10.2]
67+
ocaml: [4.14.2]
68+
coq: [8.20.1]
6969
needs: pre_check
7070
if: ${{ needs.pre_check.outputs.should_skip_coq != 'true' }}
7171
steps:
@@ -85,7 +85,7 @@ jobs:
8585
run: |
8686
if ! [ -e $HOME/.opam/config ]; then opam init -j 2 -n -y; fi
8787
opam repo add coq-released http://coq.inria.fr/opam/released || true
88-
opam list -i coq.8.10.2 --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
88+
opam list -i coq.${{ matrix.coq }} --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
8989
opam list -i coq-mathcomp-ssreflect --silent || opam install -y coq-mathcomp-ssreflect
9090
opam install -y coq-equations.1.2+8.10
9191

‎examples/containers/hs-spec/IntSetProperties.v‎

Lines changed: 40 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ Import Test.QuickCheck.Property.Notations.
7171

7272
(* Skipping definition `IntSetProperties.test_split' *)
7373

74-
Definition forValid {a} `{Test.QuickCheck.Property.Testable a}
74+
#[global] Definition forValid {a} `{Test.QuickCheck.Property.Testable a}
7575
: (Data.IntSet.Internal.IntSet -> a) -> Prop :=
7676
fun f =>
7777
Test.QuickCheck.Property.forAll Test.QuickCheck.Arbitrary.arbitrary (fun t =>
@@ -111,37 +111,38 @@ Definition forValid {a} `{Test.QuickCheck.Property.Testable a}
111111
(f
112112
t))))).
113113

114-
Definition forValidUnitTree {a} `{Test.QuickCheck.Property.Testable a}
114+
#[global] Definition forValidUnitTree {a} `{Test.QuickCheck.Property.Testable a}
115115
: (Data.IntSet.Internal.IntSet -> a) -> Prop :=
116116
fun f => forValid f.
117117

118-
Definition prop_Valid : Prop :=
118+
#[global] Definition prop_Valid : Prop :=
119119
forValidUnitTree (fun t => IntSetValidity.valid t).
120120

121-
Definition prop_EmptyValid : Prop :=
121+
#[global] Definition prop_EmptyValid : Prop :=
122122
IntSetValidity.valid Data.IntSet.Internal.empty.
123123

124-
Definition prop_SingletonValid : Coq.Numbers.BinNums.N -> Prop :=
124+
#[global] Definition prop_SingletonValid : Coq.Numbers.BinNums.N -> Prop :=
125125
fun x => IntSetValidity.valid (Data.IntSet.Internal.singleton x).
126126

127-
Definition prop_InsertIntoEmptyValid : Coq.Numbers.BinNums.N -> Prop :=
127+
#[global] Definition prop_InsertIntoEmptyValid
128+
: Coq.Numbers.BinNums.N -> Prop :=
128129
fun x =>
129130
IntSetValidity.valid (Data.IntSet.Internal.insert x Data.IntSet.Internal.empty).
130131

131-
Definition prop_Single : Coq.Numbers.BinNums.N -> bool :=
132+
#[global] Definition prop_Single : Coq.Numbers.BinNums.N -> bool :=
132133
fun x =>
133134
(Data.IntSet.Internal.insert x Data.IntSet.Internal.empty GHC.Base.==
134135
Data.IntSet.Internal.singleton x).
135136

136-
Definition prop_Member
137+
#[global] Definition prop_Member
137138
: list Coq.Numbers.BinNums.N -> Coq.Numbers.BinNums.N -> bool :=
138139
fun xs n =>
139140
let m := Data.IntSet.Internal.fromList xs in
140141
Data.Foldable.all (fun k =>
141142
Data.IntSet.Internal.member k m GHC.Base.== (Data.Foldable.elem k xs)) (cons n
142143
xs).
143144

144-
Definition prop_NotMember
145+
#[global] Definition prop_NotMember
145146
: list Coq.Numbers.BinNums.N -> Coq.Numbers.BinNums.N -> bool :=
146147
fun xs n =>
147148
let m := Data.IntSet.Internal.fromList xs in
@@ -159,15 +160,15 @@ Definition prop_NotMember
159160

160161
(* Skipping definition `IntSetProperties.prop_LookupGE' *)
161162

162-
Definition prop_InsertDelete
163+
#[global] Definition prop_InsertDelete
163164
: Coq.Numbers.BinNums.N -> Data.IntSet.Internal.IntSet -> Prop :=
164165
fun k t =>
165166
negb (Data.IntSet.Internal.member k t) Test.QuickCheck.Property.==>
166167
(let 't' := Data.IntSet.Internal.delete k (Data.IntSet.Internal.insert k t) in
167168
IntSetValidity.valid t' Test.QuickCheck.Property..&&.(**)
168169
(t' Test.QuickCheck.Property.=== t)).
169170

170-
Definition prop_MemberFromList : list Coq.Numbers.BinNums.N -> bool :=
171+
#[global] Definition prop_MemberFromList : list Coq.Numbers.BinNums.N -> bool :=
171172
fun xs =>
172173
let abs_xs :=
173174
Coq.Lists.List.flat_map (fun x =>
@@ -179,26 +180,26 @@ Definition prop_MemberFromList : list Coq.Numbers.BinNums.N -> bool :=
179180
Data.IntSet.Internal.notMember arg_3__ t) GHC.Base.∘
180181
GHC.Num.negate) abs_xs).
181182

182-
Definition prop_UnionInsert
183+
#[global] Definition prop_UnionInsert
183184
: Coq.Numbers.BinNums.N -> Data.IntSet.Internal.IntSet -> Prop :=
184185
fun x t =>
185186
let 't' := Data.IntSet.Internal.union t (Data.IntSet.Internal.singleton x) in
186187
IntSetValidity.valid t' Test.QuickCheck.Property..&&.(**)
187188
(t' Test.QuickCheck.Property.=== Data.IntSet.Internal.insert x t).
188189

189-
Definition prop_UnionAssoc
190+
#[global] Definition prop_UnionAssoc
190191
: Data.IntSet.Internal.IntSet ->
191192
Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
192193
fun t1 t2 t3 =>
193194
Data.IntSet.Internal.union t1 (Data.IntSet.Internal.union t2 t3) GHC.Base.==
194195
Data.IntSet.Internal.union (Data.IntSet.Internal.union t1 t2) t3.
195196

196-
Definition prop_UnionComm
197+
#[global] Definition prop_UnionComm
197198
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
198199
fun t1 t2 =>
199200
(Data.IntSet.Internal.union t1 t2 GHC.Base.== Data.IntSet.Internal.union t2 t1).
200201

201-
Definition prop_Diff
202+
#[global] Definition prop_Diff
202203
: list Coq.Numbers.BinNums.N -> list Coq.Numbers.BinNums.N -> Prop :=
203204
fun xs ys =>
204205
let 't := Data.IntSet.Internal.difference (Data.IntSet.Internal.fromList xs)
@@ -208,7 +209,7 @@ Definition prop_Diff
208209
Data.OldList.sort (_Data.OldList.\\_ (Data.OldList.nub xs) (Data.OldList.nub
209210
ys))).
210211

211-
Definition prop_Int
212+
#[global] Definition prop_Int
212213
: list Coq.Numbers.BinNums.N -> list Coq.Numbers.BinNums.N -> Prop :=
213214
fun xs ys =>
214215
let 't := Data.IntSet.Internal.intersection (Data.IntSet.Internal.fromList xs)
@@ -217,33 +218,33 @@ Definition prop_Int
217218
(Data.IntSet.Internal.toAscList t Test.QuickCheck.Property.===
218219
Data.OldList.sort (Data.OldList.nub ((Data.OldList.intersect) (xs) (ys)))).
219220

220-
Definition prop_disjoint
221+
#[global] Definition prop_disjoint
221222
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
222223
fun a b =>
223224
Data.IntSet.Internal.disjoint a b GHC.Base.==
224225
Data.IntSet.Internal.null (Data.IntSet.Internal.intersection a b).
225226

226227
(* Skipping definition `IntSetProperties.prop_Ordered' *)
227228

228-
Definition prop_List : list Coq.Numbers.BinNums.N -> bool :=
229+
#[global] Definition prop_List : list Coq.Numbers.BinNums.N -> bool :=
229230
fun xs =>
230231
(Data.OldList.sort (Data.OldList.nub xs) GHC.Base.==
231232
Data.IntSet.Internal.toAscList (Data.IntSet.Internal.fromList xs)).
232233

233-
Definition prop_DescList : list Coq.Numbers.BinNums.N -> bool :=
234+
#[global] Definition prop_DescList : list Coq.Numbers.BinNums.N -> bool :=
234235
fun xs =>
235236
(GHC.List.reverse (Data.OldList.sort (Data.OldList.nub xs)) GHC.Base.==
236237
Data.IntSet.Internal.toDescList (Data.IntSet.Internal.fromList xs)).
237238

238-
Definition prop_AscDescList : list Coq.Numbers.BinNums.N -> bool :=
239+
#[global] Definition prop_AscDescList : list Coq.Numbers.BinNums.N -> bool :=
239240
fun xs =>
240241
let s := Data.IntSet.Internal.fromList xs in
241242
Data.IntSet.Internal.toAscList s GHC.Base.==
242243
GHC.List.reverse (Data.IntSet.Internal.toDescList s).
243244

244245
(* Skipping definition `IntSetProperties.prop_fromList' *)
245246

246-
Definition powersOf2 : Data.IntSet.Internal.IntSet :=
247+
#[global] Definition powersOf2 : Data.IntSet.Internal.IntSet :=
247248
Data.IntSet.Internal.fromList (Coq.Lists.List.flat_map (fun i =>
248249
cons (Coq.NArith.BinNat.N.pow #2 i) nil)
249250
(GHC.Enum.enumFromTo #0 #63)).
@@ -265,7 +266,7 @@ Fixpoint prop_Prefix (arg_0__ : Data.IntSet.Internal.IntSet) : bool
265266
| _ => true
266267
end.
267268

268-
Definition prop_LeftRight : Data.IntSet.Internal.IntSet -> bool :=
269+
#[global] Definition prop_LeftRight : Data.IntSet.Internal.IntSet -> bool :=
269270
fun arg_0__ =>
270271
match arg_0__ with
271272
| Data.IntSet.Internal.Bin _ msk left_ right_ =>
@@ -278,34 +279,34 @@ Definition prop_LeftRight : Data.IntSet.Internal.IntSet -> bool :=
278279
| _ => true
279280
end.
280281

281-
Definition toSet
282+
#[global] Definition toSet
282283
: Data.IntSet.Internal.IntSet ->
283284
Data.Set.Internal.Set_ Coq.Numbers.BinNums.N :=
284285
Data.Set.Internal.fromList GHC.Base.∘ Data.IntSet.Internal.toList.
285286

286-
Definition prop_isProperSubsetOf
287+
#[global] Definition prop_isProperSubsetOf
287288
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
288289
fun a b =>
289290
Data.IntSet.Internal.isProperSubsetOf a b GHC.Base.==
290291
Data.Set.Internal.isProperSubsetOf (toSet a) (toSet b).
291292

292-
Definition prop_isProperSubsetOf2
293+
#[global] Definition prop_isProperSubsetOf2
293294
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
294295
fun a b =>
295296
let c := Data.IntSet.Internal.union a b in
296297
Data.IntSet.Internal.isProperSubsetOf a c GHC.Base.== (a GHC.Base./= c).
297298

298-
Definition prop_isSubsetOf
299+
#[global] Definition prop_isSubsetOf
299300
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
300301
fun a b =>
301302
Data.IntSet.Internal.isSubsetOf a b GHC.Base.==
302303
Data.Set.Internal.isSubsetOf (toSet a) (toSet b).
303304

304-
Definition prop_isSubsetOf2
305+
#[global] Definition prop_isSubsetOf2
305306
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
306307
fun a b => Data.IntSet.Internal.isSubsetOf a (Data.IntSet.Internal.union a b).
307308

308-
Definition prop_size : Data.IntSet.Internal.IntSet -> Prop :=
309+
#[global] Definition prop_size : Data.IntSet.Internal.IntSet -> Prop :=
309310
fun s =>
310311
let sz := Data.IntSet.Internal.size s in
311312
(sz Test.QuickCheck.Property.===
@@ -321,7 +322,7 @@ Definition prop_size : Data.IntSet.Internal.IntSet -> Prop :=
321322

322323
(* Skipping definition `IntSetProperties.prop_findMin' *)
323324

324-
Definition prop_ord
325+
#[global] Definition prop_ord
325326
: Data.IntSet.Internal.IntSet -> Data.IntSet.Internal.IntSet -> bool :=
326327
fun s1 s2 =>
327328
GHC.Base.compare s1 s2 GHC.Base.==
@@ -330,33 +331,33 @@ Definition prop_ord
330331

331332
(* Skipping definition `IntSetProperties.prop_readShow' *)
332333

333-
Definition prop_foldR : Data.IntSet.Internal.IntSet -> bool :=
334+
#[global] Definition prop_foldR : Data.IntSet.Internal.IntSet -> bool :=
334335
fun s =>
335336
Data.IntSet.Internal.foldr cons nil s GHC.Base.== Data.IntSet.Internal.toList s.
336337

337-
Definition prop_foldR' : Data.IntSet.Internal.IntSet -> bool :=
338+
#[global] Definition prop_foldR' : Data.IntSet.Internal.IntSet -> bool :=
338339
fun s =>
339340
Data.IntSet.Internal.foldr' cons nil s GHC.Base.==
340341
Data.IntSet.Internal.toList s.
341342

342-
Definition prop_foldL : Data.IntSet.Internal.IntSet -> bool :=
343+
#[global] Definition prop_foldL : Data.IntSet.Internal.IntSet -> bool :=
343344
fun s =>
344345
Data.IntSet.Internal.foldl (GHC.Base.flip cons) nil s GHC.Base.==
345346
Data.Foldable.foldl (GHC.Base.flip cons) nil (Data.IntSet.Internal.toList s).
346347

347-
Definition prop_foldL' : Data.IntSet.Internal.IntSet -> bool :=
348+
#[global] Definition prop_foldL' : Data.IntSet.Internal.IntSet -> bool :=
348349
fun s =>
349350
Data.IntSet.Internal.foldl' (GHC.Base.flip cons) nil s GHC.Base.==
350351
Data.Foldable.foldl' (GHC.Base.flip cons) nil (Data.IntSet.Internal.toList s).
351352

352-
Definition prop_map : Data.IntSet.Internal.IntSet -> bool :=
353+
#[global] Definition prop_map : Data.IntSet.Internal.IntSet -> bool :=
353354
fun s => Data.IntSet.Internal.map GHC.Base.id s GHC.Base.== s.
354355

355356
(* Skipping definition `IntSetProperties.prop_maxView' *)
356357

357358
(* Skipping definition `IntSetProperties.prop_minView' *)
358359

359-
Definition prop_split
360+
#[global] Definition prop_split
360361
: Data.IntSet.Internal.IntSet -> Coq.Numbers.BinNums.N -> Prop :=
361362
fun s i =>
362363
let 'pair s1 s2 := Data.IntSet.Internal.split i s in
@@ -369,7 +370,7 @@ Definition prop_split
369370
(Data.IntSet.Internal.delete i s Test.QuickCheck.Property.===
370371
Data.IntSet.Internal.union s1 s2)))).
371372

372-
Definition prop_splitMember
373+
#[global] Definition prop_splitMember
373374
: Data.IntSet.Internal.IntSet -> Coq.Numbers.BinNums.N -> Prop :=
374375
fun s i =>
375376
let 'pair (pair s1 t) s2 := Data.IntSet.Internal.splitMember i s in
@@ -384,7 +385,7 @@ Definition prop_splitMember
384385
(Data.IntSet.Internal.delete i s Test.QuickCheck.Property.===
385386
Data.IntSet.Internal.union s1 s2))))).
386387

387-
Definition prop_splitRoot : Data.IntSet.Internal.IntSet -> bool :=
388+
#[global] Definition prop_splitRoot : Data.IntSet.Internal.IntSet -> bool :=
388389
fun s =>
389390
let loop :=
390391
fun arg_0__ =>
@@ -402,7 +403,7 @@ Definition prop_splitRoot : Data.IntSet.Internal.IntSet -> bool :=
402403
let ls := Data.IntSet.Internal.splitRoot s in
403404
andb (loop ls) (s GHC.Base.== Data.IntSet.Internal.unions ls).
404405

405-
Definition prop_partition
406+
#[global] Definition prop_partition
406407
: Data.IntSet.Internal.IntSet -> Coq.Numbers.BinNums.N -> Prop :=
407408
fun s i =>
408409
let 'pair s1 s2 := Data.IntSet.Internal.partition GHC.Real.odd s in
@@ -414,7 +415,7 @@ Definition prop_partition
414415
Test.QuickCheck.Property..&&.(**)
415416
(s Test.QuickCheck.Property.=== Data.IntSet.Internal.union s1 s2)))).
416417

417-
Definition prop_filter
418+
#[global] Definition prop_filter
418419
: Data.IntSet.Internal.IntSet -> Coq.Numbers.BinNums.N -> Prop :=
419420
fun s i =>
420421
let evens := Data.IntSet.Internal.filter GHC.Real.even s in

‎examples/containers/lib/Data/IntMap/Internal.h2ci‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,35 @@
1-
constructors:
2-
Data.IntMap.Internal.WhenMatched: ! '[Qualified "Data.IntMap.Internal" "Mk_WhenMatched"]'
3-
Data.IntMap.Internal.View: ! '[Qualified "Data.IntMap.Internal" "Mk_View"]'
4-
Data.IntMap.Internal.WhenMissing: ! '[Qualified "Data.IntMap.Internal" "Mk_WhenMissing"]'
5-
Data.IntMap.Internal.IntMap: ! '[Qualified "Data.IntMap.Internal" "Bin",Qualified
6-
"Data.IntMap.Internal" "Tip",Qualified "Data.IntMap.Internal" "Nil"]'
7-
Data.IntMap.Internal.Stack: ! '[Qualified "Data.IntMap.Internal" "Push",Qualified
8-
"Data.IntMap.Internal" "Nada"]'
9-
Data.IntMap.Internal.SplitLookup: ! '[Qualified "Data.IntMap.Internal" "Mk_SplitLookup"]'
101
constructorFields:
112
Data.IntMap.Internal.Mk_WhenMissing: RecordFields [Qualified "Data.IntMap.Internal"
123
"missingSubtree",Qualified "Data.IntMap.Internal" "missingKey"]
4+
Data.IntMap.Internal.Nada: NonRecordFields 0
5+
Data.IntMap.Internal.Mk_SplitLookup: NonRecordFields 3
6+
Data.IntMap.Internal.Bin: NonRecordFields 4
137
Data.IntMap.Internal.Mk_View: NonRecordFields 3
148
Data.IntMap.Internal.Nil: NonRecordFields 0
159
Data.IntMap.Internal.Tip: NonRecordFields 2
16-
Data.IntMap.Internal.Nada: NonRecordFields 0
17-
Data.IntMap.Internal.Mk_SplitLookup: NonRecordFields 3
1810
Data.IntMap.Internal.Push: NonRecordFields 3
19-
Data.IntMap.Internal.Bin: NonRecordFields 4
2011
Data.IntMap.Internal.Mk_WhenMatched: RecordFields [Qualified "Data.IntMap.Internal"
2112
"matchedKey"]
22-
recordFieldTypes:
23-
Data.IntMap.Internal.matchedKey: Qualified "Data.IntMap.Internal" "WhenMatched"
24-
Data.IntMap.Internal.missingKey: Qualified "Data.IntMap.Internal" "WhenMissing"
25-
Data.IntMap.Internal.missingSubtree: Qualified "Data.IntMap.Internal" "WhenMissing"
2613
constructorTypes:
2714
Data.IntMap.Internal.Mk_WhenMissing: Qualified "Data.IntMap.Internal" "WhenMissing"
15+
Data.IntMap.Internal.Nada: Qualified "Data.IntMap.Internal" "Stack"
16+
Data.IntMap.Internal.Mk_SplitLookup: Qualified "Data.IntMap.Internal" "SplitLookup"
17+
Data.IntMap.Internal.Bin: Qualified "Data.IntMap.Internal" "IntMap"
2818
Data.IntMap.Internal.Mk_View: Qualified "Data.IntMap.Internal" "View"
2919
Data.IntMap.Internal.Nil: Qualified "Data.IntMap.Internal" "IntMap"
3020
Data.IntMap.Internal.Tip: Qualified "Data.IntMap.Internal" "IntMap"
31-
Data.IntMap.Internal.Nada: Qualified "Data.IntMap.Internal" "Stack"
32-
Data.IntMap.Internal.Mk_SplitLookup: Qualified "Data.IntMap.Internal" "SplitLookup"
3321
Data.IntMap.Internal.Push: Qualified "Data.IntMap.Internal" "Stack"
34-
Data.IntMap.Internal.Bin: Qualified "Data.IntMap.Internal" "IntMap"
3522
Data.IntMap.Internal.Mk_WhenMatched: Qualified "Data.IntMap.Internal" "WhenMatched"
23+
constructors:
24+
Data.IntMap.Internal.WhenMissing: '[Qualified "Data.IntMap.Internal" "Mk_WhenMissing"]'
25+
Data.IntMap.Internal.IntMap: '[Qualified "Data.IntMap.Internal" "Bin",Qualified
26+
"Data.IntMap.Internal" "Tip",Qualified "Data.IntMap.Internal" "Nil"]'
27+
Data.IntMap.Internal.Stack: '[Qualified "Data.IntMap.Internal" "Push",Qualified
28+
"Data.IntMap.Internal" "Nada"]'
29+
Data.IntMap.Internal.SplitLookup: '[Qualified "Data.IntMap.Internal" "Mk_SplitLookup"]'
30+
Data.IntMap.Internal.WhenMatched: '[Qualified "Data.IntMap.Internal" "Mk_WhenMatched"]'
31+
Data.IntMap.Internal.View: '[Qualified "Data.IntMap.Internal" "Mk_View"]'
32+
recordFieldTypes:
33+
Data.IntMap.Internal.matchedKey: Qualified "Data.IntMap.Internal" "WhenMatched"
34+
Data.IntMap.Internal.missingSubtree: Qualified "Data.IntMap.Internal" "WhenMissing"
35+
Data.IntMap.Internal.missingKey: Qualified "Data.IntMap.Internal" "WhenMissing"

0 commit comments

Comments
 (0)