diff options
Diffstat (limited to 'plugins/subtac/test/ListDep.v')
-rw-r--r-- | plugins/subtac/test/ListDep.v | 49 |
1 files changed, 49 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. + |