diff options
Diffstat (limited to 'theories/Lists/TheoryList.v')
| -rwxr-xr-x | theories/Lists/TheoryList.v | 445 |
1 files changed, 231 insertions, 214 deletions
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index c7abe31da9..da23394c0a 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -10,32 +10,32 @@ (** Some programs and results about lists following CAML Manual *) -Require Export PolyList. +Require Export List. Set Implicit Arguments. -Chapter Lists. +Section Lists. -Variable A : Set. +Variable A : Set. (**********************) (** The null function *) (**********************) -Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l. +Definition Isnil (l:list A) : Prop := nil = l. -Lemma Isnil_nil : (Isnil (nil A)). -Red; Auto. +Lemma Isnil_nil : Isnil nil. +red in |- *; auto. Qed. -Hints Resolve Isnil_nil. +Hint Resolve Isnil_nil. -Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)). -Unfold Isnil. -Intros; Discriminate. +Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). +unfold Isnil in |- *. +intros; discriminate. Qed. -Hints Resolve Isnil_nil not_Isnil_cons. +Hint Resolve Isnil_nil not_Isnil_cons. -Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}. -Intro l; Case l;Auto. +Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}. +intro l; case l; auto. (* Realizer (fun l => match l with | nil => true @@ -48,10 +48,11 @@ 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. +Lemma Uncons : + forall l:list A, {a : A & {m : list A | 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 @@ -64,10 +65,11 @@ 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. +Lemma Hd : + forall l:list A, {a : A | exists m : list A | 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 @@ -76,11 +78,12 @@ Realizer (fun l => match l with *) 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. +Lemma Tl : + forall l:list A, + {m : list A | ( exists a : A | a :: m = l) \/ Isnil l /\ Isnil m}. +intro l; case l. +exists (nil (A:=A)); auto. +intros a m; intros; exists m; left; exists a; reflexivity. (* Realizer (fun l => match l with | nil => nil @@ -94,25 +97,25 @@ Qed. (****************************************) (* 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. +Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat := + match l with + | nil => n + | _ :: 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. +Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}. +induction l as [| a m lrec]. +intro n; exists n; simpl in |- *; auto. +intro n; elim (lrec (S n)); simpl in |- *; intros. +exists x; transitivity (S (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). +Lemma Length : forall l:list A, {m : nat | length l = m}. +intro l. apply (Length_l_pf l 0). (* Realizer (fun l -> Length_l_pf l O). *) @@ -121,43 +124,42 @@ 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. +Inductive In_spec (a:A) : list A -> Prop := + | in_hd : forall l:list A, In_spec a (a :: l) + | in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l). +Hint Resolve in_hd in_tl. +Hint Unfold In. +Hint Resolve in_cons. + +Theorem In_In_spec : forall (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. +Inductive AllS (P:A -> Prop) : list A -> Prop := + | allS_nil : AllS P nil + | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l). +Hint Resolve allS_nil allS_cons. -Hypothesis eqA_dec : (a,b:A){a=b}+{~a=b}. +Hypothesis eqA_dec : forall 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) +Fixpoint mem (a:A) (l:list A) {struct l} : bool := + match l with + | nil => false + | b :: m => if eqA_dec a b then fun H => true else fun 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. +Hint Unfold In. +Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}. +intros a l. +induction l. +auto. +elim (eqA_dec a a0). +auto. +simpl in |- *. elim IHl; auto. (* Realizer mem. *) @@ -167,146 +169,157 @@ 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. +Require Import Le. +Require Import Lt. + +Inductive nth_spec : list A -> nat -> A -> Prop := + | nth_spec_O : forall (a:A) (l:list A), nth_spec (a :: l) 1 a + | nth_spec_S : + forall (n:nat) (a b:A) (l:list A), + nth_spec l n a -> nth_spec (b :: l) (S n) a. +Hint Resolve nth_spec_O nth_spec_S. + +Inductive fst_nth_spec : list A -> nat -> A -> Prop := + | fst_nth_O : forall (a:A) (l:list A), fst_nth_spec (a :: l) 1 a + | fst_nth_S : + forall (n:nat) (a b:A) (l:list A), + a <> b -> fst_nth_spec l n a -> fst_nth_spec (b :: l) (S n) a. +Hint Resolve fst_nth_O fst_nth_S. + +Lemma fst_nth_nth : + forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a. +induction 1; auto. Qed. -Hints Immediate fst_nth_nth. +Hint 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. +Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n. +induction 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. +Lemma nth_le_length : + forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l. +induction 1; simpl in |- *; 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. +Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A := + match l, n with + | a :: _, S O => value a + | _ :: l', S (S p) => Nth_func l' (S p) + | _, _ => error + end. + +Lemma Nth : + forall (l:list A) (n:nat), + {a : A | nth_spec l n a} + {n = 0 \/ length l < n}. +induction l as [| a l IHl]. +intro n; case n; simpl in |- *; auto with arith. +intro n; destruct n as [| [| n1]]; simpl in |- *; auto. +left; exists a; auto. +destruct (IHl (S n1)) as [[b]| o]. +left; exists b; auto. +right; destruct o. +absurd (S n1 = 0); 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. +Lemma Item : + forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {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 = 0); 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. +Require Import Minus. +Require Import DecBool. + +Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat := + match l with + | nil => fun p => error + | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p)) + end. + +Lemma Index_p : + forall (a:A) (l:list A) (p:nat), + {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}. +induction l as [| b m irec]. +auto. +intro p. +destruct (eqA_dec a b) as [e| e]. +left; exists p. +destruct e; elim minus_Sn_m; trivial; elim minus_n_n; auto with arith. +destruct (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)}. +Lemma Index : + forall (a:A) (l:list A), + {n : nat | fst_nth_spec l n a} + {AllS (fun 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. +intros a l; case (Index_p a l 1); 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. +Variables 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. +Inductive InR : list A -> Prop := + | inR_hd : forall (a:A) (l:list A), R a -> InR (a :: l) + | inR_tl : forall (a:A) (l:list A), InR l -> InR (a :: l). +Hint Resolve inR_hd inR_tl. -Definition InR_inv := - [l:(list A)]Cases l of - nil => False - | (cons b m) => (R b)\/(InR m) - end. +Definition InR_inv (l:list A) := + match l with + | nil => False + | b :: m => R b \/ InR m + end. -Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l). -NewInduction 1; Simpl; Auto. +Lemma InR_INV : forall l:list A, InR l -> InR_inv l. +induction 1; simpl in |- *; 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). +Lemma InR_cons_inv : forall (a:A) (l:list A), InR (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. +Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m). +intros l m [| ]. +induction 1; simpl in |- *; auto. +intro. induction l; simpl in |- *; 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. +Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m. +intros l m; elim l; simpl in |- *; 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)}. +Hypothesis RS_dec : forall 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. +Fixpoint find (l:list A) : Exc A := + match l with + | nil => error + | 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. +Lemma Find : forall l:list A, {a : A | In a l & R a} + {AllS P l}. +induction l as [| a m [[b H1 H2]| H]]; auto. +left; exists b; auto. +destruct (RS_dec a). +left; exists a; auto. +auto. (* Realizer find. *) @@ -315,26 +328,27 @@ 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. +Variable TS_dec : forall a:A, {c : B | T a c} + {P a}. + +Fixpoint try_find (l:list A) : Exc B := + match l with + | nil => error + | a :: l1 => + match TS_dec a with + | inleft (exist c _) => value c + | inright _ => try_find l1 + end + end. + +Lemma Try_find : + forall l:list A, {c : B | exists2 a : A | In a l & T a c} + {AllS P l}. +induction l as [| a m [[b H1]| H]]. +auto. +left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto. +destruct (TS_dec a) as [[c H1]| ]. +left; exists c. +exists a; auto. +auto. (* Realizer try_find. *) @@ -345,17 +359,20 @@ 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. +Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : + Exc B := + match l with + | nil => error + | (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)). +Inductive AllS_assoc (P:A -> Prop) : list (A * B) -> Prop := + | allS_assoc_nil : AllS_assoc P nil + | allS_assoc_cons : + forall (a:A) (b:B) (l:list (A * B)), + P a -> AllS_assoc P l -> AllS_assoc P ((a, b) :: l). -Hints Resolve allS_assoc_nil allS_assoc_cons. +Hint 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 @@ -364,13 +381,14 @@ Hints Resolve allS_assoc_nil allS_assoc_cons. (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. +Lemma Assoc : + forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}. +induction l as [| [a' b] m assrec]. auto. +destruct (eqA_dec a a'). +left; exact b. +destruct assrec as [b'| ]. +left; exact b'. +right; auto. (* Realizer assoc. *) @@ -380,7 +398,6 @@ 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. - +Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons: + datatypes. +Hint Immediate fst_nth_nth: datatypes. |