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
|
Require Import Coq.Arith.Arith.
Require Import Lt.
Require Import Omega.
Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }.
(*Proof.
intros.
elim (le_lt_dec y x) ; intros ; auto with arith.
Defined.
*)
Require Import Coq.subtac.FixSub.
Require Import Wf_nat.
Lemma preda_lt_a : forall a, 0 < a -> pred a < a.
auto with arith.
Qed.
Program Fixpoint id_struct (a : nat) : nat :=
match a with
0 => 0
| S n => S (id_struct n)
end.
Check struct_rec.
if (lt_ge_dec O a)
then S (wfrec (pred a))
else O.
Program Fixpoint wfrec (a : nat) { wf a lt } : nat :=
if (lt_ge_dec O a)
then S (wfrec (pred a))
else O.
intros.
apply preda_lt_a ; auto.
Defined.
Extraction wfrec.
Extraction Inline proj1_sig.
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
Extract Inlined Constant lt_ge_dec => "<".
Extraction wfrec.
Extraction Inline lt_ge_dec le_lt_dec.
Extraction wfrec.
Program Fixpoint structrec (a : nat) { wf a lt } : nat :=
match a with
S n => S (structrec n)
| 0 => 0
end.
intros.
unfold n0.
omega.
Defined.
Print structrec.
Extraction structrec.
Extraction structrec.
Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a).
Print structrec_fun.
|
