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
|
From QuickChick Require Import QuickChick Tactics TacticsUtil Instances
Classes DependentClasses Sets EnumProofs.
Require Import String. Open Scope string.
From Coq Require Import List Lia.
From Ltac2 Require Import Ltac2.
Import ListNotations.
Import QcDefaultNotation. Open Scope qc_scope.
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.
Set Bullet Behavior "Strict Subproofs".
(** Examples *)
Inductive tree A : Type :=
| Leaf : A -> tree A
| Leaf' : A -> A -> tree A
| Node : A -> tree A -> tree A -> tree A.
Derive EnumSized for tree.
#[local]
Instance EnumTree_SizedMonotonic A {_ : Enum A} :
SizedMonotonic (@enumSized _ (@EnumSizedtree A _)).
Proof. derive_enum_SizedMonotonic (). Qed.
#[local]
Instance EnumTree_SizeMonotonic A `{EnumMonotonic A} :
forall s, SizeMonotonic (@enumSized _ (@EnumSizedtree A _) s).
Proof. derive_enum_SizeMonotonic (). Qed.
#[local]
Instance EnumTree_correct A `{EnumMonotonicCorrect A} :
CorrectSized (@enumSized _ (@EnumSizedtree A _)).
Proof. derive_enum_Correct (). Qed.
Inductive Foo : Type :=
| Bar.
Derive EnumSized for Foo.
#[local]
Instance EnumFoo_SizedMonotonic :
SizedMonotonic (@enumSized _ EnumSizedFoo).
Proof. derive_enum_SizedMonotonic (). Qed.
#[local]
Instance EnumFoo_SizeMonotonic :
forall s, SizeMonotonic (@enumSized _ EnumSizedFoo s).
Proof. derive_enum_SizeMonotonic (). Qed.
#[local]
Instance EnumFoo_correct :
CorrectSized (@enumSized _ EnumSizedFoo).
Proof. derive_enum_Correct (). Qed.
Inductive Foo2 A : Type :=
| Bar1
| Bar2 : A -> Foo2 A.
Derive EnumSized for Foo2.
#[local]
Instance EnumFoo2_SizedMonotonic A {_ : Enum A} :
SizedMonotonic (@enumSized _ (@EnumSizedFoo2 A _)).
Proof. derive_enum_SizedMonotonic (). Qed.
#[local]
Instance EnumFoo2_SizeMonotonic A `{EnumMonotonic A} :
forall s, SizeMonotonic (@enumSized _ (@EnumSizedFoo2 A _) s).
Proof. derive_enum_SizeMonotonic (). Qed.
#[local]
Instance EnumFoo2_correct A `{EnumMonotonicCorrect A} :
CorrectSized (@enumSized _ (@EnumSizedFoo2 A _)).
Proof. derive_enum_Correct (). Qed.
(* Example with two IH *)
Inductive goodTree : nat -> tree nat -> Prop :=
| GL : goodTree 0 (Leaf nat 0)
| GN :
forall k t1 t2 n m,
goodTree n t1 ->
goodTree m t2 ->
goodTree m t1 ->
goodTree (S n) (Node nat k t1 t2).
|
