From cf367920b94b3a95c5c068c2f0672b97bf579731 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 16 Sep 2011 12:17:47 +0000 Subject: [PATCH] mah... --- weblib/basics/list.ma | 105 +++++++++++++++++++++-------------------- weblib/basics/types.ma | 8 ++-- 2 files changed, 57 insertions(+), 56 deletions(-) diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index 798f57629..14f7aaaa7 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -9,8 +9,8 @@ \ / GNU General Public License Version 2 V_______________________________________________________________ *) -include "basics/types.ma". -include "arithmetics/nat.ma". +include "basics/bool.ma". +(* include "arithmetics/nat.ma". *) inductive list (A:Type[0]) : Type[0] := | nil: list A @@ -31,12 +31,12 @@ notation "hvbox(l1 break @ 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 ]. +definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝ + λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ]. 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 // + ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. + #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // qed. (* @@ -45,24 +45,24 @@ let rec id_list A (l: list A) on l := [ nil => [] | (cons hd tl) => hd :: id_list A tl ]. *) -let rec append A (l1: list A) l2 on l1 ≝ +let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ match l1 with [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. + | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ]. -definition hd ≝ λA.λl: list A.λd:A. +definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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]. +definition tail ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒ tl]. interpretation "append" 'append l1 l2 = (append ? l1 l2). -theorem append_nil: ∀A.∀l:list A.l @ [] = l. +theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l. #A #l (elim l) normalize // qed. theorem associative_append: - ∀A.associative (list A) (append A). + ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a A). #A #l1 #l2 #l3 (elim l1) normalize // qed. (* deleterio per auto @@ -71,50 +71,51 @@ ntheorem cons_append_commute: a :: (l1 @ l2) = (a :: l1) @ l2. //; nqed. *) -theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. +theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])a title="append" href="cic:/fakeuri.def(1)"@/al1. /2/ qed. -theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. - l1@l2=[] → P (nil A) (nil A) → P l1 l2. +theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. + l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a 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/ +theorem nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. +#A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(3)"nil_append_elim/a 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 map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝ + match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)]. -let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ +let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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). + λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. + a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p x) (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T). -lemma filter_true : ∀A,l,a,p. p a = true → - filter A p (a::l) = a :: filter A p l. +lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a 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. +lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → + a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a 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. +theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a 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 ? + [ nil ⇒ nil ? | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g - ]. + ]. *) -(**************************** length ******************************) +(**************************** length ****************************** let rec length (A:Type[0]) (l:list A) on l ≝ match l with @@ -129,12 +130,12 @@ let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ [O ⇒ hd A l d |S m ⇒ nth m A (tail A l) d]. -(**************************** fold *******************************) +**************************** 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 ≝ +let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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)) + | cons a l ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (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" @@ -148,38 +149,38 @@ 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:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[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). +p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[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 title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a 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 // ] +#a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa + [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // + | >a href="cic:/matita/basics/list/filter_false.def(3)"filter_false/a // >a href="cic:/matita/basics/list/fold_false.def(3)"fold_false/a // ] 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 + nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; + nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; + assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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). +theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f. + op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i). #A #B #I #J #nil #op #f (elim I) normalize - [>nill //|#a #tl #Hind a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //] qed. diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma index c14cc60b4..494177cfc 100644 --- a/weblib/basics/types.ma +++ b/weblib/basics/types.ma @@ -25,10 +25,10 @@ interpretation "Pair construction" 'pair x y = (pair ? ? x y). interpretation "Product" 'product x y = (Prod x y). -definition fst ≝ λA,B.λp:A × B. +definition fst ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B. match p with [pair a b ⇒ a]. -definition snd ≝ λA,B.λp:A × B. +definition snd ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B. match p with [pair a b ⇒ b]. interpretation "pair pi1" 'pi1 = (fst ? ?). @@ -38,8 +38,8 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x). interpretation "pair pi1" 'pi1b x y = (fst ? ? x y). interpretation "pair pi2" 'pi2b x y = (snd ? ? x y). -theorem eq_pair_fst_snd: ∀A,B.∀p:A × B. - p = 〈 \fst p, \snd p 〉. +theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B. + p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉. #A #B #p (cases p) // qed. (* sum *) -- 2.39.2