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
|
(** * General recursive functions
This file explores a way to formalize general recursive functions
without worrying about termination proofs, counters or monads.
The definitions are actually defined by well-founded recursion on the
total relation (which isn't well-founded). Using fueling of the
accessibility proof, we can however compute with these definitions
inside Coq and reason on them independently of the termination
proof. *)
(* begin hide *)
(** printing elimination %\coqdoctac{elimination}% *)
(** printing noconf %\coqdoctac{noconf}% *)
(** printing simp %\coqdoctac{simp}% *)
(** printing by %\coqdockw{by}% *)
(** printing rec %\coqdockw{rec}% *)
(** printing Coq %\Coq{}% *)
(** printing funelim %\coqdoctac{funelim}% *)
(** printing Derive %\coqdockw{Derive}% *)
(** printing Signature %\coqdocclass{Signature}% *)
(** printing Subterm %\coqdocclass{Subterm}% *)
(** printing NoConfusion %\coqdocclass{NoConfusion}% *)
From Equations Require Import Equations.
Require Import ZArith Lia.
Require Import Program.
Require Import Psatz.
Require Import Nat.
Require Import Coq.Vectors.VectorDef.
Require Import Relations.
Set Keyed Unification.
Set Equations Transparent.
(* end hide *)
(** The total relation. *)
Definition total_relation {A : Type} : A -> A -> Prop := fun x y => True.
(** We assume an inconsistent axiom here, one should be added function per function. *)
Axiom wf_total_init : forall {A}, WellFounded (@total_relation A).
#[local]
Remove Hints wf_total_init : typeclass_instances.
(** We fuel it with some Acc_intro constructors so that definitions relying on it
can unfold a fixed number of times still. *)
#[local]
Instance wf_total_init_compute : forall {A}, WellFounded (@total_relation A).
exact (fun A => Acc_intro_generator 10 wf_total_init).
Defined.
(** Now we define an obviously non-terminating function. *)
Equations? nonterm (n : nat) : nat by wf n (@total_relation nat) :=
nonterm 0 := 0;
nonterm (S n) := S (nonterm (S n)).
Proof.
(* Every pair of arguments is in the total relation: so
[total_relation (S n) (S n)] *) red.
constructor.
Defined.
Local Obligation Tactic := idtac.
(** The automation has a little trouble here as it assumes
well-founded definitions implicitely. We show the second
equation: [nonterm (S n) = S (nonterm (S n))] using the
unfolding equation. *)
Next Obligation.
intros. now rewrite nonterm_unfold_eq at 1.
Defined.
(* Note this is a dangerous rewrite rule, so we should remove it from the hints *)
(* Print Rewrite HintDb nonterm. *)
(** Make nonterm transparent anyway so we can compute with it *)
Transparent nonterm.
(** We can compute with it (for closed natural numbers) *)
Definition at_least_five (n : nat) : bool :=
match n with
| S (S (S (S (S x)))) => true
| _ => false
end.
Transparent wf_total_init_compute.
(** Indeed it unfolds enough so that [at_least_five] gives back a result. *)
Example check_10 := eq_refl : at_least_five (nonterm 10) = true.
Example check_0 := eq_refl : at_least_five (nonterm 0) = false.
(** The elimination principle completely abstracts away from the
termination argument as well *)
Lemma nonterm_ge n : n <= nonterm n.
Proof.
funelim (nonterm n).
reflexivity.
lia.
Defined.
(** We can go as far as defining the (call-by-name) Y combinator and computing with it. *)
Section Y.
Context {A : Type}.
Equations? Y (f : A -> A) : A by wf f (@total_relation (A -> A)) :=
Y f := f (Y f).
Proof.
(* Every pair of arguments is in the total relation: so
[total_relation f f] *) red. constructor.
Defined.
Obligation Tactic := idtac.
(** The automation has a little trouble here as it assumes
well-founded definitions implicitely. We show the second
equation: [nonterm (S n) = S (nonterm (S n))] using the
unfolding equation. *)
Next Obligation.
intros. now rewrite Y_unfold_eq at 1.
Defined.
End Y.
(** Using [Y], we can easily define any general recursive function. *)
Definition fact :=
Y (fun (fact : nat -> nat) (x : nat) =>
match x with
| 0 => 1
| S n => S n * fact n
end).
Check eq_refl : fact 8 = 40320.
(** [Y] is only good in call-by-name or call-by-need, so we switch to Haskell *)
Extraction Language Haskell.
Recursive Extraction fact.
(*
y :: (a1 -> a1) -> a1
y x =
x (y x)
fact :: Nat -> Nat
fact =
y (\fact0 x -> case x of {
O -> S O;
S n -> mul (S n) (fact0 n)})
*)
(** Let's define an efficient version whose termination is not entirely obvious. *)
Definition factN :=
Y (fun (fact : N -> N) (x : N) =>
match x with
| N0 => 1%N
| Npos n => (Npos n * fact (Pos.pred_N n))%N
end).
(** [1001!] is pretty large. *)
Definition fact1001 :=
402789647337170867317246136356926989705094239074925347176343710340368450911027649612636252695456374205280468598807393254690298539867803367460225153499614535588421928591160833678742451354915921252299285456946271396995850437959540645019696372741142787347450281325324373824456300226871609431497826989489109522725791691167945698509282421538632966523376679891823696900982075223188279465194065489111498586522997573307838057934994706212934291477882221464914058745808179795130018969175605739824237247684512790169648013778158661520384916357285547219660337504067910087936301580874662367543921288988208261944834178369169805682489420504038334529389177845089679546075023305854006141256288633820079940395329251563788399404652902154519302928365169452383531030755684578503851488154092323576150311569325891190105926118761607100286827930472944913272420825078912158741589850136017030887975452922434889688775883386977825215904423682478943313806072144097432418695807412571292308739802481089407002523955080148184062810447564594783139830113821372260474145316521647368313934670783858482781506915288378941348078689691815657785305896912277993200639858696294199549107738635599538328374931258525869323348477334798827676297868823693023377418942304272267800509765805435653787530370118261219994752588866451072715583785495394684524593296728611334955079882857173250037068541860372512693170819259309411027837176612444692649174536429745421086287708588130082168792750697158901737130221751430550976429258055277255676893874108456870904122902259417224707137723406125811549952159629766771063079472679280213882978523785424760309678138268708239764925768714349554665438389311198715040908077757086900159389712443987670244241787904585093011546861502058550090914877900852701619648229332192401075747543562989953271508977501771085759521631427816116191761031257454497039673414248149210836002497114107565960458576525212556159634975715552638678172137468172843066451093984443636560722213668172225585711566558134467392654185460222589723312097599987253417831473939565071006344352518096564427781204200068323913056897090916602712260306869786107237077572445866572945760977721639408338430009976028970539150822336553856613962747814621747092348996915755983464741082000337526945990059365493439921937093368896754791416759604324895514660325913157843796039917819613717350380997781225472000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000%N.
(** We can still compute with our [Y] combinator *)
Time Check (@eq_refl _ (fact1001) <: factN 1001 = fact1001).
(** It takes [0.8sec] using [vm_compute]. *)
(** An alternative is to use the total relation directly. *)
Equations factN' (n : N) : N by wf n (@total_relation N) :=
| N0 => 1;
| Npos n => (Npos n * factN' (Pos.pred_N n)).
Next Obligation. constructor. Defined.
(** Unsurprisingly, this computes just as well *)
Time Check (@eq_refl _ (fact1001) <: factN' 1001 = fact1001).
(** It takes [0.8sec] using [vm_compute] as well. *)
(** [factN'] also makes sense in a strict/call-by-value language like OCaml. *)
Extraction Language OCaml.
Extraction factN'.
(*
(** val factN' : n -> n **)
let rec factN' = function
| N0 -> Npos XH
| Npos p -> N.mul (Npos p) (let y = Pos.pred_N p in factN' y)
*)
|
