diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/subtac/test/rec.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/subtac/test/rec.v')
-rw-r--r-- | contrib/subtac/test/rec.v | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v deleted file mode 100644 index aaefd8cc..00000000 --- a/contrib/subtac/test/rec.v +++ /dev/null @@ -1,65 +0,0 @@ -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. |