diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/subtac/test/ListDep.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
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. + |