10 files changed, 421 insertions, 0 deletions

diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
new file mode 100644
index 00000000..e3dbd127
--- /dev/null
+++ b/plugins/subtac/test/ListDep.v
@@ -0,0 +1,49 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import List.
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+
+Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
+
+Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
+Proof.
+  intros.
+  inversion H.
+  split.
+  intros.
+  apply H0.
+  auto with datatypes.
+  auto with arith.
+Qed.
+
+Section Map_DependentRecursor.
+  Variable U V : Set.
+  Variable l : list U.
+  Variable f : { x : U | In x l } -> V.
+
+  Obligations Tactic := unfold sub_list in * ;
+    program_simpl ; intuition.
+
+  Program Fixpoint map_rec ( l' : list U | sub_list l' l )
+    { measure length l' } : { r : list V | length r = length l' } :=
+    match l' with
+      | nil => nil
+      | cons x tl => let tl' := map_rec tl in
+	f x :: tl'
+    end.
+
+  Next Obligation.
+    destruct_call map_rec.
+    simpl in *.
+    subst l'.
+    simpl ; auto with arith.
+  Qed.
+
+  Program Definition map : list V := map_rec l.
+
+End Map_DependentRecursor.
+
+Extraction map.
+Extraction map_rec.
+
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
new file mode 100644
index 00000000..2cea0841
--- /dev/null
+++ b/plugins/subtac/test/ListsTest.v
@@ -0,0 +1,99 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import Coq.Program.Program.
+Require Import List.
+
+Set Implicit Arguments.
+
+Section Accessors.
+  Variable A : Set.
+
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=
+    fun l =>
+      match l with
+        | nil => !
+        | hd :: tl => hd
+      end.
+
+  Program Definition mytail (l : list A | length l <> 0) : list A :=
+    match l with
+      | nil => !
+      | hd :: tl => tl
+    end.
+End Accessors.
+
+Program Definition test_hd : nat := myhd (cons 1 nil).
+
+(*Eval compute in test_hd*)
+(*Program Definition test_tail : list A := mytail nil.*)
+
+Section app.
+  Variable A : Set.
+
+  Program Fixpoint app (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 :: (tl ++ l')
+    end
+    where "x ++ y" := (app x y).
+
+  Next Obligation.
+    intros.
+    destruct_call app ; program_simpl.
+  Defined.
+
+  Program Lemma app_id_l : forall l : list A, l = nil ++ l.
+  Proof.
+    simpl ; auto.
+  Qed.
+
+  Program Lemma app_id_r : forall l : list A, l = l ++ nil.
+  Proof.
+    induction l ; simpl in * ; auto.
+    rewrite <- IHl ; auto.
+  Qed.
+
+End app.
+
+Extraction app.
+
+Section Nth.
+
+  Variable A : Set.
+
+  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
+    match n, l with
+      | 0, hd :: _ => hd
+      | S n', _ :: tl => nth tl n'
+      | _, nil => !
+    end.
+
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith.
+  Defined.
+
+  Next Obligation.
+  Proof.
+    inversion H.
+  Qed.
+
+  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
+    match l, n with
+      | hd :: _, 0 => hd
+      | _ :: tl, S n' => nth' tl n'
+      | nil, _ => !
+    end.
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith.
+  Defined.
+
+  Next Obligation.
+  Proof.
+    intros.
+    inversion H.
+  Defined.
+
+End Nth.
+
diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
new file mode 100644
index 00000000..01e2d75f
--- /dev/null
+++ b/plugins/subtac/test/Mutind.v
@@ -0,0 +1,20 @@
+Require Import List.
+
+Program Fixpoint f a : { x : nat | x > 0 } :=
+  match a with
+  | 0 => 1
+  | S a' => g a a'
+  end
+with g a b : { x : nat | x > 0 } :=
+  match b with
+  | 0 => 1
+  | S b' => f b'
+  end.
+
+Check f.
+Check g.
+
+
+
+
+
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
new file mode 100644
index 00000000..7e0755d5
--- /dev/null
+++ b/plugins/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/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
new file mode 100644
index 00000000..97c3d941
--- /dev/null
+++ b/plugins/subtac/test/euclid.v
@@ -0,0 +1,24 @@
+Require Import Coq.Program.Program.
+Require Import Coq.Arith.Compare_dec.
+Notation "( x & y )" := (existS _ x y) : core_scope.
+
+Require Import Omega.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
+  { 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).
+
+Next Obligation.
+  assert(b * S q' = b * q' + b) by auto with arith ; omega.
+Defined.
+
+Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
+
+Eval lazy beta zeta delta iota in test_euclid.
+
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
+  (a & S a).
+
+Check testsig.
diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v
new file mode 100644
index 00000000..9ae11088
--- /dev/null
+++ b/plugins/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/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v
new file mode 100644
index 00000000..4f938f4f
--- /dev/null
+++ b/plugins/subtac/test/measure.v
@@ -0,0 +1,20 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.Program.Program.
+
+Fixpoint size (a : nat) : nat :=
+  match a with
+  0 => 1
+  | S n => S (size n)
+  end.
+
+Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
+  match a with
+  | S (S n) => S (test_measure n)
+  | 0 | S 0 => a
+  end.
+
+Check test_measure.
+Print test_measure.
\ No newline at end of file
diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v
new file mode 100644
index 00000000..aaefd8cc
--- /dev/null
+++ b/plugins/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.
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
new file mode 100644
index 00000000..90ae8bae
--- /dev/null
+++ b/plugins/subtac/test/take.v
@@ -0,0 +1,34 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import JMeq.
+Require Import List.
+Require Import Program.
+
+Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
+
+Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
+  match n with
+  | 0 => nil
+  | S p =>
+    match l with
+    | cons hd tl => let rest := take tl p in cons hd rest
+    | nil => !
+    end
+  end.
+
+Require Import Omega.
+Solve All Obligations.
+Next Obligation.
+  destruct_call take ; program_simpl.
+Defined.
+
+Next Obligation.
+  intros.
+  inversion H.
+Defined.
+
+
+
+
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v
new file mode 100644
index 00000000..5ccc154a
--- /dev/null
+++ b/plugins/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+  destruct_exists ;
+  repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac :=  do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+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).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof.
\ No newline at end of file