From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 contrib/subtac/test/rec.v | 65 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 contrib/subtac/test/rec.v

(limited to 'contrib/subtac/test/rec.v')

diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v
new file mode 100644
index 00000000..aaefd8cc
--- /dev/null
+++ b/contrib/subtac/test/rec.v
@@ -0,0 +1,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.
-- 
cgit v1.2.3