From 15822b46a7d0f5ce77983e395f3a32a20029e7d6 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 17 Oct 2011 13:02:43 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 77 +++++++++++++++++++++++++++---------- 1 file changed, 56 insertions(+), 21 deletions(-) diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 4ce43679d..849b067e7 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -103,19 +103,66 @@ theorem append_cons: ∀A.∀a:A.∀l,l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.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 (l a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a a title="nil" href="cic:/fakeuri.def(1)"[/a])) a title="append" href="cic:/fakeuri.def(1)"@/a l1. /2/ qed. +(* Other typical functions over lists are those computing the length +of a list, and the function returning the nth element *) -theorem nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a span style="text-decoration: underline;"/spanA. - 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/tutorial/chapter3/nil_append_elim.def(3)"nil_append_elim/a A l1 l2) /2/ -qed. +let rec length (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l ≝ +match l with + [ nil ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a + | cons a tl ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (length A tl)]. + +let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (d:A) ≝ + match n with + [O ⇒ a href="cic:/matita/tutorial/chapter3/hd.def(1)"hd/a A l d + |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a A l) d]. + +example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a. +normalize // qed. + +example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a])) a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a. +normalize // qed. + +lemma length_add: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. + a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l1) (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l2). +#A #l1 elim l1 normalize // qed. -definition not_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/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]. +(* Let us come to a more interesting question. How can we prove that the empty list is +different from any list with at least one element, that is from any list of the kind (a::l)? +We start defining a simple predicate stating if a list is empty or not. The predicate +is computed by inspection over the list *) -theorem nil_cons: +definition is_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A → Prop ≝ +λA.λl.match l with [ nil ⇒ l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒ (l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a])]. + +(* Next we need a simple result about negation: if you wish to prove ¬P you are +authorized to add P to your hypothesis: *) + +lemma neg_aux : ∀P:Prop. (P → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP. +#P #PtonegP % /3/ qed. + +theorem diff_cons_nil: ∀A:Type[0].∀l:a href="cic:/matita/tutorial/chapter3/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/tutorial/chapter3/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // -qed. +#A #l #a @a href="cic:/matita/tutorial/chapter3/neg_aux.def(3)"neg_aux/a #Heq +(* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux. +Next we use the change tactic to pass from the current goal a::l≠ [] to the expression +is_nil a::l, convertible with it. *) +(change with (a href="cic:/matita/tutorial/chapter3/is_nil.def(1)"is_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) +(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial +goal [] = [] *) +>Heq // qed. + +(* As an application of the previous result let us prove that l1@l2 is empty if and +only if both l1 and l2 are empty. The idea is to proceed by cases on l1: if l1=[] the +statement is trivial; on the other side, if l1 = a::tl, then the hypothesis +(a::tl)@l2 = [] is absurd, hence we can prove anything from it. When we know we can +prove both A and ¬A, a sensible way to proceed is to apply False_ind: ∀P.False → P to the +current goal, that breaks down to prove False, and then absurd: ∀A:Prop. A → ¬A → False +to reduce to the contradictory cases. Usually, you may invoke automation to take care +to solve the absurd case. *) + +lemma nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a span style="text-decoration: underline;"/spanA. + 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 cases l1 normalize /2/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. (* iterators *) @@ -147,18 +194,6 @@ match l1 with | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g ]. *) -(**************************** length ******************************) - -let rec length (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l ≝ - match l with - [ nil ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a - | cons a tl ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (length A tl)]. - -let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (d:A) ≝ - match n with - [O ⇒ a href="cic:/matita/tutorial/chapter3/hd.def(1)"hd/a A l d - |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a A l) d]. - (**************************** fold *******************************) 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/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝ -- 2.39.2