]> matita.cs.unibo.it Git - helm.git/blob - weblib/lroversi/setoids.ma
New implementation of lpo (the previous one was sometimes expnential)
[helm.git] / 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).