--- /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 "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).
projects / helm.git / commitdiff