summaryrefslogtreecommitdiff
path: root/theories7/Lists/TheoryList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Lists/TheoryList.v')
-rwxr-xr-xtheories7/Lists/TheoryList.v386
1 files changed, 0 insertions, 386 deletions
diff --git a/theories7/Lists/TheoryList.v b/theories7/Lists/TheoryList.v
deleted file mode 100755
index f7adda70..00000000
--- a/theories7/Lists/TheoryList.v
+++ /dev/null
@@ -1,386 +0,0 @@
-(************************************************************************)
-(* 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.
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 13:44:03 +0000