aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/test/rec.v
blob: aaefd8cc5fe2116052badd706612c65dd72226e4 (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
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.