X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2FFsub%2Futil.ma;h=41089172e56d6c76ece6e834aa665db4ba8feee9;hb=a5bfa65b18a876fca982270f673c686a7d124f65;hp=8b111e3f2425637f1fc75086a96265cb78ff6db7;hpb=59f20005cd1064eb12c2dbdb829c4380100bd40f;p=helm.git diff --git a/matita/library/Fsub/util.ma b/matita/library/Fsub/util.ma index 8b111e3f2..41089172e 100644 --- a/matita/library/Fsub/util.ma +++ b/matita/library/Fsub/util.ma @@ -19,27 +19,40 @@ include "list/list.ma". (*** useful definitions and lemmas not really related to Fsub ***) -lemma eqb_case : \forall x,y.(eqb x y) = true \lor (eqb x y) = false. -intros;elim (eqb x y);auto; -qed. - -lemma eq_eqb_case : \forall x,y.((x = y) \land (eqb x y) = true) \lor - ((x \neq y) \land (eqb x y) = false). -intros;lapply (eqb_to_Prop x y);elim (eqb_case x y) - [rewrite > H in Hletin;simplify in Hletin;left;auto - |rewrite > H in Hletin;simplify in Hletin;right;auto] -qed. - -let rec max m n \def +definition max \def +\lambda m,n. match (leb m n) with [true \Rightarrow n |false \Rightarrow m]. + +lemma le_n_max_m_n: \forall m,n:nat. n \le max m n. +intros. +unfold max. +apply (leb_elim m n) + [simplify.intros.apply le_n + |simplify.intros.autobatch + ] +qed. + +lemma le_m_max_m_n: \forall m,n:nat. m \le max m n. +intros. +unfold max. +apply (leb_elim m n) + [simplify.intro.assumption + |simplify.intros.autobatch + ] +qed. + +inductive in_list (A:Type): A → (list A) → Prop ≝ +| in_Base : ∀ x,l.(in_list A x (x::l)) +| in_Skip : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). -inductive in_list (A : Set) : A \to (list A) \to Prop \def - | in_Base : \forall x:A.\forall l:(list A). - (in_list A x (x :: l)) - | in_Skip : \forall x,y:A.\forall l:(list A). - (in_list A x l) \to (in_list A x (y :: l)). +notation > "hvbox(x ∈ l)" + non associative with precedence 30 for @{ 'inlist $x $l }. +notation < "hvbox(x \nbsp ∈ \nbsp l)" + non associative with precedence 30 for @{ 'inlist $x $l }. +interpretation "item in list" 'inlist x l = + (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l). definition incl : \forall A.(list A) \to (list A) \to Prop \def \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m). @@ -52,82 +65,73 @@ definition map : \forall A,B,f.((list A) \to (list B)) \def |(cons (a:A) (t:(list A))) \Rightarrow (cons B (f a) (map t))] in map. -definition swap : nat \to nat \to nat \to nat \def - \lambda u,v,x.match (eqb x u) with - [true \Rightarrow v - |false \Rightarrow match (eqb x v) with - [true \Rightarrow u - |false \Rightarrow x]]. - lemma in_list_nil : \forall A,x.\lnot (in_list A x []). intros.unfold.intro.inversion H - [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = []) - [assumption|apply nil_cons] - |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = []) - [assumption|apply nil_cons]] + [intros;lapply (sym_eq ? ? ? H2);destruct Hletin + |intros;destruct H4] qed. -lemma notin_cons : \forall A,x,y,l.\lnot (in_list A x (y::l)) \to - (y \neq x) \land \lnot (in_list A x l). -intros.split - [unfold;intro;apply H;rewrite > H1;constructor 1 - |unfold;intro;apply H;constructor 2;assumption] +lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t). +intros;inversion H;intros + [destruct H2;left;symmetry;assumption + |destruct H4;right;applyS H1] qed. -lemma swap_left : \forall x,y.(swap x y x) = y. -intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity; +lemma append_nil:\forall A:Type.\forall l:list A. l@[]=l. +intros. +elim l;intros;autobatch. qed. -lemma swap_right : \forall x,y.(swap x y y) = x. -intros;unfold swap;elim (eq_eqb_case y x) - [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity - |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity] +lemma append_cons:\forall A.\forall a:A.\forall l,l1. +l@(a::l1)=(l@[a])@l1. +intros. +rewrite > associative_append. +reflexivity. qed. -lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z. -intros;unfold swap;elim (eq_eqb_case z x) - [elim H2;lapply (H H3);elim Hletin - |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y) - [elim H5;lapply (H1 H6);elim Hletin - |elim H5;rewrite > H7;simplify;reflexivity]] -qed. +lemma in_list_append1: \forall A.\forall x:A. +\forall l1,l2. x \in l1 \to x \in l1@l2. +intros. +elim H + [simplify.apply in_Base + |simplify.apply in_Skip.assumption + ] +qed. -lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x. -intros;unfold in match (swap u v x);elim (eq_eqb_case x u) - [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right - |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v) - [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left - |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]] +lemma in_list_append2: \forall A.\forall x:A. +\forall l1,l2. x \in l2 \to x \in l1@l2. +intros 3. +elim l1 + [simplify.assumption + |simplify.apply in_Skip.apply H.assumption + ] qed. -lemma swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y. -intros;unfold swap in H;elim (eq_eqb_case x u) - [elim H1;elim (eq_eqb_case y u) - [elim H4;rewrite > H5;assumption - |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H; - elim (eq_eqb_case y v) - [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8; - lapply (H5 H8);elim Hletin - |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]] - |elim H1;elim (eq_eqb_case y u) - [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H; - elim (eq_eqb_case x v) - [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8; - elim H2;assumption - |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption] - |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H; - elim (eq_eqb_case x v) - [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v) - [elim H10;rewrite > H11;assumption - |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry; - assumption] - |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v) - [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption - |elim H10;rewrite > H12 in H;simplify in H;assumption]]]] +theorem append_to_or_in_list: \forall A:Type.\forall x:A. +\forall l,l1. x \in l@l1 \to (x \in l) \lor (x \in l1). +intros 3. +elim l + [right.apply H + |simplify in H1.inversion H1;intros + [destruct H3.left.rewrite < Hcut. + apply in_Base + |destruct H5. + elim (H l2) + [left.apply in_Skip. + rewrite < H4.assumption + |right.rewrite < H4.assumption + |rewrite > Hcut1.rewrite > H4.assumption + ] + ] + ] qed. lemma max_case : \forall m,n.(max m n) = match (leb m n) with - [ false \Rightarrow n - | true \Rightarrow m ]. + [ true \Rightarrow n + | false \Rightarrow m ]. intros;elim m;simplify;reflexivity; -qed. \ No newline at end of file +qed. + +lemma incl_A_A: ∀T,A.incl T A A. +intros.unfold incl.intros.assumption. +qed. \ No newline at end of file