commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 3b878a63c49c3a093b55373ce9584c8f8658cb2f..ad0896d708ce9792ef00ed8cfb19c1bae68b7fe0 100644 (file)
--- 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6q,r〉 →
+  r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 q \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 
+  r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 q).
 
+(* We can now construct a function from n to {p|div2Spec n p} by composing the objects
+we already have *)
 
+definition div2P: ∀n.\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6 Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"\ 6div2Spec\ 5/a\ 6 n) ≝ λn.
+ \ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n) (\ 5a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"\ 6div2_ok\ 5/a\ 6 n).
 
- axiom div2P n : nat → {N×N | True}.
+(* But we can also try do directly build such an object *)
 
+definition div2Pbis : ∀n.\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"\ 6div2Spec\ 5/a\ 6 n).
+#n elim n
+  [@(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6,\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6〉) normalize #q #r #H %1 destruct /2/
+  |#a * #p #spec cases (spec … (\ 5a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"\ 6surjective_pairing\ 5/a\ 6 …)) * #eqr #eqa
+    [@(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p,\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6〉) #q #r #H %2 destruct /2/ 
+    |@(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6〉) #q #r #H %1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 /2/
+    ]
+  ]
 
 
+lemma foo: True. 
+\ 5pre\ 6 \ 5/pre\ 6
\ No newline at end of file