Test files for subtac.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8714 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 301 insertions, 0 deletions

diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
new file mode 100644
index 0000000000..e5f42defb9
--- /dev/null
+++ b/contrib/subtac/test/ListsTest.v
@@ -0,0 +1,101 @@
+Require Import Coq.subtac.Utils.
+Require Import List.
+Require Import Arith.
+Variable A : Set.
+
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
+Extraction Inline proj1_sig.
+Notation "'forall' { x : A | P } , Q" :=
+  (forall x:{x:A|P}, Q)
+  (at level 200, x ident, right associativity).
+Require Import Omega.
+Program Definition myhd : 
+  forall { l : list A | length l <> 0 }, A :=
+  
+  fun l =>
+    match l with
+    | nil => _
+    | hd :: tl => hd
+    end.
+
+Proof.
+  destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+Defined.
+
+Extraction myhd.
+
+Program Definition mytail : 
+  forall { l : list A | length l <> 0 }, list A :=
+
+  fun l => 
+    match `l with
+    | nil => _
+    | hd :: tl => tl
+    end.
+
+Proof.
+destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+Defined.
+
+Extraction mytail.
+
+Variable a : A.
+
+Program Definition test_hd : A := myhd (cons a nil).
+Proof.
+simpl ; auto.
+Defined.
+
+Extraction test_hd.
+
+Program Definition test_tail : list A := mytail nil.
+
+Program Fixpoint append (l : list A) (l' : list A) { struct l } :
+ { r : list A | length r = length l + length l' } :=
+ match l with
+ nil => l'
+ | hd :: tl => hd :: (append tl l')
+ end.
+rewrite Heql ; auto.
+simpl.
+rewrite (subset_simpl (append tl0 l')).
+unfold tl0 ; unfold hd0.
+rewrite Heql.
+simpl ; auto.
+Defined.
+
+Extraction append.
+
+Lemma append_app' : forall l : list A, (`append nil l) = l.
+Proof.
+simpl ; auto.
+Qed.
+
+Lemma append_app : forall l : list A, (`append l nil) = l.
+Proof.
+intros.
+induction l ; simpl ; auto.
+simpl in IHl.
+rewrite IHl.
+reflexivity.
+Qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
new file mode 100644
index 0000000000..ab200354c6
--- /dev/null
+++ b/contrib/subtac/test/Mutind.v
@@ -0,0 +1,7 @@
+Fixpoint f (a : nat) : nat := match a with 0 => 0
+| S a' => g a a'
+  end
+with g (a b : nat) { struct b } : nat := 
+  match b with 0 => 0
+  | S b' => f b'
+  end.
\ No newline at end of file
diff --git a/contrib/subtac/test/Test1.v b/contrib/subtac/test/Test1.v
new file mode 100644
index 0000000000..14b8085496
--- /dev/null
+++ b/contrib/subtac/test/Test1.v
@@ -0,0 +1,16 @@
+Program Definition test (a b : nat) : { x : nat | x = a + b } := 
+  ((a + b) : { x : nat | x = a + b }).
+Proof.
+intros.
+reflexivity.
+Qed.
+
+Print test.
+
+Require Import List.
+
+Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
+  match l with
+    nil => 1
+    | a :: l => a
+  end.
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
new file mode 100644
index 0000000000..481b6708df
--- /dev/null
+++ b/contrib/subtac/test/euclid.v
@@ -0,0 +1,66 @@
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+
+Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) =>
+@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a
+  (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)).
+
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
+  (a & a).
+reflexivity.
+Defined.
+
+Extraction testsig.
+Extraction sigS.
+Extract Inductive sigS => "" [ "" ].
+Extraction testsig.
+
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Omega.
+
+Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w.
+intros.
+assert(y * S z = y * z + y).
+auto.
+rewrite H1.
+omega.
+Qed.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
+  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  (S q' & r)
+  else (O & a).
+intro euclid.
+simpl ; intros.
+Print euclid_evars.
+eapply euclid_evars with euclid.
+refine (euclid_evars _ _ _ euclid a Acc_a b).
+; simpl ; intros.
+Show Existentials.
+
+induction b0 ; induction r.
+simpl in H.
+simpl.
+simpl in p0.
+destruct p0.
+split.
+
+apply minus_eq_add.
+omega.
+auto with arith.
+auto.
+simpl.
+induction b0 ; simpl.
+split ; auto.
+omega.
+exact (euclid a0 Acc_a0 b0).
+
+exact (Acc_a).
+auto.
+auto.
+Focus 1.
+
+
diff --git a/contrib/subtac/test/id.v b/contrib/subtac/test/id.v
new file mode 100644
index 0000000000..9ae1108817
--- /dev/null
+++ b/contrib/subtac/test/id.v
@@ -0,0 +1,46 @@
+Require Coq.Arith.Arith.
+
+Require Import Coq.subtac.Utils.
+Program Fixpoint id (n : nat) : { x : nat | x = n } :=
+  match n with
+  | O => O
+  | S p => S (id p)
+  end.
+intros ; auto.
+
+pose (subset_simpl (id p)).
+simpl in e.
+unfold p0.
+rewrite e.
+auto.
+Defined.
+
+Check id.
+Print id.
+Extraction id.
+
+Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
+Require Import Omega.
+
+Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
+  if le_gt_dec n 0 then 0
+  else S (id_if (pred n)).
+intros.
+auto with arith.
+intros.
+pose (subset_simpl (id_if (pred n))).
+simpl in e.
+rewrite e.
+induction n ; auto with arith.
+Defined.
+
+Print id_if_instance.
+Extraction id_if_instance.
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+
+Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=
+  (a & a).
+intros.
+auto.
+Qed.
diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v
new file mode 100644
index 0000000000..aaefd8cc5f
--- /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.