From: Claudio Sacerdoti Coen Date: Wed, 10 Sep 2014 13:22:43 +0000 (+0000) Subject: New chapter on setoids. X-Git-Tag: make_still_working~848 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b2aa3d637ec0e530a37748f2832ac45967965b7a;p=helm.git New chapter on setoids. --- diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma new file mode 100644 index 000000000..233b0bbba --- /dev/null +++ b/matita/matita/lib/tutorial/chapter12.ma @@ -0,0 +1,477 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/relations.ma". +include "basics/types.ma". +include "arithmetics/nat.ma". +include "hints_declaration.ma". + +(******************* Quotienting in type theory **********************) + +(* One fundamental operation in set theory is quotienting: given a set S + and an equivalence relation R over S, quotienting creates a new set S/R + whose elements are equivalence classes of elements of S. The idea behind + quotienting is to replace the structural equality over S with R, therefore + identifying elements up to R. The use of equivalence classes is just a + technicality. + + The type theory of Matita does not have quotient types. In the litterature + there are alternative proposals to introduce quotient types, but no consensus + have been reached yet. Nevertheless, quotient types can be dispensed and + replaced by setoids. A setoid is defined as a type S coupled with an + equivalence relation R, used to compare elements of S. In place of working + with equivalence classes of S up to R, one keeps working with elements of S, + but compares them using R in place of =. Setoids over types (elements of + Type[0]) can be declared in Matita as follows. *) + +record equivalence_relation (A: Type[0]) : Type[0] ≝ { + eqrel:> relation A + ; equiv_refl: reflexive … eqrel + ; equiv_sym: symmetric … eqrel + ; equiv_trans: transitive … eqrel +}. + +record setoid : Type[1] ≝ { + carrier:> Type[0] + ; eq_setoid: equivalence_relation carrier +}. + +(* Note that carrier has been defined as a coercion so that when S is a setoid + we can write x:S in place of x: carrier S. *) + +(* We use the notation ≃ for the equality over setoid elements. *) +notation "hvbox(n break ≃ m)" + non associative with precedence 45 +for @{ 'congruent $n $m }. + +interpretation "eq_setoid" 'congruent n m = (eqrel ? (eq_setoid ?) n m). + +(* Example: integers as pairs of naturals (n,m) quotiented by + (n1,m1) ≝ (n2,m2) iff n1 + m2 = m1 + n2. The integer +n is represented + by any pair (k,n+k), while the integer -n by any pair (n+k,n). + The three proof obligations are to prove reflexivity, symmetry and + transitivity. Only the latter is not closed by automation. *) +definition Z: setoid ≝ + mk_setoid (ℕ × ℕ) + (mk_equivalence_relation … + (λc1,c2. \fst c1 + \snd c2 = \fst c2 + \snd c1) …). + whd // * #x1 #x2 * #y1 #y2 * #z1 #z3 #H1 #H2 + cut (x1 + y2 + y1 + z3 = y1 + x2 + z1 + y2) // #H3 + cut ((y2 + y1) + (x1 + z3) = (y2 + y1) + (z1 + x2)) // #H4 + @(injective_plus_r … H4) +qed. + +(* The two integers (0,1) and (1,2) are equal up to ≝, written + 〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to + eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two + pairs are to be compare according to the equivalence relation + of an unknown setoid ? whose carrier is ℕ × ℕ. An hint can be + used to always pick Z as the setoid for ℕ × ℕ. *) + +unification hint 0 ≔ ; + X ≟ Z +(* ---------------------------------------- *) ⊢ + ℕ × ℕ ≡ carrier X. + +(* Thanks to the hint, Matita now accepts the statement. *) +example ex1: 〈0,1〉 ≃ 〈1,2〉. + // +qed. + +(* Every type is a setoid when elements are compared up to Leibniz equality. *) +definition LEIBNIZ: Type[0] → setoid ≝ + λA. + mk_setoid A + (mk_equivalence_relation … (eq …) …). + // +qed. + +(* Note that we declare the hint with a lower precedence level (10 vs 0, + precedence levels are in decreasing order). In this way an ad-hoc setoid + hint will be always preferred to the Leibniz one. for example, + 〈0,1〉 ≃ 〈1,2〉 is still interpreted in Z, while 1 ≃ 2 is interpreted as 1=2. *) +unification hint 10 ≔ A: Type[0]; + X ≟ LEIBNIZ A +(* ---------------------------------------- *) ⊢ + A ≡ carrier X. + +(* Propositions up to coimplication form a setoid. *) +definition PROP: setoid ≝ + mk_setoid Prop + (mk_equivalence_relation … (λx,y. x ↔ y) …). + whd [ @iff_trans | @iff_sym | /2/ ] +qed. + +unification hint 0 ≔ ; + X ≟ PROP +(* ---------------------------------------- *) ⊢ + Prop ≡ carrier X. + +(* In set theory functions and relations over a quotient S/R can be defined + by lifting a function/relation over S that respects R. Respecting R means that + the relations holds for an element x of S iff it holds for every y of S such + that x R y. Similarly, a function f respects R iff f x = f y for every x,y + such that x R y. In type theory propositions are just special cases of + functions whose codomain is Prop. + + Note that in the definition of respect for functions in set theory f x and + f y are compared using =. When working with setoids in type theory we need + to systematically abandon = in favour of ≃, unless we know in advance that + a certain type taken in input is never going to be quotiented. We say that + a function between two setoids is proper when it respects their equalities. *) + +definition proper: ∀I,O:setoid. (I → O) → Prop ≝ + λI,O,f. ∀x,y:I. x ≃ y → f x ≃ f y. + +(* A proper function is called a morphism. *) +record morphism (I,O: setoid) : Type[0] ≝ { + mor_carr:1> I → O + ; mor_proper: proper … mor_carr + }. + +(* We introduce a notation for morhism using a long arrow. *) +notation "hvbox(I break ⤞ O)" + right associative with precedence 20 +for @{ 'morphism $I $O }. + +interpretation "morphism" 'morphism I O = (morphism I O). + +(* By declaring mor_carr as a coercion it is possible to write f x for + mor_carr f x in order to apply a morphism f to an argument. *) + +(* Example: oppositive of an integer number. We first implement the function + over Z and then lift it to a morphism. The proof obligation is to prove + properness. *) +definition opp: Z → Z ≝ λc.〈\snd c,\fst c〉. + +definition OPP: Z ⤞ Z ≝ mk_morphism … opp …. + normalize // +qed. + +(* When writing expressions over Z we will always use the function opp, that + does not carry additional information. The following hints will be automatically + used by the system to retrieve the morphism associated to opp when needed, i.e. + to retrieve the proof of properness of opp. This is a use of unification hints + to implement automatic proof search. The first hint is used when the function + is partially applied, the second one when it is applied to an argument. *) + +unification hint 0 ≔ ; + X ≟ OPP +(* ---------------------------------------- *) ⊢ + opp ≡ mor_carr … X. + +unification hint 0 ≔ x:Z ; + X ≟ OPP +(* ---------------------------------------- *) ⊢ + opp x ≡ mor_carr … X x. + +(* Example: we state that opp is proper and we will prove it without using + automation and without referring to OPP. When we apply the universal mor_proper + property of morhisms, Matita looks for the morphism associate to opp x and + finds it thanks to the second unification hint above, completing the proof. *) +example ex2: ∀x,y. x ≃ y → opp x ≃ opp y. + #x #y #EQ @mor_proper @EQ +qed. + +(* The previous definition of proper only deals with unary functions. In type + theory n-ary functions are better handled in Curryfied form as unary functions + whose output is a function space type. When we restrict to morphisms, we do not + need a notion of properness for n-ary functions because the function space can + also be seen as a setoid quotienting functions using functional extensionality: + two morphisms are equal when they map equal elements to equal elements. *) +definition function_space: setoid → setoid → setoid ≝ + λI,O. + mk_setoid (I ⤞ O) + (mk_equivalence_relation … (λf,g. ∀x,y:I. x ≃ y → f x ≃ g y) …). + whd + [ #f1 #f2 #f3 #f1_f2 #f2_f3 #x #y #EQ @(equiv_trans … (f2 x)) /2/ + | #f1 #f2 #f1_f2 #x #y #EQ @(equiv_sym … (f1_f2 …)) @equiv_sym // + | #f #x #y #EQ @mor_proper // ] +qed. + +unification hint 0 ≔ I,O: setoid; + X ≟ function_space I O +(* ---------------------------------------- *) ⊢ + I ⤞ O ≡ carrier X. + +(* We overload the notation so that I ⤞ O can mean both the type of morphisms + from I to O or the function space from I to O. *) +interpretation "function_space" 'morphism I O = (function_space I O). + +(* A binary morphism is just obtained by Currification. In the following + we will use I1 ⤞ I2 ⤞ O directly in place of bin_morphism. *) +definition bin_morphism: setoid → setoid → setoid → Type[0] ≝ + λI1,I2,O. I1 ⤞ I2 ⤞ O. + +(* Directly inhabiting a binary morphism is annoying because one needs to + write a function that returns a morphism in place of a binary function. + Moreover, there are two proof obligations to prove. We can simplify the work + by introducing a new constructor for binary morphisms that takes in input a + binary function and opens a single proof obligation, called proper2. *) +definition proper2: ∀I1,I2,O: setoid. (I1 → I2 → O) → Prop ≝ + λI1,I2,O,f. + ∀x1,x2,y1,y2. x1 ≃ x2 → y1 ≃ y2 → f x1 y1 ≃ f x2 y2. + +definition mk_bin_morphism: + ∀I1,I2,O: setoid. ∀f: I1 → I2 → O. proper2 … f → I1 ⤞ I2 ⤞ O ≝ +λI1,I2,O,f,proper. + mk_morphism … (λx. mk_morphism … (λy. f x y) …) …. + normalize /2/ +qed. + +(* We can also coerce a binary morphism to a binary function and prove that + proper2 holds for every binary morphism. *) +definition binary_function_of_binary_morphism: + ∀I1,I2,O: setoid. (I1 ⤞ I2 ⤞ O) → (I1 → I2 → O) ≝ +λI1,I2,O,f,x,y. f x y. + +coercion binary_function_of_binary_morphism: + ∀I1,I2,O: setoid. ∀f:I1 ⤞ I2 ⤞ O. (I1 → I2 → O) ≝ + binary_function_of_binary_morphism + on _f: ? ⤞ ? ⤞ ? to ? → ? → ?. + +theorem mor_proper2: ∀I1,I2,O: setoid. ∀f: I1 ⤞ I2 ⤞ O. proper2 … f. + #I2 #I2 #O #f #x1 #x2 #y1 #y2 #EQx #EQy @(mor_proper … f … EQx … EQy) +qed. + +(* Example: addition of integer numbers. We define addition as a function + before lifting it to a morphism and declaring the hints to automatically + prove it proper when needed. *) +definition Zplus: Z → Z → Z ≝ λx,y. 〈\fst x + \fst y,\snd x + \snd y〉. + +(* We overload + over integers. *) +interpretation "Zplus" 'plus x y = (Zplus x y). + +definition ZPLUS: Z ⤞ Z ⤞ Z ≝ mk_bin_morphism … Zplus …. + normalize * #x1a #x1b * // +qed. + +unification hint 0 ≔ x,y:Z ; + X ≟ ZPLUS +(* ---------------------------------------- *) ⊢ + x + y ≡ mor_carr … X x y. + +(* The identity function is a morphism and composition of morphisms is also + a morphism. This means that the identity function is always proper and + a compound context is proper if every constituent is. *) +definition id_morphism: ∀S: setoid. S ⤞ S ≝ + λS. mk_morphism … (λx.x) …. + // +qed. + +definition comp_morphism: ∀S1,S2,S3. (S2 ⤞ S3) → (S1 ⤞ S2) → (S1 ⤞ S3) ≝ + λS1,S2,S3,f1,f2. mk_morphism … (λx. f1 (f2 x)) …. + normalize #x1 #x2 #EQ @mor_proper @mor_proper // +qed. + +(* +(* The following hint is an example of proof automation rule. It says that + f1 (f2 x) can be seen to be the application of the morphism + comp_morphism F1 F2 to x as long as two morphisms F1 and F2 can be + associated to f1 and f2. *) +unification hint 0 ≔ + S1,S2,S3: setoid, f1: S2 → S3, f2: S1 → S2, x:S1, F1: S2 ⤞ S3, F2: S1 ⤞ S2; + f1 ≟ mor_carr … F1, + f2 ≟ mor_carr … F2, + X ≟ comp_morphism … F1 F2 +(* ---------------------------------------- *) ⊢ + f1 (f2 x) ≡ mor_carr … X x. *) + +(* By iterating applications of mor_proper, we can consume the context bit by + bit in order to perform a rewriting. Like in ex2, the script works on any + setoid because it does not reference OPP anywhere. The above theorem on + composition of morphisms justify the correctness of the scripts. *) +example ex3: ∀x,y. x ≃ y → opp (opp (opp x)) ≃ opp (opp (opp y)). + #x #y #EQ @mor_proper @mor_proper @mor_proper @EQ +qed. + +(* We can improve the readability of the previous script by assigning + a notation to mor_proper and by packing together the various applications + of mor_proper and EQ. We pick the prefix symbol †. *) +notation "† c" with precedence 90 for @{'proper $c }. + +interpretation "mor_proper" 'proper c = (mor_proper ????? c). + +example ex3': ∀x,y. x ≃ y → opp (opp (opp x)) ≃ opp (opp (opp y)). + #x #y #EQ @(†(†(†EQ))) +qed. + +(* While the term (†(†(†EQ))) can seem puzzling at first, note that it + closely matches the term (opp (opp (opp x))). Each occurrence of the + unary morphism opp is replaced by † and the occurrence x to be rewritten to y + is replaced by EQ: x ≃ y. Therefore the term (†(†(†EQ))) is a compact + notation to express at once where the rewriting should be performed and + what hypothesis should be used for the rewriting. We will explain now + the problem of rewriting setoid equalities in full generality, and a lightweight + solution to it. *) + +(****** Rewriting setoid equalities *********) + +(* In set theory, once a quotient S/R has been defined, its elements are + compared using the standard equality = whose main property is that of replacing + equals to equals in every context. If E1=E2 then f E1 can be replaced with f E2 + for every context f. Note that f is applied to equivalence classes of elements + of S. Therefore every function and property in f must have been lifted to work + on equivalence classes, and this was possible only if f respected R. + + When using setoids we keep working with elements of S instead of forming a new + type. Therefore, we must deal with contexts f that are not proper. When f is + not proper, f E1 cannot be replaced with f E2 even if E1 ≃ E2. For example, + 〈0,1〉 ≃ 〈1,2〉 but \fst 〈0,1〉 ≠ \fst 〈1,2〉. Therefore every time we want to + rewrite E1 with E2 under the assumption that E1 ≃ E2 we need to prove the + context to be proper. Most of the time the context is just a composition of + morphisms and, like in ex3', the only information that the user needs to + give to the system is the position of the occurrences of E1 to be replaced + and the equations to be used for the rewriting. As for ex3', we can provide + a simple syntax to describe contexts and equations at the same time. The + syntax is just given by a few notations to hide applications of mor_proper, + reflexivity, symmetry and transitivity. + + Here is a synopsis of the syntax: + - †_ to rewrite in the argument of a unary morphism + - _‡_ to rewrite in both arguments of a binary morphism + - # to avoid rewriting in this position + - t to rewrite from left to right in this position using the proof t. + Usually t is the name of an hypothesis in the context of type E1 ≃ E2 + - t^-1 to rewrite from right to left in this position using the proof t. + Concretely, it applies symmetry to t, proving E2 ≃ E1 from E1 ≃ E2. + - ._ to start rewriting when the goal is not an equation ≃. + Concretely, it applies the proof of P E2 → P E1 obtained by splitting + the double implication P E2 ↔ P E1, which is equivalent to P E2 ≃ P E1 + where ≃ is the equality of the PROP setoid. Thus the argument should + be a proof of P E2 ≃ P E1, obtained using the previous symbols according + to the shape of P. + - .=_ to prove an equation G1 ≃ G2 by first rewriting into E1 leaving a new + goal G1' ≃ G2. Concretely, it applies transitivity of ≃. +*) + +notation "l ‡ r" with precedence 90 for @{'proper2 $l $r }. + +interpretation "mor_proper2" 'proper2 x y = (mor_proper ? (function_space ? ?) ?? ? x ?? y). + +notation "#" with precedence 90 for @{'reflex}. + +interpretation "reflexivity" 'reflex = (equiv_refl ???). + +interpretation "symmetry" 'invert r = (equiv_sym ???? r). + +notation ".= r" with precedence 55 for @{'trans $r}. + +interpretation "transitivity" 'trans r = (equiv_trans ????? r ?). + +notation ". r" with precedence 55 for @{'fi $r}. + +definition fi: ∀A,B:Prop. A ≃ B → (B → A) ≝ λA,B,r. proj2 ?? r. + +interpretation "fi" 'fi r = (fi ?? r). + +(* The following example shows several of the features at once: + 1. the first occurrence of x2 is turned into x1 by rewriting the hypothesis + from right to left. + 2. the first occurrence of x1 is turned into x2 by rewriting the hypothesis + from left to right. + 3. the two rewritings are performed at once. + 4. the subterm z+y does not need to be rewritten. Therefore a single # is + used in place of #‡#, which is also correct but produces a larger proof. + 5. we can directly start with an application of ‡ because the goal is a + setoid equality *) +example ex4: ∀x1,x2,y,z:Z. x1 ≃ x2 → + (y + x2) + (x1 + (z + y)) ≃ (y + x1) + (x2 + (z + y)). + #x1 #x2 #y #z #EQ @((#‡EQ^-1)‡(EQ‡#)) +qed. + +(* The following example is just to illustrate the use of .=. We prove the + same statement of ex4, but this time we perform one rewriting at a time. + Note that in an intermediate goal Matita replaces occurrences of Zplus with + occurrences of (the carrier of) ZPLUS. To recover the notation + it is + sufficient to expand the declaration of ZPLUS. *) +example ex5: ∀x1,x2,y,z:Z. x1 ≃ x2 → + (y + x2) + (x1 + (z + y)) ≃ (y + x1) + (x2 + (z + y)). + #x1 #x2 #y #z #EQ @(.=(#‡EQ^-1)‡#) whd in match ZPLUS; @(#‡(EQ‡#)) +qed. + +(* Our last example involves rewriting under a predicate different from ≃. + We first introduce such a predicate over integers. *) +definition is_zero: Z → Prop ≝ λc. \fst c = \snd c. + +definition IS_ZERO: Z ⤞ PROP ≝ mk_morphism … is_zero …. + normalize /3 by conj,injective_plus_r/ +qed. + +unification hint 0 ≔ x:Z ; + X ≟ IS_ZERO +(* ---------------------------------------- *) ⊢ + is_zero x ≡ mor_carr … X x. + +(* We can rewrite under any predicate starting with . *) +example ex6: ∀x,y:Z. x ≃ y → is_zero (x + y) → is_zero (x + x). + #x #y #EQ #H @(.†(#‡EQ)) @H +qed. + +(****** Dependent setoids ********) + +(* A setoid is essentially a type equipped with its own notion of equality. + In a dependent type theory, one expects to be able to both build types (and + setoids) dependent on other types (and setoids). Working with families of + setoids that depend over a plain type --- i.e. not another setoid --- pauses + no additional problem. For example, we can build a setoid out of vectors of + length n assigning to it the type ℕ → setoid. All the machinery for setoids + just introduced keeps working. On the other hand, types that depend over a + setoid require a much more complex machinery and, in practice, it is not + advised to try to work with them in an intentional type theory like the one + of Matita. + + To understand the issue, imagine that we have defined a family of + types I dependent over integers: I: Z → Type. Because 〈0,1〉 and 〈1,2〉 both + represent the same integer +1, the two types I 〈0,1〉 and of I 〈1,2〉 should have + exactly the same inhabitants. However, being different types, their inhabitants + are disjoint. The solution is to equip the type I with a transport function + t: ∀n,m:Z. n ≃ m → I n → I m that maps an element of I n to the corresponding + element of I m. Starting from this idea, the picture quickly becomes complex + when one start considering all the additional equations that the transport + functions should satisfy. For example, if p: n ≃ m, then t … p (t … p^-1 x) = x, + i.e. the element in I n corresponding to the element in I m that corresponds to + x in I n should be exactly x. Moreover, for any function f: ∀n. I n → T n for + some other type T dependent over n the following equation should hold: + f … (t … p x) = t … p (f … x) (i.e. transporting and applying f should commute + because f should be insensitive too up to ≃ to the actual representation of the + integral indexes). *) + +(****** Avoiding setoids *******) + +(* Quotients are used pervasively in mathematics. In many practical situations, + for example when dealing with finite objects like pairs of naturals, an unique + representation can be imposed, for example by introducing a normalization + procedure to be called after every operation. For example, integer numbers can + be normalized to either 〈0,n〉 or 〈n,0〉. Or they can be represented as either 0 + or a non zero number, with the latter being encoded by a boolean (the sign) and + a natural (the predecessor of the absolute value). For example, -3 would be + represented by NonZero 〈false,2〉, +3 by NonZero 〈true,2〉 and 0 by Zero. + Rational numbers n/m can be put in normal form by dividing both n and m by their + greatest common divisor, or by picking n=0, m=1 when n is 0. These normal form + is an unique representation. + + Imposing an unique representation is not always possible. For example, picking + a canonical representative for a Cauchy sequence is not a computable operation. + Nevertheless, when possible, avoiding setoids is preferrable: + 1) when the Leibniz equality is used, replacing n with m knowing n=m does not + require any proof of properness + 2) at the moment automation in Matita is only available for Leibniz equalities. + By switching to setoids less proofs are automatically found + 3) types dependent over plain types do not need ad-hoc transport functions + because the rewriting principle for Leibniz equality plays that role and + already satisfies for free all required equations + 4) normal forms are usually smaller than other forms. By sticking to normal + forms both the memory consumption and the computational cost of operations + may be reduced. *) \ No newline at end of file