weblib/lroversi/setoids.ma

   1
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "higher_order_defs/relations.ma".
  16 include "logic/coimplication.ma".
  17
  18 (* definition of a =_ID b. What is "break"? *)
  19 notation "hvbox(a break = \sub \ID b)"
  20   non associative with precedence 45
  21   for @{ 'eqID $a $b }.
  22
  23 (* LR: Which is the difference with the notation just defined here above?
  24        Doesn't the above notation become useless after the following one?
  25    CSC: "notation" is a notation used both in input and in output;
  26         "notation >" is used only in input. It is also given since it is
  27         more compact to write *)
  28 notation > "hvbox(a break =_\ID b)"
  29   non associative with precedence 45
  30   for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
  31
  32 (* Association of the notation a =_ID b to Leibniz equivalence
  33    "cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b" ? *)
  34 interpretation "ID eq" 'eqID x y =
  35   (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
  36
  37 (* An arbitrary equivalence relation is a relation on a type A which is
  38    refl, sym, trans *)
  39 record equivalence_relation (A:Type) : Type ≝
  40  { eq_rel:2> A → A → Prop;
  41    refl: reflexive ? eq_rel;
  42    sym: symmetric ? eq_rel;
  43    trans: transitive ? eq_rel
  44  }.
  45
  46 (* A setoid is weaker than a set meaning that it is based on a generic
  47    equivalence relation which is not necessarily Leibnitz relation *)
  48 record setoid : Type ≝
  49  { carr:> Type;
  50    eq: equivalence_relation carr
  51  }.
  52
  53 (* LR: Definition of a = b to denote the equivalence relation on a setoid.
  54        a = b stands for
  55        ????????????????
  56        I cannot read the meaning of  "eq_rel ? (eq ?) $a $b".
  57        "eq" should be defined in "setoid" and
  58        "eq_rel" in "equivalence_relation".
  59        If this is true I cannot justify why "eq_rel" can have 4 arguments.
  60    CSC: Take the setoid
  61            S := { carr = T; eq = { eq_rel = # : T -> T -> Prop; ... }}
  62         a = b  stands for  (eq_rel ? (eq ?) a b)
  63         which is understood as (eq_rel T (eq S) a b) where a,b:T.
  64
  65         eq_rel has four arguments since its type is:
  66            ∀ A:Type. setoid A → A → A → Prop
  67         in general all projections of a record are also quantified over the
  68         parameters of the record (here A) and the record itself (here"setoid A)"
  69 *)
  70 notation > "hvbox(a break = b)"
  71   non associative with precedence 45
  72   for @{ eq_rel ? (eq ?) $a $b }.
  73 interpretation "eq setoid"
  74    'eq t x y = (eq_rel ? (eq t) x y). (* eq ?: ? → ? → Prop*)
  75 interpretation "setoid symmetry"
  76    'invert r = (sym ???? r). (* *)
  77
  78 (* LR: Why is .= linked to "trans"?
  79    CSC: Suppose your goal is a=b and
  80         suppose you want to prove your goal using a lemma that
  81         proves a = a' to obtain a new goal a' = b
  82         (i.e. you want to rewrite in the l.h.s. of the equation).
  83
  84         This is possible since = is transitive, i.e.
  85         trans: ∀A.(setoid A) → (∀a,a',b. a=a' → a'=b → a=b)
  86
  87         Hence, to perform the rewriting using the lemma r: a=a' it is
  88         sufficient to apply  (trans ????? r ?)  (the last question mark is
  89         added automatically by apply and it is the goal that remains open).
  90 *)
  91 notation ".= r"
  92    with precedence 50
  93    for @{'trans $r}.
  94 interpretation "trans"
  95   'trans r = (trans ????? r).
  96
  97 (* Notations associated to binary_morphism which ensures
  98    a function fun1: A → B is a morphism w.r.t. the equivalence
  99    relation eq *)
 100 record unary_morphism (A,B: setoid) : Type ≝
 101  { fun1:1> A → B;
 102    prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
 103  }.
 104 (* Notation † c associated to the whole prop1 where c is a
 105    Prop, namely a statement that establishes the equality
 106    between two elements of the (carrier) of a setoid *)
 107 notation "† c"
 108    with precedence 90 for @{'prop1 $c }.
 109 interpretation "prop1"
 110    'prop1 c  = (prop1 ????? c).
 111 (* Notation B:setoid ⇒ C:setoid associated to
 112    the whole structure unary_morphism *)
 113 notation "B ⇒ C" right associative
 114    with precedence 72
 115    for @{'unary_morphism $B $C}.
 116 interpretation "'unary_morphism"
 117    'unary_morphism A B = (unary_morphism A B).
 118
 119 (* Notations associated to binary_morphism which ensures
 120    a function fun2: A → B → C is a morphism w.r.t. the equivalence
 121    relation eq *)
 122 record binary_morphism (A,B,C:setoid) : Type ≝
 123  { fun2:2> A → B → C;
 124    prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
 125  }.
 126 (* Notation l ‡ r  associated to the whole prop2 where l and r are
 127    two Prop, namely two statements that establish the equality
 128    between two elements of the (carrier) of a setoid *)
 129 notation "l ‡ r"
 130    with precedence 90 for @{'prop2 $l $r }.
 131 interpretation "prop2"
 132   'prop2 l r = (prop2 ???????? l r).
 133 (* Notation A:setoid × B:setoid ⇒ C:setoid
 134    associated to the whole structure binary_morphism *)
 135 notation "A × term 74 B ⇒ term 19 C"
 136    non associative with precedence 72
 137    for @{'binary_morphism $A $B $C}.
 138 interpretation "'binary_morphism0"
 139    'binary_morphism A B C = (binary_morphism A B C).
 140 (* Notation that abbreviates the statement "is reflexive"
 141    relatively to an equivalence relation of a setoid *)
 142 notation "#"
 143    with precedence 90 for @{'refl}. (**)
 144 interpretation "refl" 'refl = (refl ???).
 145
 146 definition if: ∀A,B. (A \liff B) → A → B.
 147 (* CSC's original proof: intros; cases H; autobatch. *)
 148 (* LR's "alternative" one to learn: *)
 149 intros; cases H; clear H; clear H3; apply H2; clear H2; apply H1.
 150 qed.
 151
 152 definition fi: ∀A,B. (A \liff B) → B → A.
 153  intros; cases H; autobatch.
 154 qed.
 155
 156 (* LR: The definition of PROP is an "exercise" that allows to formalize
 157        the idea that the set Prop of proposition in Matita together
 158        with the bi-implication Iff, which is an equivalence relation
 159        among p∈Prop form a setoid.
 160
 161        Specifically, PROP is such that: *)
 162 definition PROP: setoid.
 163  constructor 1;
 164   [ apply Prop (* the carrier of PROP is the set of propositions *)
 165   | constructor 1; (* the equivalence relation is *)
 166      [ apply Iff   (* the bi-implication that holds on Prop,
 167                       which is defined in "logic/coimplication.ma" and
 168                       which we can prove to be: *)
 169      | intros 1; split; intro; assumption (* reflexive *)
 170      | intros 3; cases H; split; assumption (* symmetric *)
 171      | intros 5; cases H; cases H1; split; intro;
 172      autobatch (* transitive *)
 173   ]] qed.
 174
 175 definition fi': ∀A,B:PROP. A=B → B → A ≝ fi.
 176
 177 notation ". r"
 178    with precedence 50 for @{'fi $r}.
 179 interpretation "fi"
 180   'fi r = (fi' ?? r).
 181
 182 definition and_morphism: PROP × PROP ⇒ PROP.
 183  constructor 1;
 184   [ apply And (* LR: It's a bit obscure the reason why
 185                      And: Prop → Prop → Prop  can be used here
 186                      where PROP → PROP → PROP is required *)
 187   | intros; split; intro; whd in H H1; elim H; elim H1; elim H2; autobatch ]
 188 qed.
 189
 190 interpretation "and_morphism"
 191   'and a b = (fun2 ??? and_morphism a b).
 192
 193 definition or_morphism: PROP × PROP ⇒ PROP.
 194  constructor 1;
 195   [ apply Or
 196   | intros; split; intro; elim H; elim H1; elim H2; autobatch ]
 197 qed.
 198
 199 interpretation "or_morphism"
 200   'or a b = (fun2 ??? or_morphism a b).
 201
 202 definition if_morphism: PROP × PROP ⇒ PROP.
 203  constructor 1;
 204   [ apply (λA,B. A → B)
 205   | normalize; intros; elim H; elim H1; split; intros; autobatch depth=4 ]
 206 qed.
 207
 208 (* LR: Added by me just as a curiosity. *)
 209 interpretation "if_morphism"
 210   'if a b = (fun2 ??? if_morphism a b).