--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
projects / helm.git / commitdiff