1 files changed, 86 insertions, 0 deletions
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
new file mode 100644
index 00000000..7ab720f6
--- /dev/null
+++ b/contrib/subtac/test/ListDep.v
@@ -0,0 +1,86 @@
+Require Import List.
+Require Import Coq.subtac.Utils.
+
+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.
+
+  Program Fixpoint map_rec ( l' : list U | sub_list l' l )
+    { measure l' length } : { 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.
+    
+    Obligation 1.
+    intros.
+    destruct tl' ; simpl ; simpl in e.
+    subst x0 tl0.
+    rewrite <- Heql'.
+    rewrite e.
+    auto.
+    Qed.
+
+    Obligation 2.
+    simpl.
+    intros.
+    destruct l'.
+    simpl in Heql'.
+    destruct x0 ; simpl ; try discriminate.
+    inversion Heql'.
+    inversion s.
+    apply H.
+    auto with datatypes.
+    Qed.
+
+
+    Obligation 3 of map_rec.
+    simpl.
+    intros.
+    rewrite <- Heql'.
+    simpl ; auto with arith.
+    Qed.
+
+    Obligation 4.
+    simpl.
+    intros.
+    destruct l'.
+    simpl in Heql'.
+    destruct x0 ; simpl ; try discriminate.
+    inversion Heql'.
+    subst x tl.
+    apply sub_list_tl with u ; auto.
+    Qed.
+  
+    Obligation 5.
+    intros.
+    rewrite <- Heql' ; auto.
+    Qed.
+    
+    Program Definition map : list V := map_rec l.
+    Obligation 1.
+      split ; auto.
+    Qed.
+    
+End Map_DependentRecursor.
+
+Extraction map.
+Extraction map_rec.
+