From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

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

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

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.
+
-- 
cgit v1.2.3