-(* In this Chapter we shall develop a naif theory of sets represented as characteristic
-predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop. *)
+(* In this Chapter we shall develop a naif theory of sets represented as
+characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
+A→Prop. *)
include "basics/types.ma".
include "basics/bool.ma".
definition DeqBool ≝ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
(* At this point, we would expect to be able to prove things like the
-following: for any boolean b, if b==false is true then b=false. *)
+following: for any boolean b, if b==false is true then b=false.
+Unfortunately, this would not work, unless we declare b of type
+DeqBool (change the type in the following statement and see what
+happens). *)
-(* unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
+example exhint: ∀b:\ 5a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6. (b\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#b #H @(\P H)
+qed.
+
+(* The point is that == expects in input a pair of objects whose type must be the
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
+system has no knowledge of it (it is an information that has been supplied by the
+user, and stored somewhere in the library). More explicitly, the type inference
+inference system, would face an unification problem consisting to unify bool
+against the carrier of something (a metavaribale) and it has no way to synthetize
+the answer. To solve this kind of situations, matita provides a mechanism to hint
+the system the expected solution. A unification hint is a kind of rule, whose rhd
+is the unification problem, containing some metavariables X1, ..., Xn, and whose
+left hand side is the solution suggested to the system, in the form of equations
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.
+To make an example, in the previous case, the unification problem is bool = carr X,
+and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
+bool is convertible with (carr (mk_DeqSet bool beb true)). *)
+
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
(* ---------------------------------------- *) ⊢
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
-unification hint 0 ≔ b1,b2:bool;
- X ≟ mk_DeqSet bool beqb beqb_true
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
(* ---------------------------------------- *) ⊢
- beqb b1 b2 ≡ eqb X b1 b2. *)
+ \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X b1 b2.
-example exhint: ∀b:bool. (b == false) = true → b = false.
-#b #H @(\P H).
+(* After having provided the previous hints, we may rewrite example exhint
+declaring b of type bool. *)
+
+example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. (b \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#b #H @(\P H)
qed.
-(* pairs *)
+(* The cartesian product of two DeqSets is still a DeqSet. To prove
+this, we must as usual define the boolen equality function, and prove
+it correctly reflects propositional equality. *)
+
definition eq_pairs ≝
- λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p2) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p2).
-lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
- eq_pairs A B p1 p2 = true ↔ p1 = p2.
+lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
+ \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B p1 p2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p2.
#A #B * #a1 #b1 * #a2 #b2 %
- [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
- |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+ [#H cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
+ |#H destruct normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … a2)) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … b2)) //
]
qed.
-definition DeqProd ≝ λA,B:DeqSet.
- mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-
-unification hint 0 ≔ C1,C2;
- T1 ≟ carr C1,
- T2 ≟ carr C2,
- X ≟ DeqProd C1 C2
+definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
+ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 A B).
+
+(* Having an unification problem of the kind T1×T2 = carr X, what kind
+of hint can we give to the system? We expect T1 to be the carrier of a
+DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
+This is expressed by the following hint: *)
+
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 C1,C2;
+ T1 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
+ T2 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2
(* ---------------------------------------- *) ⊢
- T1×T2 ≡ carr X.
+ T1\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6T2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
-unification hint 0 ≔ T1,T2,p1,p2;
- X ≟ DeqProd T1 T2
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 T1,T2,p1,p2;
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 T1 T2
(* ---------------------------------------- *) ⊢
- eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+ \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 T1 T2 p1 p2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X p1 p2.
example hint2: ∀b1,b2.
- 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 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\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2〉.
#b1 #b2 #H @(\P H).
\ No newline at end of file
projects / helm.git / blobdiff