1
Require Import Coq.Arith.Arith.
5
Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }.
8
elim (le_lt_dec y x) ; intros ; auto with arith.
11
Require Import Coq.subtac.FixSub.
12
Require Import Wf_nat.
14
Lemma preda_lt_a : forall a, 0 < a -> pred a < a.
18
Program Fixpoint id_struct (a : nat) : nat :=
21
| S n => S (id_struct n)
27
then S (wfrec (pred a))
30
Program Fixpoint wfrec (a : nat) { wf a lt } : nat :=
32
then S (wfrec (pred a))
35
apply preda_lt_a ; auto.
40
Extraction Inline proj1_sig.
41
Extract Inductive bool => "bool" [ "true" "false" ].
42
Extract Inductive sumbool => "bool" [ "true" "false" ].
43
Extract Inlined Constant lt_ge_dec => "<".
46
Extraction Inline lt_ge_dec le_lt_dec.
50
Program Fixpoint structrec (a : nat) { wf a lt } : nat :=
52
S n => S (structrec n)
64
Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a).