2 files changed, 78 insertions, 136 deletions
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 8429c267..b8d13fe6 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,95 +1,76 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import Coq.subtac.Utils.
 Require Import List.
 
-Variable A : Set.
-
-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.
+Set Implicit Arguments.
 
+Section Accessors.
+  Variable A : Set.
 
-Extraction myhd.
-Extraction Inline proj1_sig.
+  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+    fun l =>
+      match l with
+        | nil => !
+        | hd :: tl => hd
+      end.
 
-Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
-  fun l => 
+  Program Definition mytail (l : list A | length l <> 0) : list A :=
     match l with
-    | nil => _
-    | hd :: tl => tl
+      | nil => !
+      | hd :: tl => tl
     end.
-Proof.
-destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
-Defined.
-
-Extraction mytail.
-
-Variable a : A.
+End Accessors.
 
-Program Definition test_hd : A := myhd (cons a nil).
-Proof.
-simpl ; auto.
-Defined.
-
-Extraction test_hd.
+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 ; subtac_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 ; 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.
 
-
-
-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.
-subst ; auto.
-simpl ; rewrite (subset_simpl (append tl0 l')).
-simpl ; subst.
-simpl ; auto.
-Defined.
-
-Extraction append.
-
-
-Program Lemma append_app' : forall l : list A, l = append nil l.
-Proof.
-simpl ; auto.
-Qed.
-
-Program Lemma append_app : forall l : list A, l = append l nil.
-Proof.
-intros.
-induction l ; simpl ; auto.
-simpl in IHl.
-rewrite <- IHl.
-reflexivity.
-Qed.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+  Next Obligation.
+  Proof.
+    inversion l0.
+  Defined.
+End Nth.
 
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index ba5bdf23..a5a8b85f 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,66 +1,27 @@
-
-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 sig.
-Extract Inductive sig => "" [ "" ].
-Extraction testsig.
-
+Require Import Coq.subtac.Utils.
 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}  :
+Notation "( x & y )" := (existS _ x y) : core_scope.
+  
+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).
-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.
+Require Import Omega.
+
+Obligations.
+Solve Obligations using subtac_simpl ; omega.
+
+Next Obligation.
+  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+Defined.
 
-apply minus_eq_add.
-omega.
-auto with arith.
-auto.
-simpl.
-induction b0 ; simpl.
-split ; auto.
-omega.
-exact (euclid a0 Acc_a0 b0).
+Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
 
-exact (Acc_a).
-auto.
-auto.
-Focus 1.
+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.