From: Andrea Asperti Date: Fri, 9 Dec 2011 10:43:51 +0000 (+0000) Subject: list.ma moved inside lists. X-Git-Tag: make_still_working~2038 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=844794906f5a9f97406d72b5305ce13fb75acf94;p=helm.git list.ma moved inside lists. Minor integrations. --- diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma index ce857937c..7b2606485 100644 --- a/matita/matita/lib/basics/bool.ma +++ b/matita/matita/lib/basics/bool.ma @@ -52,6 +52,9 @@ theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true. theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true. #b1 #b2 (cases b1) normalize // (cases b2) // qed. +theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true. +/3/ qed. + definition orb : bool → bool → bool ≝ λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2]. @@ -61,9 +64,24 @@ theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop. match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2). #b1 #b2 #P (elim b1) normalize // qed. +lemma orb_true_r1: ∀b1,b2:bool. + b1 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H // qed. + +lemma orb_true_r2: ∀b1,b2:bool. + b2 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H cases b1 // qed. + +lemma orb_true_l: ∀b1,b2:bool. + (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true). +* normalize /2/ qed. + definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q]. +notation "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. +interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f). + theorem bool_to_decidable_eq: ∀b1,b2:bool. decidable (b1=b2). #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed. @@ -73,3 +91,22 @@ theorem true_or_false: #b (cases b) /2/ qed. +(****** DeqSet: a set with a decidbale equality ******) + +record DeqSet : Type[1] ≝ { carr :> Type[0]; + eqb: carr → carr → bool; + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) +}. + +notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. +interpretation "eqb" 'eqb a b = (eqb ? a b). + + +(****** EnumSet: a DeqSet with an enumeration function ****** + +record EnumSet : Type[1] ≝ { carr :> DeqSet; + enum: carr + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) +}. + +*) \ No newline at end of file diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma deleted file mode 100644 index eaf89510a..000000000 --- a/matita/matita/lib/basics/list.ma +++ /dev/null @@ -1,218 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| - \ / This file is distributed under the terms of the - \ / GNU General Public License Version 2 - V_______________________________________________________________ *) - -include "basics/types.ma". -include "arithmetics/nat.ma". - -inductive list (A:Type[0]) : Type[0] := - | nil: list A - | cons: A -> list A -> list A. - -notation "hvbox(hd break :: tl)" - right associative with precedence 47 - for @{'cons $hd $tl}. - -notation "[ list0 x sep ; ]" - non associative with precedence 90 - for ${fold right @'nil rec acc @{'cons $x $acc}}. - -notation "hvbox(l1 break @ l2)" - right associative with precedence 47 - for @{'append $l1 $l2 }. - -interpretation "nil" 'nil = (nil ?). -interpretation "cons" 'cons hd tl = (cons ? hd tl). - -definition not_nil: ∀A:Type[0].list A → Prop ≝ - λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ]. - -theorem nil_cons: - ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. - #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq // -qed. - -(* -let rec id_list A (l: list A) on l := - match l with - [ nil => [] - | (cons hd tl) => hd :: id_list A tl ]. *) - -let rec append A (l1: list A) l2 on l1 ≝ - match l1 with - [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. - -definition hd ≝ λA.λl: list A.λd:A. - match l with [ nil ⇒ d | cons a _ ⇒ a]. - -definition tail ≝ λA.λl: list A. - match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. - -interpretation "append" 'append l1 l2 = (append ? l1 l2). - -theorem append_nil: ∀A.∀l:list A.l @ [] = l. -#A #l (elim l) normalize // qed. - -theorem associative_append: - ∀A.associative (list A) (append A). -#A #l1 #l2 #l3 (elim l1) normalize // qed. - -(* deleterio per auto -ntheorem cons_append_commute: - ∀A:Type.∀l1,l2:list A.∀a:A. - a :: (l1 @ l2) = (a :: l1) @ l2. -//; nqed. *) - -theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. -#A #a #l #l1 >associative_append // qed. - -theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. - l1@l2=[] → P (nil A) (nil A) → P l1 l2. -#A #l1 #l2 #P (cases l1) normalize // -#a #l3 #heq destruct -qed. - -theorem nil_to_nil: ∀A.∀l1,l2:list A. - l1@l2 = [] → l1 = [] ∧ l2 = []. -#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/ -qed. - -(* iterators *) - -let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ - match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. - -let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ - match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)]. - -definition filter ≝ - λT.λp:T → bool. - foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T). - -lemma filter_true : ∀A,l,a,p. p a = true → - filter A p (a::l) = a :: filter A p l. -#A #l #a #p #pa (elim l) normalize >pa normalize // qed. - -lemma filter_false : ∀A,l,a,p. p a = false → - filter A p (a::l) = filter A p l. -#A #l #a #p #pa (elim l) normalize >pa normalize // qed. - -theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. -#A #B #f #g #l #eqfg (elim l) normalize // qed. - -let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝ -match l1 with - [ nil ⇒ nil ? - | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g - ]. - -(**************************** length ******************************) - -let rec length (A:Type[0]) (l:list A) on l ≝ - match l with - [ nil ⇒ 0 - | cons a tl ⇒ S (length A tl)]. - -notation "|M|" non associative with precedence 60 for @{'norm $M}. -interpretation "norm" 'norm l = (length ? l). - -let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ - match n with - [O ⇒ hd A l d - |S m ⇒ nth m A (tail A l) d]. - -lemma nth_nil: ∀A,a,i. nth i A ([]) a = a. -#A #a #i elim i normalize // -qed. - -(**************************** fold *******************************) - -let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝ - match l with - [ nil ⇒ b - | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l)) - (fold A B op b p f l)]. - -notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" - with precedence 80 -for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}. - -notation "\fold [ op , nil ]_{ident i ∈ l } f" - with precedence 80 -for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}. - -interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l). - -theorem fold_true: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → - \fold[op,nil]_{i ∈ a::l| p i} (f i) = - op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). -#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. - -theorem fold_false: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f. -p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = - \fold[op,nil]_{i ∈ l| p i} (f i). -#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. - -theorem fold_filter: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B. - \fold[op,nil]_{i ∈ l| p i} (f i) = - \fold[op,nil]_{i ∈ (filter A p l)} (f i). -#A #B #a #l #p #op #nil #f elim l // -#a #tl #Hind cases(true_or_false (p a)) #pa - [ >filter_true // > fold_true // >fold_true // - | >filter_false // >fold_false // ] -qed. - -record Aop (A:Type[0]) (nil:A) : Type[0] ≝ - {op :2> A → A → A; - nill:∀a. op nil a = a; - nilr:∀a. op a nil = a; - assoc: ∀a,b,c.op a (op b c) = op (op a b) c - }. - -theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f. - op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) = - \fold[op,nil]_{i∈(I@J)} (f i). -#A #B #I #J #nil #op #f (elim I) normalize - [>nill //|#a #tl #Hind