summaryrefslogtreecommitdiff
path: root/theories7/Lists
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Lists')
-rwxr-xr-xtheories7/Lists/List.v261
-rw-r--r--theories7/Lists/ListSet.v389
-rwxr-xr-xtheories7/Lists/MonoList.v259
-rw-r--r--theories7/Lists/PolyList.v646
-rw-r--r--theories7/Lists/PolyListSyntax.v10
-rwxr-xr-xtheories7/Lists/Streams.v170
-rwxr-xr-xtheories7/Lists/TheoryList.v386
7 files changed, 0 insertions, 2121 deletions
diff --git a/theories7/Lists/List.v b/theories7/Lists/List.v
deleted file mode 100755
index 574b2688..00000000
--- a/theories7/Lists/List.v
+++ /dev/null
@@ -1,261 +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: List.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
-
-(* This file is a copy of file MonoList.v *)
-
-(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
-
-Require Le.
-
-Parameter List_Dom:Set.
-Definition A := List_Dom.
-
-Inductive list : Set := nil : list | cons : A -> list -> list.
-
-Fixpoint app [l:list] : list -> list
- := [m:list]<list>Cases l of
- nil => m
- | (cons a l1) => (cons a (app l1 m))
- end.
-
-
-Lemma app_nil_end : (l:list)(l=(app l nil)).
-Proof.
- Intro l ; Elim l ; Simpl ; Auto.
- Induction 1; Auto.
-Qed.
-Hints Resolve app_nil_end : list v62.
-
-Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)).
-Proof.
- Intros l m n ; Elim l ; Simpl ; Auto with list.
- Induction 1; Auto with list.
-Qed.
-Hints Resolve app_ass : list v62.
-
-Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n).
-Proof.
- Auto with list.
-Qed.
-Hints Resolve ass_app : list v62.
-
-Definition tail :=
- [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list.
-
-
-Lemma nil_cons : (a:A)(m:list)~nil=(cons a m).
- Intros; Discriminate.
-Qed.
-
-(****************************************)
-(* Length of lists *)
-(****************************************)
-
-Fixpoint length [l:list] : nat
- := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end.
-
-(******************************)
-(* Length order of lists *)
-(******************************)
-
-Section length_order.
-Definition lel := [l,m:list](le (length l) (length m)).
-
-Hints Unfold lel : list.
-
-Variables a,b:A.
-Variables l,m,n:list.
-
-Lemma lel_refl : (lel l l).
-Proof.
- Unfold lel ; Auto with list.
-Qed.
-
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
-Proof.
- Unfold lel ; Intros.
- Apply le_trans with (length m) ; Auto with list.
-Qed.
-
-Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
-Proof.
- Intro l' ; Elim l' ; Auto with list arith.
- Intros a' y H H0.
- (* <list>nil=(cons a' y)
- ============================
- H0 : (lel (cons a' y) nil)
- H : (lel y nil)->(<list>nil=y)
- y : list
- a' : A
- l' : list *)
- Absurd (le (S (length y)) O); Auto with list arith.
-Qed.
-End length_order.
-
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62.
-
-Fixpoint In [a:A;l:list] : Prop :=
- Cases l of
- nil => False
- | (cons b m) => (b=a)\/(In a m)
- end.
-
-Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
-Proof.
- Simpl ; Auto with list.
-Qed.
-Hints Resolve in_eq : list v62.
-
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
-Proof.
- Simpl ; Auto with list.
-Qed.
-Hints Resolve in_cons : list v62.
-
-Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Auto with list.
- Intros a0 y H H0.
- (* ((<A>a0=a)\/(In a y))\/(In a m)
- ============================
- H0 : (<A>a0=a)\/(In a (app y m))
- H : (In a (app y m))->((In a y)\/(In a m))
- y : list
- a0 : A
- a : A
- m : list
- l : list *)
- Elim H0 ; Auto with list.
- Intro H1.
- (* ((<A>a0=a)\/(In a y))\/(In a m)
- ============================
- H1 : (In a (app y m)) *)
- Elim (H H1) ; Auto with list.
-Qed.
-Hints Immediate in_app_or : list v62.
-
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Intro H.
- (* 1 (In a m)
- ============================
- H : False\/(In a m)
- a : A
- m : list
- l : list *)
- Elim H ; Auto with list ; Intro H0.
- (* (In a m)
- ============================
- H0 : False *)
- Elim H0. (* subProof completed *)
- Intros y H0 H1.
- (* 2 (<A>H=a)\/(In a (app y m))
- ============================
- H1 : ((<A>H=a)\/(In a y))\/(In a m)
- H0 : ((In a y)\/(In a m))->(In a (app y m))
- y : list *)
- Elim H1 ; Auto 4 with list.
- Intro H2.
- (* (<A>H=a)\/(In a (app y m))
- ============================
- H2 : (<A>H=a)\/(In a y) *)
- Elim H2 ; Auto with list.
-Qed.
-Hints Resolve in_or_app : list v62.
-
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
-
-Hints Unfold incl : list v62.
-
-Lemma incl_refl : (l:list)(incl l l).
-Proof.
- Auto with list.
-Qed.
-Hints Resolve incl_refl : list v62.
-
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_tl : list v62.
-
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
-Proof.
- Auto with list.
-Qed.
-
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_appl : list v62.
-
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_appr : list v62.
-
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
-Proof.
- Unfold incl ; Simpl ; Intros a l m H H0 a0 H1.
- (* (In a0 m)
- ============================
- H1 : (<A>a=a0)\/(In a0 l)
- a0 : A
- H0 : (a:A)(In a l)->(In a m)
- H : (In a m)
- m : list
- l : list
- a : A *)
- Elim H1.
- (* 1 (<A>a=a0)->(In a0 m) *)
- Elim H1 ; Auto with list ; Intro H2.
- (* (<A>a=a0)->(In a0 m)
- ============================
- H2 : <A>a=a0 *)
- Elim H2 ; Auto with list. (* solves subgoal *)
- (* 2 (In a0 l)->(In a0 m) *)
- Auto with list.
-Qed.
-Hints Resolve incl_cons : list v62.
-
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
-Proof.
- Unfold incl ; Simpl ; Intros l m n H H0 a H1.
- (* (In a n)
- ============================
- H1 : (In a (app l m))
- a : A
- H0 : (a:A)(In a m)->(In a n)
- H : (a:A)(In a l)->(In a n)
- n : list
- m : list
- l : list *)
- Elim (in_app_or l m a) ; Auto with list.
-Qed.
-Hints Resolve incl_app : list v62.
diff --git a/theories7/Lists/ListSet.v b/theories7/Lists/ListSet.v
deleted file mode 100644
index 9bf259da..00000000
--- a/theories7/Lists/ListSet.v
+++ /dev/null
@@ -1,389 +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: ListSet.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
-
-(** A Library for finite sets, implemented as lists
- A Library with similar interface will soon be available under
- the name TreeSet in the theories/Trees directory *)
-
-(** PolyList is loaded, but not exported.
- This allow to "hide" the definitions, functions and theorems of PolyList
- and to see only the ones of ListSet *)
-
-Require PolyList.
-
-Set Implicit Arguments.
-V7only [Implicits nil [1].].
-
-Section first_definitions.
-
- Variable A : Set.
- Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}.
-
- Definition set := (list A).
-
- Definition empty_set := (!nil ?) : set.
-
- Fixpoint set_add [a:A; x:set] : set :=
- Cases x of
- | nil => (cons a nil)
- | (cons a1 x1) => Cases (Aeq_dec a a1) of
- | (left _) => (cons a1 x1)
- | (right _) => (cons a1 (set_add a x1))
- end
- end.
-
-
- Fixpoint set_mem [a:A; x:set] : bool :=
- Cases x of
- | nil => false
- | (cons a1 x1) => Cases (Aeq_dec a a1) of
- | (left _) => true
- | (right _) => (set_mem a x1)
- end
- end.
-
- (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
- Fixpoint set_remove [a:A; x:set] : set :=
- Cases x of
- | nil => empty_set
- | (cons a1 x1) => Cases (Aeq_dec a a1) of
- | (left _) => x1
- | (right _) => (cons a1 (set_remove a x1))
- end
- end.
-
- Fixpoint set_inter [x:set] : set -> set :=
- Cases x of
- | nil => [y]nil
- | (cons a1 x1) => [y]if (set_mem a1 y)
- then (cons a1 (set_inter x1 y))
- else (set_inter x1 y)
- end.
-
- Fixpoint set_union [x,y:set] : set :=
- Cases y of
- | nil => x
- | (cons a1 y1) => (set_add a1 (set_union x y1))
- end.
-
- (** returns the set of all els of [x] that does not belong to [y] *)
- Fixpoint set_diff [x:set] : set -> set :=
- [y]Cases x of
- | nil => nil
- | (cons a1 x1) => if (set_mem a1 y)
- then (set_diff x1 y)
- else (set_add a1 (set_diff x1 y))
- end.
-
-
- Definition set_In : A -> set -> Prop := (In 1!A).
-
- Lemma set_In_dec : (a:A; x:set){(set_In a x)}+{~(set_In a x)}.
-
- Proof.
- Unfold set_In.
- (*** Realizer set_mem. Program_all. ***)
- Induction x.
- Auto.
- Intros a0 x0 Ha0. Case (Aeq_dec a a0); Intro eq.
- Rewrite eq; Simpl; Auto with datatypes.
- Elim Ha0.
- Auto with datatypes.
- Right; Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes.
- Qed.
-
- Lemma set_mem_ind :
- (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set)
- ((set_In a x) -> (P y))
- ->(P z)
- ->(P (if (set_mem a x) then y else z)).
-
- Proof.
- Induction x; Simpl; Intros.
- Assumption.
- Elim (Aeq_dec a a0); Auto with datatypes.
- Qed.
-
- Lemma set_mem_ind2 :
- (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set)
- ((set_In a x) -> (P y))
- ->(~(set_In a x) -> (P z))
- ->(P (if (set_mem a x) then y else z)).
-
- Proof.
- Induction x; Simpl; Intros.
- Apply H0; Red; Trivial.
- Case (Aeq_dec a a0); Auto with datatypes.
- Intro; Apply H; Intros; Auto.
- Apply H1; Red; Intro.
- Case H3; Auto.
- Qed.
-
-
- Lemma set_mem_correct1 :
- (a:A)(x:set)(set_mem a x)=true -> (set_In a x).
- Proof.
- Induction x; Simpl.
- Discriminate.
- Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
- Qed.
-
- Lemma set_mem_correct2 :
- (a:A)(x:set)(set_In a x) -> (set_mem a x)=true.
- Proof.
- Induction x; Simpl.
- Intro Ha; Elim Ha.
- Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
- Intros H1 H2 [H3 | H4].
- Absurd a0=a; Auto with datatypes.
- Auto with datatypes.
- Qed.
-
- Lemma set_mem_complete1 :
- (a:A)(x:set)(set_mem a x)=false -> ~(set_In a x).
- Proof.
- Induction x; Simpl.
- Tauto.
- Intros a0 l; Elim (Aeq_dec a a0).
- Intros; Discriminate H0.
- Unfold not; Intros; Elim H1; Auto with datatypes.
- Qed.
-
- Lemma set_mem_complete2 :
- (a:A)(x:set)~(set_In a x) -> (set_mem a x)=false.
- Proof.
- Induction x; Simpl.
- Tauto.
- Intros a0 l; Elim (Aeq_dec a a0).
- Intros; Elim H0; Auto with datatypes.
- Tauto.
- Qed.
-
- Lemma set_add_intro1 : (a,b:A)(x:set)
- (set_In a x) -> (set_In a (set_add b x)).
-
- Proof.
- Unfold set_In; Induction x; Simpl.
- Auto with datatypes.
- Intros a0 l H [ Ha0a | Hal ].
- Elim (Aeq_dec b a0); Left; Assumption.
- Elim (Aeq_dec b a0); Right; [ Assumption | Auto with datatypes ].
- Qed.
-
- Lemma set_add_intro2 : (a,b:A)(x:set)
- a=b -> (set_In a (set_add b x)).
-
- Proof.
- Unfold set_In; Induction x; Simpl.
- Auto with datatypes.
- Intros a0 l H Hab.
- Elim (Aeq_dec b a0);
- [ Rewrite Hab; Intro Hba0; Rewrite Hba0; Simpl; Auto with datatypes
- | Auto with datatypes ].
- Qed.
-
- Hints Resolve set_add_intro1 set_add_intro2.
-
- Lemma set_add_intro : (a,b:A)(x:set)
- a=b\/(set_In a x) -> (set_In a (set_add b x)).
-
- Proof.
- Intros a b x [H1 | H2] ; Auto with datatypes.
- Qed.
-
- Lemma set_add_elim : (a,b:A)(x:set)
- (set_In a (set_add b x)) -> a=b\/(set_In a x).
-
- Proof.
- Unfold set_In.
- Induction x.
- Simpl; Intros [H1|H2]; Auto with datatypes.
- Simpl; Do 3 Intro.
- Elim (Aeq_dec b a0).
- Simpl; Tauto.
- Simpl; Intros; Elim H0.
- Trivial with datatypes.
- Tauto.
- Tauto.
- Qed.
-
- Lemma set_add_elim2 : (a,b:A)(x:set)
- (set_In a (set_add b x)) -> ~(a=b) -> (set_In a x).
- Intros a b x H; Case (set_add_elim H); Intros; Trivial.
- Case H1; Trivial.
- Qed.
-
- Hints Resolve set_add_intro set_add_elim set_add_elim2.
-
- Lemma set_add_not_empty : (a:A)(x:set)~(set_add a x)=empty_set.
- Proof.
- Induction x; Simpl.
- Discriminate.
- Intros; Elim (Aeq_dec a a0); Intros; Discriminate.
- Qed.
-
-
- Lemma set_union_intro1 : (a:A)(x,y:set)
- (set_In a x) -> (set_In a (set_union x y)).
- Proof.
- Induction y; Simpl; Auto with datatypes.
- Qed.
-
- Lemma set_union_intro2 : (a:A)(x,y:set)
- (set_In a y) -> (set_In a (set_union x y)).
- Proof.
- Induction y; Simpl.
- Tauto.
- Intros; Elim H0; Auto with datatypes.
- Qed.
-
- Hints Resolve set_union_intro2 set_union_intro1.
-
- Lemma set_union_intro : (a:A)(x,y:set)
- (set_In a x)\/(set_In a y) -> (set_In a (set_union x y)).
- Proof.
- Intros; Elim H; Auto with datatypes.
- Qed.
-
- Lemma set_union_elim : (a:A)(x,y:set)
- (set_In a (set_union x y)) -> (set_In a x)\/(set_In a y).
- Proof.
- Induction y; Simpl.
- Auto with datatypes.
- Intros.
- Generalize (set_add_elim H0).
- Intros [H1 | H1].
- Auto with datatypes.
- Tauto.
- Qed.
-
- Lemma set_union_emptyL : (a:A)(x:set)(set_In a (set_union empty_set x)) -> (set_In a x).
- Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction.
- Qed.
-
-
- Lemma set_union_emptyR : (a:A)(x:set)(set_In a (set_union x empty_set)) -> (set_In a x).
- Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction.
- Qed.
-
-
- Lemma set_inter_intro : (a:A)(x,y:set)
- (set_In a x) -> (set_In a y) -> (set_In a (set_inter x y)).
- Proof.
- Induction x.
- Auto with datatypes.
- Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hy.
- Simpl; Rewrite Ha0a.
- Generalize (!set_mem_correct1 a y).
- Generalize (!set_mem_complete1 a y).
- Elim (set_mem a y); Simpl; Intros.
- Auto with datatypes.
- Absurd (set_In a y); Auto with datatypes.
- Elim (set_mem a0 y); [ Right; Auto with datatypes | Auto with datatypes].
- Qed.
-
- Lemma set_inter_elim1 : (a:A)(x,y:set)
- (set_In a (set_inter x y)) -> (set_In a x).
- Proof.
- Induction x.
- Auto with datatypes.
- Simpl; Intros a0 l Hrec y.
- Generalize (!set_mem_correct1 a0 y).
- Elim (set_mem a0 y); Simpl; Intros.
- Elim H0; EAuto with datatypes.
- EAuto with datatypes.
- Qed.
-
- Lemma set_inter_elim2 : (a:A)(x,y:set)
- (set_In a (set_inter x y)) -> (set_In a y).
- Proof.
- Induction x.
- Simpl; Tauto.
- Simpl; Intros a0 l Hrec y.
- Generalize (!set_mem_correct1 a0 y).
- Elim (set_mem a0 y); Simpl; Intros.
- Elim H0; [ Intro Hr; Rewrite <- Hr; EAuto with datatypes | EAuto with datatypes ] .
- EAuto with datatypes.
- Qed.
-
- Hints Resolve set_inter_elim1 set_inter_elim2.
-
- Lemma set_inter_elim : (a:A)(x,y:set)
- (set_In a (set_inter x y)) -> (set_In a x)/\(set_In a y).
- Proof.
- EAuto with datatypes.
- Qed.
-
- Lemma set_diff_intro : (a:A)(x,y:set)
- (set_In a x) -> ~(set_In a y) -> (set_In a (set_diff x y)).
- Proof.
- Induction x.
- Simpl; Tauto.
- Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hay.
- Rewrite Ha0a; Generalize (set_mem_complete2 Hay).
- Elim (set_mem a y); [ Intro Habs; Discriminate Habs | Auto with datatypes ].
- Elim (set_mem a0 y); Auto with datatypes.
- Qed.
-
- Lemma set_diff_elim1 : (a:A)(x,y:set)
- (set_In a (set_diff x y)) -> (set_In a x).
- Proof.
- Induction x.
- Simpl; Tauto.
- Simpl; Intros a0 l Hrec y; Elim (set_mem a0 y).
- EAuto with datatypes.
- Intro; Generalize (set_add_elim H).
- Intros [H1 | H2]; EAuto with datatypes.
- Qed.
-
- Lemma set_diff_elim2 : (a:A)(x,y:set)
- (set_In a (set_diff x y)) -> ~(set_In a y).
- Intros a x y; Elim x; Simpl.
- Intros; Contradiction.
- Intros a0 l Hrec.
- Apply set_mem_ind2; Auto.
- Intros H1 H2; Case (set_add_elim H2); Intros; Auto.
- Rewrite H; Trivial.
- Qed.
-
- Lemma set_diff_trivial : (a:A)(x:set)~(set_In a (set_diff x x)).
- Red; Intros a x H.
- Apply (set_diff_elim2 H).
- Apply (set_diff_elim1 H).
- Qed.
-
-Hints Resolve set_diff_intro set_diff_trivial.
-
-
-End first_definitions.
-
-Section other_definitions.
-
- Variables A,B : Set.
-
- Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B).
-
- (** [B^A], set of applications from [A] to [B] *)
- Definition set_power : (set A) -> (set B) -> (set (set A*B)) :=
- (list_power 1!A 2!B).
-
- Definition set_map : (A->B) -> (set A) -> (set B) := (map 1!A 2!B).
-
- Definition set_fold_left : (B -> A -> B) -> (set A) -> B -> B :=
- (fold_left 1!B 2!A).
-
- Definition set_fold_right : (A -> B -> B) -> (set A) -> B -> B :=
- [f][x][b](fold_right f b x).
-
-
-End other_definitions.
-
-V7only [Implicits nil [].].
-Unset Implicit Arguments.
diff --git a/theories7/Lists/MonoList.v b/theories7/Lists/MonoList.v
deleted file mode 100755
index 2ab78f7f..00000000
--- a/theories7/Lists/MonoList.v
+++ /dev/null
@@ -1,259 +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: MonoList.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
-
-(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
-
-Require Le.
-
-Parameter List_Dom:Set.
-Definition A := List_Dom.
-
-Inductive list : Set := nil : list | cons : A -> list -> list.
-
-Fixpoint app [l:list] : list -> list
- := [m:list]<list>Cases l of
- nil => m
- | (cons a l1) => (cons a (app l1 m))
- end.
-
-
-Lemma app_nil_end : (l:list)(l=(app l nil)).
-Proof.
- Intro l ; Elim l ; Simpl ; Auto.
- Induction 1; Auto.
-Qed.
-Hints Resolve app_nil_end : list v62.
-
-Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)).
-Proof.
- Intros l m n ; Elim l ; Simpl ; Auto with list.
- Induction 1; Auto with list.
-Qed.
-Hints Resolve app_ass : list v62.
-
-Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n).
-Proof.
- Auto with list.
-Qed.
-Hints Resolve ass_app : list v62.
-
-Definition tail :=
- [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list.
-
-
-Lemma nil_cons : (a:A)(m:list)~nil=(cons a m).
- Intros; Discriminate.
-Qed.
-
-(****************************************)
-(* Length of lists *)
-(****************************************)
-
-Fixpoint length [l:list] : nat
- := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end.
-
-(******************************)
-(* Length order of lists *)
-(******************************)
-
-Section length_order.
-Definition lel := [l,m:list](le (length l) (length m)).
-
-Hints Unfold lel : list.
-
-Variables a,b:A.
-Variables l,m,n:list.
-
-Lemma lel_refl : (lel l l).
-Proof.
- Unfold lel ; Auto with list.
-Qed.
-
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
-Proof.
- Unfold lel ; Intros.
- Apply le_trans with (length m) ; Auto with list.
-Qed.
-
-Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
-Proof.
- Unfold lel ; Simpl ; Auto with list arith.
-Qed.
-
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
-Proof.
- Intro l' ; Elim l' ; Auto with list arith.
- Intros a' y H H0.
- (* <list>nil=(cons a' y)
- ============================
- H0 : (lel (cons a' y) nil)
- H : (lel y nil)->(<list>nil=y)
- y : list
- a' : A
- l' : list *)
- Absurd (le (S (length y)) O); Auto with list arith.
-Qed.
-End length_order.
-
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62.
-
-Fixpoint In [a:A;l:list] : Prop :=
- Cases l of
- nil => False
- | (cons b m) => (b=a)\/(In a m)
- end.
-
-Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
-Proof.
- Simpl ; Auto with list.
-Qed.
-Hints Resolve in_eq : list v62.
-
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
-Proof.
- Simpl ; Auto with list.
-Qed.
-Hints Resolve in_cons : list v62.
-
-Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Auto with list.
- Intros a0 y H H0.
- (* ((<A>a0=a)\/(In a y))\/(In a m)
- ============================
- H0 : (<A>a0=a)\/(In a (app y m))
- H : (In a (app y m))->((In a y)\/(In a m))
- y : list
- a0 : A
- a : A
- m : list
- l : list *)
- Elim H0 ; Auto with list.
- Intro H1.
- (* ((<A>a0=a)\/(In a y))\/(In a m)
- ============================
- H1 : (In a (app y m)) *)
- Elim (H H1) ; Auto with list.
-Qed.
-Hints Immediate in_app_or : list v62.
-
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Intro H.
- (* 1 (In a m)
- ============================
- H : False\/(In a m)
- a : A
- m : list
- l : list *)
- Elim H ; Auto with list ; Intro H0.
- (* (In a m)
- ============================
- H0 : False *)
- Elim H0. (* subProof completed *)
- Intros y H0 H1.
- (* 2 (<A>H=a)\/(In a (app y m))
- ============================
- H1 : ((<A>H=a)\/(In a y))\/(In a m)
- H0 : ((In a y)\/(In a m))->(In a (app y m))
- y : list *)
- Elim H1 ; Auto 4 with list.
- Intro H2.
- (* (<A>H=a)\/(In a (app y m))
- ============================
- H2 : (<A>H=a)\/(In a y) *)
- Elim H2 ; Auto with list.
-Qed.
-Hints Resolve in_or_app : list v62.
-
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
-
-Hints Unfold incl : list v62.
-
-Lemma incl_refl : (l:list)(incl l l).
-Proof.
- Auto with list.
-Qed.
-Hints Resolve incl_refl : list v62.
-
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_tl : list v62.
-
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
-Proof.
- Auto with list.
-Qed.
-
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_appl : list v62.
-
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
-Proof.
- Auto with list.
-Qed.
-Hints Immediate incl_appr : list v62.
-
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
-Proof.
- Unfold incl ; Simpl ; Intros a l m H H0 a0 H1.
- (* (In a0 m)
- ============================
- H1 : (<A>a=a0)\/(In a0 l)
- a0 : A
- H0 : (a:A)(In a l)->(In a m)
- H : (In a m)
- m : list
- l : list
- a : A *)
- Elim H1.
- (* 1 (<A>a=a0)->(In a0 m) *)
- Elim H1 ; Auto with list ; Intro H2.
- (* (<A>a=a0)->(In a0 m)
- ============================
- H2 : <A>a=a0 *)
- Elim H2 ; Auto with list. (* solves subgoal *)
- (* 2 (In a0 l)->(In a0 m) *)
- Auto with list.
-Qed.
-Hints Resolve incl_cons : list v62.
-
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
-Proof.
- Unfold incl ; Simpl ; Intros l m n H H0 a H1.
- (* (In a n)
- ============================
- H1 : (In a (app l m))
- a : A
- H0 : (a:A)(In a m)->(In a n)
- H : (a:A)(In a l)->(In a n)
- n : list
- m : list
- l : list *)
- Elim (in_app_or l m a) ; Auto with list.
-Qed.
-Hints Resolve incl_app : list v62.
diff --git a/theories7/Lists/PolyList.v b/theories7/Lists/PolyList.v
deleted file mode 100644
index e69ecd10..00000000
--- a/theories7/Lists/PolyList.v
+++ /dev/null
@@ -1,646 +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: PolyList.v,v 1.2.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
-
-Require Le.
-
-
-Section Lists.
-
-Variable A : Set.
-
-Set Implicit Arguments.
-
-Inductive list : Set := nil : list | cons : A -> list -> list.
-
-Infix "::" cons (at level 7, right associativity) : list_scope
- V8only (at level 60, right associativity).
-
-Open Scope list_scope.
-
-(*************************)
-(** Discrimination *)
-(*************************)
-
-Lemma nil_cons : (a:A)(m:list)~(nil=(cons a m)).
-Proof.
- Intros; Discriminate.
-Qed.
-
-(*************************)
-(** Concatenation *)
-(*************************)
-
-Fixpoint app [l:list] : list -> list
- := [m:list]Cases l of
- nil => m
- | (cons a l1) => (cons a (app l1 m))
- end.
-
-Infix RIGHTA 7 "^" app : list_scope
- V8only RIGHTA 60 "++".
-
-Lemma app_nil_end : (l:list)l=(l^nil).
-Proof.
- NewInduction l ; Simpl ; Auto.
- Rewrite <- IHl; Auto.
-Qed.
-Hints Resolve app_nil_end.
-
-Tactic Definition now_show c := Change c.
-V7only [Tactic Definition NowShow := now_show.].
-
-Lemma app_ass : (l,m,n : list)((l^m)^ n)=(l^(m^n)).
-Proof.
- Intros. NewInduction l ; Simpl ; Auto.
- NowShow '(cons a (app (app l m) n))=(cons a (app l (app m n))).
- Rewrite <- IHl; Auto.
-Qed.
-Hints Resolve app_ass.
-
-Lemma ass_app : (l,m,n : list)(l^(m^n))=((l^m)^n).
-Proof.
- Auto.
-Qed.
-Hints Resolve ass_app.
-
-Lemma app_comm_cons : (x,y:list)(a:A) (cons a (x^y))=((cons a x)^y).
-Proof.
- Auto.
-Qed.
-
-Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil.
-Proof.
- NewDestruct x;NewDestruct y;Simpl;Auto.
- Intros H;Discriminate H.
- Intros;Discriminate H.
-Qed.
-
-Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)).
-Proof.
-Unfold not .
- NewDestruct x;Simpl;Intros.
- Discriminate H.
- Discriminate H.
-Qed.
-
-Lemma app_eq_unit:(x,y:list)(a:A)
- (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil.
-
-Proof.
- NewDestruct x;NewDestruct y;Simpl.
- Intros a H;Discriminate H.
- Left;Split;Auto.
- Right;Split;Auto.
- Generalize H .
- Generalize (app_nil_end l) ;Intros E.
- Rewrite <- E;Auto.
- Intros.
- Injection H.
- Intro.
- Cut nil=(l^(cons a0 l0));Auto.
- Intro.
- Generalize (app_cons_not_nil H1); Intro.
- Elim H2.
-Qed.
-
-Lemma app_inj_tail : (x,y:list)(a,b:A)
- (x^(cons a nil))=(y^(cons b nil)) -> x=y /\ a=b.
-Proof.
- NewInduction x as [|x l IHl];NewDestruct y;Simpl;Auto.
- Intros a b H.
- Injection H.
- Auto.
- Intros a0 b H.
- Injection H;Intros.
- Generalize (app_cons_not_nil H0) ;NewDestruct 1.
- Intros a b H.
- Injection H;Intros.
- Cut nil=(l^(cons a nil));Auto.
- Intro.
- Generalize (app_cons_not_nil H2) ;NewDestruct 1.
- Intros a0 b H.
- Injection H;Intros.
- NewDestruct (IHl l0 a0 b H0).
- Split;Auto.
- Rewrite <- H1;Rewrite <- H2;Reflexivity.
-Qed.
-
-(*************************)
-(** Head and tail *)
-(*************************)
-
-Definition head :=
- [l:list]Cases l of
- | nil => Error
- | (cons x _) => (Value x)
- end.
-
-Definition tail : list -> list :=
- [l:list]Cases l of
- | nil => nil
- | (cons a m) => m
- end.
-
-(****************************************)
-(** Length of lists *)
-(****************************************)
-
-Fixpoint length [l:list] : nat
- := Cases l of nil => O | (cons _ m) => (S (length m)) end.
-
-(******************************)
-(** Length order of lists *)
-(******************************)
-
-Section length_order.
-Definition lel := [l,m:list](le (length l) (length m)).
-
-Variables a,b:A.
-Variables l,m,n:list.
-
-Lemma lel_refl : (lel l l).
-Proof.
- Unfold lel ; Auto with arith.
-Qed.
-
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
-Proof.
- Unfold lel ; Intros.
- NowShow '(le (length l) (length n)).
- Apply le_trans with (length m) ; Auto with arith.
-Qed.
-
-Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
-Proof.
- Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
-Proof.
- Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
-Proof.
- Intro l' ; Elim l' ; Auto with arith.
- Intros a' y H H0.
- NowShow 'nil=(cons a' y).
- Absurd (le (S (length y)) O); Auto with arith.
-Qed.
-End length_order.
-
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.
-
-(*********************************)
-(** The [In] predicate *)
-(*********************************)
-
-Fixpoint In [a:A;l:list] : Prop :=
- Cases l of nil => False | (cons b m) => (b=a)\/(In a m) end.
-
-Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
-Proof.
- Simpl ; Auto.
-Qed.
-Hints Resolve in_eq.
-
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
-Proof.
- Simpl ; Auto.
-Qed.
-Hints Resolve in_cons.
-
-Lemma in_nil : (a:A)~(In a nil).
-Proof.
- Unfold not; Intros a H; Inversion_clear H.
-Qed.
-
-
-Lemma in_inv : (a,b:A)(l:list)
- (In b (cons a l)) -> a=b \/ (In b l).
-Proof.
- Intros a b l H ; Inversion_clear H ; Auto.
-Qed.
-
-Lemma In_dec : ((x,y:A){x=y}+{~x=y}) -> (a:A)(l:list){(In a l)}+{~(In a l)}.
-
-Proof.
- NewInduction l as [|a0 l IHl].
- Right; Apply in_nil.
- NewDestruct (H a0 a); Simpl; Auto.
- NewDestruct IHl; Simpl; Auto.
- Right; Unfold not; Intros [Hc1 | Hc2]; Auto.
-Qed.
-
-Lemma in_app_or : (l,m:list)(a:A)(In a (l^m))->((In a l)\/(In a m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Auto.
- Intros a0 y H H0.
- NowShow '(a0=a\/(In a y))\/(In a m).
- Elim H0 ; Auto.
- Intro H1.
- NowShow '(a0=a\/(In a y))\/(In a m).
- Elim (H H1) ; Auto.
-Qed.
-Hints Immediate in_app_or.
-
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (l^m)).
-Proof.
- Intros l m a.
- Elim l ; Simpl ; Intro H.
- NowShow '(In a m).
- Elim H ; Auto ; Intro H0.
- NowShow '(In a m).
- Elim H0. (* subProof completed *)
- Intros y H0 H1.
- NowShow 'H=a\/(In a (app y m)).
- Elim H1 ; Auto 4.
- Intro H2.
- NowShow 'H=a\/(In a (app y m)).
- Elim H2 ; Auto.
-Qed.
-Hints Resolve in_or_app.
-
-(***************************)
-(** Set inclusion on list *)
-(***************************)
-
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
-Hints Unfold incl.
-
-Lemma incl_refl : (l:list)(incl l l).
-Proof.
- Auto.
-Qed.
-Hints Resolve incl_refl.
-
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
-Proof.
- Auto.
-Qed.
-Hints Immediate incl_tl.
-
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
-Proof.
- Auto.
-Qed.
-
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (n^m)).
-Proof.
- Auto.
-Qed.
-Hints Immediate incl_appl.
-
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (m^n)).
-Proof.
- Auto.
-Qed.
-Hints Immediate incl_appr.
-
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
-Proof.
- Unfold incl ; Simpl ; Intros a l m H H0 a0 H1.
- NowShow '(In a0 m).
- Elim H1.
- NowShow 'a=a0->(In a0 m).
- Elim H1 ; Auto ; Intro H2.
- NowShow 'a=a0->(In a0 m).
- Elim H2 ; Auto. (* solves subgoal *)
- NowShow '(In a0 l)->(In a0 m).
- Auto.
-Qed.
-Hints Resolve incl_cons.
-
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (l^m) n).
-Proof.
- Unfold incl ; Simpl ; Intros l m n H H0 a H1.
- NowShow '(In a n).
- Elim (in_app_or H1); Auto.
-Qed.
-Hints Resolve incl_app.
-
-(**************************)
-(** Nth element of a list *)
-(**************************)
-
-Fixpoint nth [n:nat; l:list] : A->A :=
- [default]Cases n l of
- O (cons x l') => x
- | O other => default
- | (S m) nil => default
- | (S m) (cons x t) => (nth m t default)
- end.
-
-Fixpoint nth_ok [n:nat; l:list] : A->bool :=
- [default]Cases n l of
- O (cons x l') => true
- | O other => false
- | (S m) nil => false
- | (S m) (cons x t) => (nth_ok m t default)
- end.
-
-Lemma nth_in_or_default :
- (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}.
-(* Realizer nth_ok. Program_all. *)
-Proof.
- Intros n l d; Generalize n; NewInduction l; Intro n0.
- Right; Case n0; Trivial.
- Case n0; Simpl.
- Auto.
- Intro n1; Elim (IHl n1); Auto.
-Qed.
-
-Lemma nth_S_cons :
- (n:nat)(l:list)(d:A)(a:A)(In (nth n l d) l)
- ->(In (nth (S n) (cons a l) d) (cons a l)).
-Proof.
- Simpl; Auto.
-Qed.
-
-Fixpoint nth_error [l:list;n:nat] : (Exc A) :=
- Cases n l of
- | O (cons x _) => (Value x)
- | (S n) (cons _ l) => (nth_error l n)
- | _ _ => Error
- end.
-
-Definition nth_default : A -> list -> nat -> A :=
- [default,l,n]Cases (nth_error l n) of
- | (Some x) => x
- | None => default
- end.
-
-Lemma nth_In :
- (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l).
-
-Proof.
-Unfold lt; NewInduction n as [|n hn]; Simpl.
-NewDestruct l ; Simpl ; [ Inversion 2 | Auto].
-NewDestruct l as [|a l hl] ; Simpl.
-Inversion 2.
-Intros d ie ; Right ; Apply hn ; Auto with arith.
-Qed.
-
-(********************************)
-(** Decidable equality on lists *)
-(********************************)
-
-
-Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
-Proof.
- NewInduction x as [|a l IHl]; NewDestruct y as [|a0 l0]; Auto.
- NewDestruct (H a a0) as [e|e].
- NewDestruct (IHl l0) as [e'|e'].
- Left; Rewrite e; Rewrite e'; Trivial.
- Right; Red; Intro.
- Apply e'; Injection H0; Trivial.
- Right; Red; Intro.
- Apply e; Injection H0; Trivial.
-Qed.
-
-(*************************)
-(** Reverse *)
-(*************************)
-
-Fixpoint rev [l:list] : list :=
- Cases l of
- nil => nil
- | (cons x l') => (rev l')^(cons x nil)
- end.
-
-Lemma distr_rev :
- (x,y:list) (rev (x^y))=((rev y)^(rev x)).
-Proof.
- NewInduction x as [|a l IHl].
- NewDestruct y.
- Simpl.
- Auto.
-
- Simpl.
- Apply app_nil_end;Auto.
-
- Intro y.
- Simpl.
- Rewrite (IHl y).
- Apply (app_ass (rev y) (rev l) (cons a nil)).
-Qed.
-
-Remark rev_unit : (l:list)(a:A) (rev l^(cons a nil))= (cons a (rev l)).
-Proof.
- Intros.
- Apply (distr_rev l (cons a nil));Simpl;Auto.
-Qed.
-
-Lemma idempot_rev : (l:list)(rev (rev l))=l.
-Proof.
- NewInduction l as [|a l IHl].
- Simpl;Auto.
-
- Simpl.
- Rewrite (rev_unit (rev l) a).
- Rewrite -> IHl;Auto.
-Qed.
-
-(*********************************************)
-(** Reverse Induction Principle on Lists *)
-(*********************************************)
-
-Section Reverse_Induction.
-
-Unset Implicit Arguments.
-
-Remark rev_list_ind: (P:list->Prop)
- (P nil)
- ->((a:A)(l:list)(P (rev l))->(P (rev (cons a l))))
- ->(l:list) (P (rev l)).
-Proof.
- NewInduction l; Auto.
-Qed.
-Set Implicit Arguments.
-
-Lemma rev_ind :
- (P:list->Prop)
- (P nil)->
- ((x:A)(l:list)(P l)->(P l^(cons x nil)))
- ->(l:list)(P l).
-Proof.
- Intros.
- Generalize (idempot_rev l) .
- Intros E;Rewrite <- E.
- Apply (rev_list_ind P).
- Auto.
-
- Simpl.
- Intros.
- Apply (H0 a (rev l0)).
- Auto.
-Qed.
-
-End Reverse_Induction.
-
-End Lists.
-
-Implicits nil [1].
-
-Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62.
-Hints Resolve app_comm_cons app_cons_not_nil : datatypes v62.
-Hints Immediate app_eq_nil : datatypes v62.
-Hints Resolve app_eq_unit app_inj_tail : datatypes v62.
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons
- : datatypes v62.
-Hints Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app : datatypes v62.
-Hints Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app
- : datatypes v62.
-
-Section Functions_on_lists.
-
-(****************************************************************)
-(** Some generic functions on lists and basic functions of them *)
-(****************************************************************)
-
-Section Map.
-Variables A,B:Set.
-Variable f:A->B.
-Fixpoint map [l:(list A)] : (list B) :=
- Cases l of
- nil => nil
- | (cons a t) => (cons (f a) (map t))
- end.
-End Map.
-
-Lemma in_map : (A,B:Set)(f:A->B)(l:(list A))(x:A)
- (In x l) -> (In (f x) (map f l)).
-Proof.
- NewInduction l as [|a l IHl]; Simpl;
- [ Auto
- | NewDestruct 1;
- [ Left; Apply f_equal with f:=f; Assumption
- | Auto]
- ].
-Qed.
-
-Fixpoint flat_map [A,B:Set; f:A->(list B); l:(list A)] : (list B) :=
- Cases l of
- nil => nil
- | (cons x t) => (app (f x) (flat_map f t))
- end.
-
-Fixpoint list_prod [A:Set; B:Set; l:(list A)] : (list B)->(list A*B) :=
- [l']Cases l of
- nil => nil
- | (cons x t) => (app (map [y:B](x,y) l')
- (list_prod t l'))
- end.
-
-Lemma in_prod_aux :
- (A:Set)(B:Set)(x:A)(y:B)(l:(list B))
- (In y l) -> (In (x,y) (map [y0:B](x,y0) l)).
-Proof.
- NewInduction l;
- [ Simpl; Auto
- | Simpl; NewDestruct 1 as [H1|];
- [ Left; Rewrite H1; Trivial
- | Right; Auto]
- ].
-Qed.
-
-Lemma in_prod : (A:Set)(B:Set)(l:(list A))(l':(list B))
- (x:A)(y:B)(In x l)->(In y l')->(In (x,y) (list_prod l l')).
-Proof.
- NewInduction l;
- [ Simpl; Tauto
- | Simpl; Intros; Apply in_or_app; NewDestruct H;
- [ Left; Rewrite H; Apply in_prod_aux; Assumption
- | Right; Auto]
- ].
-Qed.
-
-(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
- indexed by elts of [x], sorted in lexicographic order. *)
-
-Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) :=
- [l']Cases l of
- nil => (cons nil nil)
- | (cons x t) => (flat_map [f:(list A*B)](map [y:B](cons (x,y) f) l')
- (list_power t l'))
- end.
-
-(************************************)
-(** Left-to-right iterator on lists *)
-(************************************)
-
-Section Fold_Left_Recursor.
-Variables A,B:Set.
-Variable f:A->B->A.
-Fixpoint fold_left[l:(list B)] : A -> A :=
-[a0]Cases l of
- nil => a0
- | (cons b t) => (fold_left t (f a0 b))
- end.
-End Fold_Left_Recursor.
-
-(************************************)
-(** Right-to-left iterator on lists *)
-(************************************)
-
-Section Fold_Right_Recursor.
-Variables A,B:Set.
-Variable f:B->A->A.
-Variable a0:A.
-Fixpoint fold_right [l:(list B)] : A :=
- Cases l of
- nil => a0
- | (cons b t) => (f b (fold_right t))
- end.
-End Fold_Right_Recursor.
-
-Theorem fold_symmetric :
- (A:Set)(f:A->A->A)
- ((x,y,z:A)(f x (f y z))=(f (f x y) z))
- ->((x,y:A)(f x y)=(f y x))
- ->(a0:A)(l:(list A))(fold_left f l a0)=(fold_right f a0 l).
-Proof.
-NewDestruct l as [|a l].
-Reflexivity.
-Simpl.
-Rewrite <- H0.
-Generalize a0 a.
-NewInduction l as [|a3 l IHl]; Simpl.
-Trivial.
-Intros.
-Rewrite H.
-Rewrite (H0 a2).
-Rewrite <- (H a1).
-Rewrite (H0 a1).
-Rewrite IHl.
-Reflexivity.
-Qed.
-
-End Functions_on_lists.
-
-V7only [Implicits nil [].].
-
-(** Exporting list notations *)
-
-V8Infix "::" cons (at level 60, right associativity) : list_scope.
-
-Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 60 "++".
-
-Open Scope list_scope.
-
-Delimits Scope list_scope with list.
-
-Bind Scope list_scope with list.
diff --git a/theories7/Lists/PolyListSyntax.v b/theories7/Lists/PolyListSyntax.v
deleted file mode 100644
index 15c57166..00000000
--- a/theories7/Lists/PolyListSyntax.v
+++ /dev/null
@@ -1,10 +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: PolyListSyntax.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
-
diff --git a/theories7/Lists/Streams.v b/theories7/Lists/Streams.v
deleted file mode 100755
index ccfc4895..00000000
--- a/theories7/Lists/Streams.v
+++ /dev/null
@@ -1,170 +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: Streams.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
-
-Set Implicit Arguments.
-
-(** Streams *)
-
-Section Streams.
-
-Variable A : Set.
-
-CoInductive Set Stream := Cons : A->Stream->Stream.
-
-
-Definition hd :=
- [x:Stream] Cases x of (Cons a _) => a end.
-
-Definition tl :=
- [x:Stream] Cases x of (Cons _ s) => s end.
-
-
-Fixpoint Str_nth_tl [n:nat] : Stream->Stream :=
- [s:Stream] Cases n of
- O => s
- |(S m) => (Str_nth_tl m (tl s))
- end.
-
-Definition Str_nth : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)).
-
-
-Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end).
-Proof.
- Intro x.
- Case x.
- Trivial.
-Qed.
-
-Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)).
-Proof.
- Induction n; Simpl; Auto.
-Qed.
-Hints Resolve tl_nth_tl : datatypes v62.
-
-Lemma Str_nth_tl_plus
-: (n,m:nat)(s:Stream)(Str_nth_tl n (Str_nth_tl m s))=(Str_nth_tl (plus n m) s).
-Induction n; Simpl; Intros; Auto with datatypes.
-Rewrite <- H.
-Rewrite tl_nth_tl; Trivial with datatypes.
-Qed.
-
-Lemma Str_nth_plus
- : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s).
-Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes.
-Qed.
-
-(** Extensional Equality between two streams *)
-
-CoInductive EqSt : Stream->Stream->Prop :=
- eqst : (s1,s2:Stream)
- ((hd s1)=(hd s2))->
- (EqSt (tl s1) (tl s2))
- ->(EqSt s1 s2).
-
-(** A coinduction principle *)
-
-Tactic Definition CoInduction proof :=
- Cofix proof; Intros; Constructor;
- [Clear proof | Try (Apply proof;Clear proof)].
-
-
-(** Extensional equality is an equivalence relation *)
-
-Theorem EqSt_reflex : (s:Stream)(EqSt s s).
-CoInduction EqSt_reflex.
-Reflexivity.
-Qed.
-
-Theorem sym_EqSt :
- (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
-(CoInduction Eq_sym).
-Case H;Intros;Symmetry;Assumption.
-Case H;Intros;Assumption.
-Qed.
-
-
-Theorem trans_EqSt :
- (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
-(CoInduction Eq_trans).
-Transitivity (hd s2).
-Case H; Intros; Assumption.
-Case H0; Intros; Assumption.
-Apply (Eq_trans (tl s1) (tl s2) (tl s3)).
-Case H; Trivial with datatypes.
-Case H0; Trivial with datatypes.
-Qed.
-
-(** The definition given is equivalent to require the elements at each
- position to be equal *)
-
-Theorem eqst_ntheq :
- (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2).
-Unfold Str_nth; Induction n.
-Intros s1 s2 H; Case H; Trivial with datatypes.
-Intros m hypind.
-Simpl.
-Intros s1 s2 H.
-Apply hypind.
-Case H; Trivial with datatypes.
-Qed.
-
-Theorem ntheq_eqst :
- (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
-(CoInduction Equiv2).
-Apply (H O).
-Intros n; Apply (H (S n)).
-Qed.
-
-Section Stream_Properties.
-
-Variable P : Stream->Prop.
-
-(*i
-Inductive Exists : Stream -> Prop :=
- | Here : forall x:Stream, P x -> Exists x
- | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
-i*)
-
-Inductive Exists : Stream -> Prop :=
- Here : (x:Stream)(P x) ->(Exists x) |
- Further : (x:Stream)(Exists (tl x))->(Exists x).
-
-CoInductive ForAll : Stream -> Prop :=
- forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll x).
-
-
-Section Co_Induction_ForAll.
-Variable Inv : Stream -> Prop.
-Hypothesis InvThenP : (x:Stream)(Inv x)->(P x).
-Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
-
-Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
-(CoInduction ForAll_coind);Auto.
-Qed.
-End Co_Induction_ForAll.
-
-End Stream_Properties.
-
-End Streams.
-
-Section Map.
-Variables A,B : Set.
-Variable f : A->B.
-CoFixpoint map : (Stream A)->(Stream B) :=
- [s:(Stream A)](Cons (f (hd s)) (map (tl s))).
-End Map.
-
-Section Constant_Stream.
-Variable A : Set.
-Variable a : A.
-CoFixpoint const : (Stream A) := (Cons a const).
-End Constant_Stream.
-
-Unset Implicit Arguments.
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-06-13 12:10:46 +0000