diff options
Diffstat (limited to 'contrib/subtac/test/ListDep.v')
-rw-r--r-- | contrib/subtac/test/ListDep.v | 86 |
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. + |