diff options
Diffstat (limited to 'theories/Lists/MonoList.v')
| -rwxr-xr-x | theories/Lists/MonoList.v | 269 |
1 files changed, 269 insertions, 0 deletions
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v new file mode 100755 index 00000000..d639a39d --- /dev/null +++ b/theories/Lists/MonoList.v @@ -0,0 +1,269 @@ +(************************************************************************) +(* 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.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) + +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) + +Require Import Le. + +Parameter List_Dom : Set. +Definition A := List_Dom. + +Inductive list : Set := + | nil : list + | cons : A -> list -> list. + +Fixpoint app (l m:list) {struct l} : list := + match l return list with + | nil => m + | cons a l1 => cons a (app l1 m) + end. + + +Lemma app_nil_end : forall l:list, l = app l nil. +Proof. + intro l; elim l; simpl in |- *; auto. + simple induction 1; auto. +Qed. +Hint Resolve app_nil_end: list v62. + +Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n). +Proof. + intros l m n; elim l; simpl in |- *; auto with list. + simple induction 1; auto with list. +Qed. +Hint Resolve app_ass: list v62. + +Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n. +Proof. + auto with list. +Qed. +Hint Resolve ass_app: list v62. + +Definition tail (l:list) : list := + match l return list with + | cons _ m => m + | _ => nil + end. + + +Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m. + intros; discriminate. +Qed. + +(****************************************) +(* Length of lists *) +(****************************************) + +Fixpoint length (l:list) : nat := + match l return nat with + | cons _ m => S (length m) + | _ => 0 + end. + +(******************************) +(* Length order of lists *) +(******************************) + +Section length_order. +Definition lel (l m:list) := length l <= length m. + +Hint Unfold lel: list. + +Variables a b : A. +Variables l m n : list. + +Lemma lel_refl : lel l l. +Proof. + unfold lel in |- *; auto with list. +Qed. + +Lemma lel_trans : lel l m -> lel m n -> lel l n. +Proof. + unfold lel in |- *; 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 in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_cons : lel l m -> lel l (cons b m). +Proof. + unfold lel in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m. +Proof. + unfold lel in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_nil : forall 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 (S (length y) <= 0); auto with list arith. +Qed. +End length_order. + +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list + v62. + +Fixpoint In (a:A) (l:list) {struct l} : Prop := + match l with + | nil => False + | cons b m => b = a \/ In a m + end. + +Lemma in_eq : forall (a:A) (l:list), In a (cons a l). +Proof. + simpl in |- *; auto with list. +Qed. +Hint Resolve in_eq: list v62. + +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l). +Proof. + simpl in |- *; auto with list. +Qed. +Hint Resolve in_cons: list v62. + +Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m. +Proof. + intros l m a. + elim l; simpl in |- *; 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. +Hint Immediate in_app_or: list v62. + +Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m). +Proof. + intros l m a. + elim l; simpl in |- *; 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. +Hint Resolve in_or_app: list v62. + +Definition incl (l m:list) := forall a:A, In a l -> In a m. + +Hint Unfold incl: list v62. + +Lemma incl_refl : forall l:list, incl l l. +Proof. + auto with list. +Qed. +Hint Resolve incl_refl: list v62. + +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m). +Proof. + auto with list. +Qed. +Hint Immediate incl_tl: list v62. + +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. +Proof. + auto with list. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m). +Proof. + auto with list. +Qed. +Hint Immediate incl_appl: list v62. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n). +Proof. + auto with list. +Qed. +Hint Immediate incl_appr: list v62. + +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m. +Proof. + unfold incl in |- *; simpl in |- *; 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. +Hint Resolve incl_cons: list v62. + +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n. +Proof. + unfold incl in |- *; simpl in |- *; 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. +Hint Resolve incl_app: list v62.
\ No newline at end of file |