diff options
Diffstat (limited to 'theories7/Lists/TheoryList.v')
| -rwxr-xr-x | theories7/Lists/TheoryList.v | 386 |
1 files changed, 386 insertions, 0 deletions
diff --git a/theories7/Lists/TheoryList.v b/theories7/Lists/TheoryList.v new file mode 100755 index 00000000..f7adda70 --- /dev/null +++ b/theories7/Lists/TheoryList.v @@ -0,0 +1,386 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: TheoryList.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Some programs and results about lists following CAML Manual *) + +Require Export PolyList. +Set Implicit Arguments. +Chapter Lists. + +Variable A : Set. + +(**********************) +(** The null function *) +(**********************) + +Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l. + +Lemma Isnil_nil : (Isnil (nil A)). +Red; Auto. +Qed. +Hints Resolve Isnil_nil. + +Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)). +Unfold Isnil. +Intros; Discriminate. +Qed. + +Hints Resolve Isnil_nil not_Isnil_cons. + +Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}. +Intro l; Case l;Auto. +(* +Realizer (fun l => match l with + | nil => true + | _ => false + end). +*) +Qed. + +(************************) +(** The Uncons function *) +(************************) + +Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}. +Intro l; Case l. +Auto. +Intros a m; Intros; Left; Exists a; Exists m; Reflexivity. +(* +Realizer (fun l => match l with + | nil => error + | (cons a m) => value (a,m) + end). +*) +Qed. + +(********************************) +(** The head function *) +(********************************) + +Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}. +Intro l; Case l. +Auto. +Intros a m; Intros; Left; Exists a; Exists m; Reflexivity. +(* +Realizer (fun l => match l with + | nil => error + | (cons a m) => value a + end). +*) +Qed. + +Lemma Tl : (l:(list A)){m:(list A)| (EX a:A |(cons a m)=l) + \/ ((Isnil l) /\ (Isnil m)) }. +Intro l; Case l. +Exists (nil A); Auto. +Intros a m; Intros; Exists m; Left; Exists a; Reflexivity. +(* +Realizer (fun l => match l with + | nil => nil + | (cons a m) => m + end). +*) +Qed. + +(****************************************) +(** Length of lists *) +(****************************************) + +(* length is defined in List *) +Fixpoint Length_l [l:(list A)] : nat -> nat + := [n:nat] Cases l of + nil => n + | (cons _ m) => (Length_l m (S n)) + end. + +(* A tail recursive version *) +Lemma Length_l_pf : (l:(list A))(n:nat){m:nat|(plus n (length l))=m}. +NewInduction l as [|a m lrec]. +Intro n; Exists n; Simpl; Auto. +Intro n; Elim (lrec (S n)); Simpl; Intros. +Exists x; Transitivity (S (plus n (length m))); Auto. +(* +Realizer Length_l. +*) +Qed. + +Lemma Length : (l:(list A)){m:nat|(length l)=m}. +Intro l. Apply (Length_l_pf l O). +(* +Realizer (fun l -> Length_l_pf l O). +*) +Qed. + +(*******************************) +(** Members of lists *) +(*******************************) +Inductive In_spec [a:A] : (list A) -> Prop := + | in_hd : (l:(list A))(In_spec a (cons a l)) + | in_tl : (l:(list A))(b:A)(In a l)->(In_spec a (cons b l)). +Hints Resolve in_hd in_tl. +Hints Unfold In. +Hints Resolve in_cons. + +Theorem In_In_spec : (a:A)(l:(list A))(In a l) <-> (In_spec a l). +Split. +Elim l; [ Intros; Contradiction + | Intros; Elim H0; + [ Intros; Rewrite H1; Auto + | Auto ]]. +Intros; Elim H; Auto. +Qed. + +Inductive AllS [P:A->Prop] : (list A) -> Prop + := allS_nil : (AllS P (nil A)) + | allS_cons : (a:A)(l:(list A))(P a)->(AllS P l)->(AllS P (cons a l)). +Hints Resolve allS_nil allS_cons. + +Hypothesis eqA_dec : (a,b:A){a=b}+{~a=b}. + +Fixpoint mem [a:A; l:(list A)] : bool := + Cases l of + nil => false + | (cons b m) => if (eqA_dec a b) then [H]true else [H](mem a m) + end. + +Hints Unfold In. +Lemma Mem : (a:A)(l:(list A)){(In a l)}+{(AllS [b:A]~b=a l)}. +Intros a l. +NewInduction l. +Auto. +Elim (eqA_dec a a0). +Auto. +Simpl. Elim IHl; Auto. +(* +Realizer mem. +*) +Qed. + +(*********************************) +(** Index of elements *) +(*********************************) + +Require Le. +Require Lt. + +Inductive nth_spec : (list A)->nat->A->Prop := + nth_spec_O : (a:A)(l:(list A))(nth_spec (cons a l) (S O) a) +| nth_spec_S : (n:nat)(a,b:A)(l:(list A)) + (nth_spec l n a)->(nth_spec (cons b l) (S n) a). +Hints Resolve nth_spec_O nth_spec_S. + +Inductive fst_nth_spec : (list A)->nat->A->Prop := + fst_nth_O : (a:A)(l:(list A))(fst_nth_spec (cons a l) (S O) a) +| fst_nth_S : (n:nat)(a,b:A)(l:(list A))(~a=b)-> + (fst_nth_spec l n a)->(fst_nth_spec (cons b l) (S n) a). +Hints Resolve fst_nth_O fst_nth_S. + +Lemma fst_nth_nth : (l:(list A))(n:nat)(a:A)(fst_nth_spec l n a)->(nth_spec l n a). +NewInduction 1; Auto. +Qed. +Hints Immediate fst_nth_nth. + +Lemma nth_lt_O : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(lt O n). +NewInduction 1; Auto. +Qed. + +Lemma nth_le_length : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)). +NewInduction 1; Simpl; Auto with arith. +Qed. + +Fixpoint Nth_func [l:(list A)] : nat -> (Exc A) + := [n:nat] Cases l n of + (cons a _) (S O) => (value A a) + | (cons _ l') (S (S p)) => (Nth_func l' (S p)) + | _ _ => Error + end. + +Lemma Nth : (l:(list A))(n:nat) + {a:A|(nth_spec l n a)}+{(n=O)\/(lt (length l) n)}. +NewInduction l as [|a l IHl]. +Intro n; Case n; Simpl; Auto with arith. +Intro n; NewDestruct n as [|[|n1]]; Simpl; Auto. +Left; Exists a; Auto. +NewDestruct (IHl (S n1)) as [[b]|o]. +Left; Exists b; Auto. +Right; NewDestruct o. +Absurd (S n1)=O; Auto. +Auto with arith. +(* +Realizer Nth_func. +*) +Qed. + +Lemma Item : (l:(list A))(n:nat){a:A|(nth_spec l (S n) a)}+{(le (length l) n)}. +Intros l n; Case (Nth l (S n)); Intro. +Case s; Intro a; Left; Exists a; Auto. +Right; Case o; Intro. +Absurd (S n)=O; Auto. +Auto with arith. +Qed. + +Require Minus. +Require DecBool. + +Fixpoint index_p [a:A;l:(list A)] : nat -> (Exc nat) := + Cases l of nil => [p]Error + | (cons b m) => [p](ifdec (eqA_dec a b) (Value p) (index_p a m (S p))) + end. + +Lemma Index_p : (a:A)(l:(list A))(p:nat) + {n:nat|(fst_nth_spec l (minus (S n) p) a)}+{(AllS [b:A]~a=b l)}. +NewInduction l as [|b m irec]. +Auto. +Intro p. +NewDestruct (eqA_dec a b) as [e|e]. +Left; Exists p. +NewDestruct e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith. +NewDestruct (irec (S p)) as [[n H]|]. +Left; Exists n; Auto with arith. +Elim minus_Sn_m; Auto with arith. +Apply lt_le_weak; Apply lt_O_minus_lt; Apply nth_lt_O with m a; Auto with arith. +Auto. +Qed. + +Lemma Index : (a:A)(l:(list A)) + {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}. + +Intros a l; Case (Index_p a l (S O)); Auto. +Intros (n,P); Left; Exists n; Auto. +Rewrite (minus_n_O n); Trivial. +(* +Realizer (fun a l -> Index_p a l (S O)). +*) +Qed. + +Section Find_sec. +Variable R,P : A -> Prop. + +Inductive InR : (list A) -> Prop + := inR_hd : (a:A)(l:(list A))(R a)->(InR (cons a l)) + | inR_tl : (a:A)(l:(list A))(InR l)->(InR (cons a l)). +Hints Resolve inR_hd inR_tl. + +Definition InR_inv := + [l:(list A)]Cases l of + nil => False + | (cons b m) => (R b)\/(InR m) + end. + +Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l). +NewInduction 1; Simpl; Auto. +Qed. + +Lemma InR_cons_inv : (a:A)(l:(list A))(InR (cons a l))->((R a)\/(InR l)). +Intros a l H; Exact (InR_INV H). +Qed. + +Lemma InR_or_app : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)). +Intros l m [|]. +NewInduction 1; Simpl; Auto. +Intro. NewInduction l; Simpl; Auto. +Qed. + +Lemma InR_app_or : (l,m:(list A))(InR (app l m))->((InR l)\/(InR m)). +Intros l m; Elim l; Simpl; Auto. +Intros b l' Hrec IAc; Elim (InR_cons_inv IAc);Auto. +Intros; Elim Hrec; Auto. +Qed. + +Hypothesis RS_dec : (a:A){(R a)}+{(P a)}. + +Fixpoint find [l:(list A)] : (Exc A) := + Cases l of nil => Error + | (cons a m) => (ifdec (RS_dec a) (Value a) (find m)) + end. + +Lemma Find : (l:(list A)){a:A | (In a l) & (R a)}+{(AllS P l)}. +NewInduction l as [|a m [[b H1 H2]|H]]; Auto. +Left; Exists b; Auto. +NewDestruct (RS_dec a). +Left; Exists a; Auto. +Auto. +(* +Realizer find. +*) +Qed. + +Variable B : Set. +Variable T : A -> B -> Prop. + +Variable TS_dec : (a:A){c:B| (T a c)}+{(P a)}. + +Fixpoint try_find [l:(list A)] : (Exc B) := + Cases l of + nil => Error + | (cons a l1) => + Cases (TS_dec a) of + (inleft (exist c _)) => (Value c) + | (inright _) => (try_find l1) + end + end. + +Lemma Try_find : (l:(list A)){c:B|(EX a:A |(In a l) & (T a c))}+{(AllS P l)}. +NewInduction l as [|a m [[b H1]|H]]. +Auto. +Left; Exists b; NewDestruct H1 as [a' H2 H3]; Exists a'; Auto. +NewDestruct (TS_dec a) as [[c H1]|]. +Left; Exists c. +Exists a; Auto. +Auto. +(* +Realizer try_find. +*) +Qed. + +End Find_sec. + +Section Assoc_sec. + +Variable B : Set. +Fixpoint assoc [a:A;l:(list A*B)] : (Exc B) := + Cases l of nil => Error + | (cons (a',b) m) => (ifdec (eqA_dec a a') (Value b) (assoc a m)) + end. + +Inductive AllS_assoc [P:A -> Prop]: (list A*B) -> Prop := + allS_assoc_nil : (AllS_assoc P (nil A*B)) + | allS_assoc_cons : (a:A)(b:B)(l:(list A*B)) + (P a)->(AllS_assoc P l)->(AllS_assoc P (cons (a,b) l)). + +Hints Resolve allS_assoc_nil allS_assoc_cons. + +(* The specification seems too weak: it is enough to return b if the + list has at least an element (a,b); probably the intention is to have + the specification + + (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}. +*) + +Lemma Assoc : (a:A)(l:(list A*B))(B+{(AllS_assoc [a':A]~(a=a') l)}). +NewInduction l as [|[a' b] m assrec]. Auto. +NewDestruct (eqA_dec a a'). +Left; Exact b. +NewDestruct assrec as [b'|]. +Left; Exact b'. +Right; Auto. +(* +Realizer assoc. +*) +Qed. + +End Assoc_sec. + +End Lists. + +Hints Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons + : datatypes. +Hints Immediate fst_nth_nth : datatypes. + |