From: matitaweb Date: Wed, 12 Oct 2011 15:49:17 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2195 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a01d31298e5e699fa198135655018bf73fe6e3f0;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 3b878a63c..ad0896d70 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -215,13 +215,31 @@ an element of a of type A and a proof of P(a). The crucial point is to have a la reach enough to comprise proofs among its expressions. *) -inductive Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝ -| sub_intro : ∀a:A. P a → Sub A P. +record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝ + {witness: A; + proof: P witness}. + definition div2Spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → + r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a + r 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 a title="logical and" href="cic:/fakeuri.def(1)"∧/a n 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/twice.def(2)"twice/a q). +(* We can now construct a function from n to {p|div2Spec n p} by composing the objects +we already have *) +definition div2P: ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)" Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/a n) ≝ λn. + a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a ?? (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n) (a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"div2_ok/a n). - axiom div2P n : nat → {N×N | True}. +(* But we can also try do directly build such an object *) +definition div2Pbis : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/a n). +#n elim n + [@(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉) normalize #q #r #H %1 destruct /2/ + |#a * #p #spec cases (spec … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa + [@(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,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〉) #q #r #H %2 destruct /2/ + |@(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉) #q #r #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a /2/ + ] + ] +lemma foo: True. +pre /pre \ No newline at end of file