From: matitaweb Date: Wed, 12 Oct 2011 13:52:23 +0000 (+0000) Subject: commit by user lroversi X-Git-Tag: make_still_working~2200 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e55edd820bb75b0e20d67b57d6d09977e5d7b3ab;p=helm.git commit by user lroversi --- diff --git a/weblib/lroversi/prova.ma b/weblib/lroversi/prova.ma new file mode 100644 index 000000000..e69de29bb diff --git a/weblib/lroversi/setoids.ma b/weblib/lroversi/setoids.ma new file mode 100644 index 000000000..730ca5805 --- /dev/null +++ b/weblib/lroversi/setoids.ma @@ -0,0 +1,210 @@ + +(* ___ *) +(* ||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 "higher_order_defs/relations.ma". +include "logic/coimplication.ma". + +(* definition of a =_ID b. What is "break"? *) +notation "hvbox(a break = \sub \ID b)" + non associative with precedence 45 + for @{ 'eqID $a $b }. + +(* LR: Which is the difference with the notation just defined here above? + Doesn't the above notation become useless after the following one? + CSC: "notation" is a notation used both in input and in output; + "notation >" is used only in input. It is also given since it is + more compact to write *) +notation > "hvbox(a break =_\ID b)" + non associative with precedence 45 + for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }. + +(* Association of the notation a =_ID b to Leibniz equivalence + "cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b" ? *) +interpretation "ID eq" 'eqID x y = + (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y). + +(* An arbitrary equivalence relation is a relation on a type A which is + refl, sym, trans *) +record equivalence_relation (A:Type) : Type ≝ + { eq_rel:2> A → A → Prop; + refl: reflexive ? eq_rel; + sym: symmetric ? eq_rel; + trans: transitive ? eq_rel + }. + +(* A setoid is weaker than a set meaning that it is based on a generic + equivalence relation which is not necessarily Leibnitz relation *) +record setoid : Type ≝ + { carr:> Type; + eq: equivalence_relation carr + }. + +(* LR: Definition of a = b to denote the equivalence relation on a setoid. + a = b stands for + ???????????????? + I cannot read the meaning of "eq_rel ? (eq ?) $a $b". + "eq" should be defined in "setoid" and + "eq_rel" in "equivalence_relation". + If this is true I cannot justify why "eq_rel" can have 4 arguments. + CSC: Take the setoid + S := { carr = T; eq = { eq_rel = # : T -> T -> Prop; ... }} + a = b stands for (eq_rel ? (eq ?) a b) + which is understood as (eq_rel T (eq S) a b) where a,b:T. + + eq_rel has four arguments since its type is: + ∀ A:Type. setoid A → A → A → Prop + in general all projections of a record are also quantified over the + parameters of the record (here A) and the record itself (here"setoid A)" +*) +notation > "hvbox(a break = b)" + non associative with precedence 45 + for @{ eq_rel ? (eq ?) $a $b }. +interpretation "eq setoid" + 'eq t x y = (eq_rel ? (eq t) x y). (* eq ?: ? → ? → Prop*) +interpretation "setoid symmetry" + 'invert r = (sym ???? r). (* *) + +(* LR: Why is .= linked to "trans"? + CSC: Suppose your goal is a=b and + suppose you want to prove your goal using a lemma that + proves a = a' to obtain a new goal a' = b + (i.e. you want to rewrite in the l.h.s. of the equation). + + This is possible since = is transitive, i.e. + trans: ∀A.(setoid A) → (∀a,a',b. a=a' → a'=b → a=b) + + Hence, to perform the rewriting using the lemma r: a=a' it is + sufficient to apply (trans ????? r ?) (the last question mark is + added automatically by apply and it is the goal that remains open). +*) +notation ".= r" + with precedence 50 + for @{'trans $r}. +interpretation "trans" + 'trans r = (trans ????? r). + +(* Notations associated to binary_morphism which ensures + a function fun1: A → B is a morphism w.r.t. the equivalence + relation eq *) +record unary_morphism (A,B: setoid) : Type ≝ + { fun1:1> A → B; + prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a') + }. +(* Notation † c associated to the whole prop1 where c is a + Prop, namely a statement that establishes the equality + between two elements of the (carrier) of a setoid *) +notation "† c" + with precedence 90 for @{'prop1 $c }. +interpretation "prop1" + 'prop1 c = (prop1 ????? c). +(* Notation B:setoid ⇒ C:setoid associated to + the whole structure unary_morphism *) +notation "B ⇒ C" right associative + with precedence 72 + for @{'unary_morphism $B $C}. +interpretation "'unary_morphism" + 'unary_morphism A B = (unary_morphism A B). + +(* Notations associated to binary_morphism which ensures + a function fun2: A → B → C is a morphism w.r.t. the equivalence + relation eq *) +record binary_morphism (A,B,C:setoid) : Type ≝ + { fun2:2> A → B → C; + prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b') + }. +(* Notation l ‡ r associated to the whole prop2 where l and r are + two Prop, namely two statements that establish the equality + between two elements of the (carrier) of a setoid *) +notation "l ‡ r" + with precedence 90 for @{'prop2 $l $r }. +interpretation "prop2" + 'prop2 l r = (prop2 ???????? l r). +(* Notation A:setoid × B:setoid ⇒ C:setoid + associated to the whole structure binary_morphism *) +notation "A × term 74 B ⇒ term 19 C" + non associative with precedence 72 + for @{'binary_morphism $A $B $C}. +interpretation "'binary_morphism0" + 'binary_morphism A B C = (binary_morphism A B C). +(* Notation that abbreviates the statement "is reflexive" + relatively to an equivalence relation of a setoid *) +notation "#" + with precedence 90 for @{'refl}. (**) +interpretation "refl" 'refl = (refl ???). + +definition if: ∀A,B. (A \liff B) → A → B. +(* CSC's original proof: intros; cases H; autobatch. *) +(* LR's "alternative" one to learn: *) +intros; cases H; clear H; clear H3; apply H2; clear H2; apply H1. +qed. + +definition fi: ∀A,B. (A \liff B) → B → A. + intros; cases H; autobatch. +qed. + +(* LR: The definition of PROP is an "exercise" that allows to formalize + the idea that the set Prop of proposition in Matita together + with the bi-implication Iff, which is an equivalence relation + among p∈Prop form a setoid. + + Specifically, PROP is such that: *) +definition PROP: setoid. + constructor 1; + [ apply Prop (* the carrier of PROP is the set of propositions *) + | constructor 1; (* the equivalence relation is *) + [ apply Iff (* the bi-implication that holds on Prop, + which is defined in "logic/coimplication.ma" and + which we can prove to be: *) + | intros 1; split; intro; assumption (* reflexive *) + | intros 3; cases H; split; assumption (* symmetric *) + | intros 5; cases H; cases H1; split; intro; + autobatch (* transitive *) + ]] qed. + +definition fi': ∀A,B:PROP. A=B → B → A ≝ fi. + +notation ". r" + with precedence 50 for @{'fi $r}. +interpretation "fi" + 'fi r = (fi' ?? r). + +definition and_morphism: PROP × PROP ⇒ PROP. + constructor 1; + [ apply And (* LR: It's a bit obscure the reason why + And: Prop → Prop → Prop can be used here + where PROP → PROP → PROP is required *) + | intros; split; intro; whd in H H1; elim H; elim H1; elim H2; autobatch ] +qed. + +interpretation "and_morphism" + 'and a b = (fun2 ??? and_morphism a b). + +definition or_morphism: PROP × PROP ⇒ PROP. + constructor 1; + [ apply Or + | intros; split; intro; elim H; elim H1; elim H2; autobatch ] +qed. + +interpretation "or_morphism" + 'or a b = (fun2 ??? or_morphism a b). + +definition if_morphism: PROP × PROP ⇒ PROP. + constructor 1; + [ apply (λA,B. A → B) + | normalize; intros; elim H; elim H1; split; intros; autobatch depth=4 ] +qed. + +(* LR: Added by me just as a curiosity. *) +interpretation "if_morphism" + 'if a b = (fun2 ??? if_morphism a b).