]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/technicalities/setoids.ma
...
[helm.git] / helm / software / matita / library / technicalities / setoids.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti. C.Sacerdoti Coen.                          *)
8 (*      ||A||       E.Tassi. S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
16 (* Original author: Claudio Sacerdoti Coen. for the Coq system       *)
17
18 include "datatypes/constructors.ma".
19 include "logic/coimplication.ma".
20 include "logic/connectives2.ma".
21
22 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
23
24 (* X will be used to distinguish covariant arguments whose type is an   *)
25 (* Asymmetric* relation from contravariant arguments of the same type *)
26 inductive X_Relation_Class (X: Type) : Type ≝
27    SymmetricReflexive :
28      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → X_Relation_Class X
29  | AsymmetricReflexive : X → ∀A,Aeq. reflexive A Aeq → X_Relation_Class X
30  | SymmetricAreflexive : ∀A,Aeq. symmetric A Aeq → X_Relation_Class X
31  | AsymmetricAreflexive : X → ∀A.∀Aeq : relation A. X_Relation_Class X
32  | Leibniz : Type → X_Relation_Class X.
33
34 inductive variance : Set ≝
35    Covariant : variance
36  | Contravariant : variance.
37
38 definition Argument_Class ≝ X_Relation_Class variance.
39 definition Relation_Class ≝ X_Relation_Class unit.
40
41 inductive Reflexive_Relation_Class : Type :=
42    RSymmetric :
43      ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
44  | RAsymmetric :
45      ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
46  | RLeibniz : Type → Reflexive_Relation_Class.
47
48 inductive Areflexive_Relation_Class  : Type :=
49  | ASymmetric : ∀A,Aeq. symmetric A Aeq → Areflexive_Relation_Class
50  | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
51
52 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
53  intros (a); cases a;
54   [ apply (SymmetricReflexive ? ? ? H H1)
55   | apply (AsymmetricReflexive ? something ? ? H)
56   | apply (SymmetricAreflexive ? ? ? H)
57   | apply (AsymmetricAreflexive ? something ? r)
58   | apply (Leibniz ? T)
59   ]
60 qed.
61
62 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
63  intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
64 qed.
65
66 definition relation_of_relation_class:
67  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
68 intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
69 qed.
70
71 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
72  ∀R.
73   carrier_of_relation_class ? (relation_class_of_argument_class R) =
74    carrier_of_relation_class ? R.
75 intro; cases R; reflexivity.
76 qed.
77
78 inductive nelistT (A : Type) : Type :=
79    singl : A → nelistT A
80  | cons : A → nelistT A → nelistT A.
81
82 definition Arguments := nelistT Argument_Class.
83
84 definition function_type_of_morphism_signature :
85  Arguments → Relation_Class → Type.
86   intros (In Out); elim In; 
87   [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
88   | exact (carrier_of_relation_class ? a → T)
89   ]
90 qed. 
91
92 definition make_compatibility_goal_aux:
93  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
94  intros 2; 
95  elim In (a); simplify in f f1;
96  generalize in match f1; clear f1;
97  generalize in match f; clear f;
98   [ elim a; simplify in f f1;
99      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
100      | cases x;
101         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
102         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
103         ]
104      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
105      | cases x;
106         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
107         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
108         ]
109      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
110      ]
111   | change with
112      ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
113       (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
114       Prop).
115     elim a; simplify in f f1;
116      [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
117      |2,4: cases x;
118         [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
119         |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
120         ]
121      | exact (∀x. R (f x) (f1 x))
122      ]
123   ]
124 qed. 
125
126 definition make_compatibility_goal :=
127  λIn,Out,f. make_compatibility_goal_aux In Out f f.
128
129 record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
130  { Function : function_type_of_morphism_signature In Out;
131    Compat : make_compatibility_goal In Out Function
132  }.
133
134 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
135  intro;
136  elim n;
137   [ apply (singl ? (Leibniz ? a))
138   | apply (cons ? (Leibniz ? a) a1)
139   ]
140 qed.
141
142 (* every function is a morphism from Leibniz+ to Leibniz *)
143 definition morphism_theory_of_function :
144  ∀In: nelistT Type.∀Out: Type.
145   let In' := list_of_Leibniz_of_list_of_types In in
146   let Out' := Leibniz ? Out in
147    function_type_of_morphism_signature In' Out' →
148     Morphism_Theory In' Out'.
149   intros;
150   apply (mk_Morphism_Theory ? ? f);
151   unfold In' in f ⊢ %; clear In';
152   unfold Out' in f ⊢ %; clear Out';
153   generalize in match f; clear f;
154   elim In;
155    [ unfold make_compatibility_goal;
156      whd; intros;
157      reflexivity
158    | simplify;
159      intro;
160      unfold In' in f;
161      unfold Out' in f;
162      exact (H (f1 x))
163    ]
164 qed.
165
166 (* THE iff RELATION CLASS *)
167
168 definition Iff_Relation_Class : Relation_Class.
169  apply (SymmetricReflexive unit ? iff);
170   [ exact symmetric_iff
171   | exact reflexive_iff
172   ]
173 qed.
174
175 (* THE impl RELATION CLASS *)
176
177 definition impl \def \lambda A,B:Prop. A → B.
178
179 theorem impl_refl: reflexive ? impl.
180  unfold reflexive;
181  intros;
182  unfold impl;
183  intro;
184  assumption.
185 qed.
186
187 definition Impl_Relation_Class : Relation_Class.
188  unfold Relation_Class;
189  apply (AsymmetricReflexive unit something ? impl);
190  exact impl_refl.
191 qed.
192
193 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
194
195 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
196  ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq.
197   let ASetoidClass := SymmetricAreflexive ? ? ? sym in
198    (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass))
199      Iff_Relation_Class).
200  intros;
201  apply mk_Morphism_Theory;
202   [ exact Aeq
203   | unfold make_compatibility_goal;
204     simplify; unfold ASetoidClass; simplify;
205     intros;
206     split;
207     unfold transitive in H;
208     unfold symmetric in sym;
209     intro;
210       [ apply (H x2 x1 x3 ? ?);
211           [apply (sym x1 x2 ?).
212            apply (H1).
213           |apply (H x1 x x3 ? ?);
214             [apply (H3).
215             |apply (H2).
216             ]
217           ]
218       | apply (H x1 x3 x ? ?);
219          [apply (H x1 x2 x3 ? ?);
220             [apply (H1).
221             |apply (H3).
222             ]
223          |apply (sym x x3 ?).
224           apply (H2).
225          ]
226       ]
227   ].
228 qed.
229
230 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
231  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq.
232   ∀trans: transitive ? Aeq.
233    let ASetoidClass := SymmetricReflexive ? ? ? sym refl in
234     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
235  intros;
236  apply mk_Morphism_Theory;
237  normalize;
238   [ exact Aeq
239   | intros;
240     split;
241     intro;
242     unfold transitive in H;
243     unfold symmetric in sym;
244     [ apply (H x2 x1 x3 ? ?);
245         [apply (sym x1 x2 ?).
246          apply (H1).
247         |apply (H x1 x x3 ? ?);
248           [apply (H3).
249           |apply (H2).
250           ]
251         ]
252     | apply (H x1 x2 x ? ?);
253       [apply (H1).
254       |apply (H x2 x3 x ? ?);
255         [apply (H3).
256         |apply (sym x x3 ?).
257          apply (H x x3 x3 ? ?);
258           [apply (H2).
259           |apply (refl x3).
260           ]
261         ]
262       ]
263     ]
264   ]
265 qed.
266
267 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
268  ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
269   let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
270   let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
271    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
272  intros;
273  apply mk_Morphism_Theory;
274  [ simplify;
275    apply Aeq
276  | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
277    intros;
278    whd;
279    intros;
280    apply (H x2 x1 x3 ? ?);
281     [apply (H1).
282     |apply (H x1 x x3 ? ?);
283       [apply (H3).
284       |apply (H2).
285       ]
286     ]
287  ].
288 qed.
289
290 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
291  ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
292   let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
293   let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
294    (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
295  intros;
296  apply mk_Morphism_Theory;
297  [ simplify;
298    apply Aeq
299  | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
300    intros;
301    whd;
302    intro;
303    apply (H x2 x1 x3 ? ?);
304      [apply (H1).
305      |apply (H x1 x x3 ? ?);
306        [apply (H3).
307        |apply (H2).
308        ]
309      ]
310  ].
311 qed.
312
313 (* iff AS A RELATION *)
314
315 (*DA PORTARE:Add Relation Prop iff
316  reflexivity proved by iff_refl
317  symmetry proved by iff_sym
318  transitivity proved by iff_trans
319  as iff_relation.*)
320
321 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
322 definition morphism_theory_of_predicate :
323  ∀(In: nelistT Type).
324   let In' := list_of_Leibniz_of_list_of_types In in
325    function_type_of_morphism_signature In' Iff_Relation_Class →
326     Morphism_Theory In' Iff_Relation_Class.
327   intros;
328   apply mk_Morphism_Theory;
329   [ apply f
330   | generalize in match f; clear f;
331     unfold In'; clear In';
332     elim In;
333      [ normalize;
334        intro;
335        apply iff_refl
336      | simplify;
337        intro x;
338        apply (H (f1 x))
339      ]
340   ].
341 qed.
342
343 (* impl AS A RELATION *)
344
345 theorem impl_trans: transitive ? impl.
346  whd;
347  unfold impl;
348  intros;
349  apply (H1 ?).apply (H ?).apply (H2).
350  autobatch.
351 qed.
352
353 (*DA PORTARE: Add Relation Prop impl
354  reflexivity proved by impl_refl
355  transitivity proved by impl_trans
356  as impl_relation.*)
357
358 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
359
360 inductive rewrite_direction : Type :=
361    Left2Right: rewrite_direction
362  | Right2Left: rewrite_direction.
363
364 definition variance_of_argument_class : Argument_Class → option variance.
365  intros;
366  elim a;
367   [ apply None
368   | apply (Some ? x)
369   | apply None
370   | apply (Some ? x)
371   | apply None
372   ]
373 qed.
374
375 definition opposite_direction :=
376  λdir.
377    match dir with
378     [ Left2Right ⇒ Right2Left
379     | Right2Left ⇒ Left2Right
380     ].
381
382 lemma opposite_direction_idempotent:
383  ∀dir. opposite_direction (opposite_direction dir) = dir.
384   intros;
385   elim dir;
386   reflexivity.
387 qed.
388
389 inductive check_if_variance_is_respected :
390  option variance → rewrite_direction → rewrite_direction →  Prop
391 :=
392    MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
393  | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
394  | MSContravariant :
395      ∀dir.
396       check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
397
398 definition relation_class_of_reflexive_relation_class:
399  Reflexive_Relation_Class → Relation_Class.
400  intro;
401  elim r;
402   [ apply (SymmetricReflexive ? ? ? H H1)
403   | apply (AsymmetricReflexive ? something ? ? H)
404   | apply (Leibniz ? T)
405   ]
406 qed.
407
408 definition relation_class_of_areflexive_relation_class:
409  Areflexive_Relation_Class → Relation_Class.
410  intro;
411  elim a;
412   [ apply (SymmetricAreflexive ? ? ? H)
413   | apply (AsymmetricAreflexive ? something ? r)
414   ]
415 qed.
416
417 definition carrier_of_reflexive_relation_class :=
418  λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
419
420 definition carrier_of_areflexive_relation_class :=
421  λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
422
423 definition relation_of_areflexive_relation_class :=
424  λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
425
426 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction →  Type :=
427     App :
428       ∀In,Out,dir'.
429         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
430            Morphism_Context Hole dir Out dir'
431   | ToReplace : Morphism_Context Hole dir Hole dir
432   | ToKeep :
433      ∀S,dir'.
434       carrier_of_reflexive_relation_class S →
435         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
436  | ProperElementToKeep :
437      ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
438       relation_of_areflexive_relation_class S x x →
439         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
440 with Morphism_Context_List :
441    rewrite_direction → Arguments → Type
442 :=
443     fcl_singl :
444       ∀S,dir',dir''.
445        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
446         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
447          Morphism_Context_List Hole dir dir'' (singl ? S)
448  | fcl_cons :
449       ∀S,L,dir',dir''.
450        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
451         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
452          Morphism_Context_List Hole dir dir'' L →
453           Morphism_Context_List Hole dir dir'' (cons ? S L).
454
455 lemma Morphism_Context_rect2:
456  ∀Hole,dir.
457  ∀P:
458   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
459  ∀P0:
460   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
461  (∀In,Out,dir'.
462    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
463     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
464  P Hole dir (ToReplace Hole dir) →
465  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
466    P (relation_class_of_reflexive_relation_class S) dir'
467     (ToKeep Hole dir S dir' c)) →
468  (∀S:Areflexive_Relation_Class.∀dir'.
469    ∀x:carrier_of_areflexive_relation_class S.
470     ∀r:relation_of_areflexive_relation_class S x x.
471      P (relation_class_of_areflexive_relation_class S) dir'
472       (ProperElementToKeep Hole dir S dir' x r)) →
473  (∀S:Argument_Class.∀dir',dir''.
474    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
475     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
476      P (relation_class_of_argument_class S) dir' m ->
477       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
478  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
479    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
480     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
481      P (relation_class_of_argument_class S) dir' m →
482       ∀m0:Morphism_Context_List Hole dir dir'' L.
483        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
484  ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
485   P r r0 m
486
487  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
488  let rec
489   F (rc:Relation_Class) (r0:rewrite_direction)
490    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
491  ≝
492   match m return λrc.λr0.λm0.P rc r0 m0 with
493   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
494   | ToReplace ⇒ f0
495   | ToKeep S dir' c ⇒ f1 S dir' c
496   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
497   ]
498  and
499   F0 (r:rewrite_direction) (a:Arguments)
500    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
501  ≝
502   match m return λr.λa.λm0.P0 r a m0 with
503   [ fcl_singl S dir' dir'' c m0 ⇒
504       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
505   | fcl_cons S L dir' dir'' c m0 m1 ⇒
506       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
507         m1 (F0 dir'' L m1)
508   ]
509 in F.
510
511 lemma Morphism_Context_List_rect2:
512  ∀Hole,dir.
513  ∀P:
514   ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
515  ∀P0:
516   ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
517  (∀In,Out,dir'.
518    ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
519     P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
520  P Hole dir (ToReplace Hole dir) →
521  (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
522    P (relation_class_of_reflexive_relation_class S) dir'
523     (ToKeep Hole dir S dir' c)) →
524  (∀S:Areflexive_Relation_Class.∀dir'.
525    ∀x:carrier_of_areflexive_relation_class S.
526     ∀r:relation_of_areflexive_relation_class S x x.
527      P (relation_class_of_areflexive_relation_class S) dir'
528       (ProperElementToKeep Hole dir S dir' x r)) →
529  (∀S:Argument_Class.∀dir',dir''.
530    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
531     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
532      P (relation_class_of_argument_class S) dir' m ->
533       P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
534  (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
535    ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
536     ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
537      P (relation_class_of_argument_class S) dir' m →
538       ∀m0:Morphism_Context_List Hole dir dir'' L.
539        P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
540  ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
541   P0 r a m
542
543  λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
544  let rec
545   F (rc:Relation_Class) (r0:rewrite_direction)
546    (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
547  ≝
548   match m return λrc.λr0.λm0.P rc r0 m0 with
549   [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
550   | ToReplace ⇒ f0
551   | ToKeep S dir' c ⇒ f1 S dir' c
552   | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
553   ]
554  and
555   F0 (r:rewrite_direction) (a:Arguments)
556    (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
557  ≝
558   match m return λr.λa.λm0.P0 r a m0 with
559   [ fcl_singl S dir' dir'' c m0 ⇒
560       f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
561   | fcl_cons S L dir' dir'' c m0 m1 ⇒
562       f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
563         m1 (F0 dir'' L m1)
564   ]
565 in F0.
566
567 definition product_of_arguments : Arguments → Type.
568  intro;
569  elim a;
570   [ apply (carrier_of_relation_class ? a1)
571   | apply (Prod (carrier_of_relation_class ? a1) T)
572   ]
573 qed.
574
575 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
576  intros (dir R);
577  cases (variance_of_argument_class R) (a);
578   [ exact dir
579   | cases a;
580      [ exact dir                      (* covariant *)
581      | exact (opposite_direction dir) (* contravariant *)
582      ]
583   ]
584 qed.
585
586 definition directed_relation_of_relation_class:
587  ∀dir:rewrite_direction.∀R: Relation_Class.
588    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
589  intros;
590  cases r;
591   [ exact (relation_of_relation_class ? ? c c1)
592   | apply (relation_of_relation_class ? ? c1 c)
593   ]
594 qed.
595
596 definition directed_relation_of_argument_class:
597  ∀dir:rewrite_direction.∀R: Argument_Class.
598    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
599   intros (dir R c c1);
600   rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class R) in c c1;
601   exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)  c c1).
602 qed.
603
604
605 definition relation_of_product_of_arguments:
606  ∀dir:rewrite_direction.∀In.
607   product_of_arguments In → product_of_arguments In → Prop.
608  intros 2;
609  elim In 0;
610   [ simplify;
611     intro;
612     exact (directed_relation_of_argument_class (get_rewrite_direction r a) a)
613   | intros;
614     change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
615     change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
616     cases p (c p2);
617     cases p1 (c1 p3);
618    apply And;
619     [ exact
620       (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
621     | exact (R p2 p3)
622     ]
623   ]
624 qed. 
625
626 definition apply_morphism:
627  ∀In,Out.∀m: function_type_of_morphism_signature In Out.
628   ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
629  intro;
630  elim In;
631   [ exact (f p)
632   | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
633    elim p;
634    change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out);
635    exact (f ? (f1 a1) b)
636   ]
637 qed.
638
639 theorem apply_morphism_compatibility_Right2Left:
640  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
641   ∀args1,args2: product_of_arguments In.
642      make_compatibility_goal_aux ? ? m1 m2 →
643       relation_of_product_of_arguments Right2Left ? args1 args2 →
644         directed_relation_of_relation_class Right2Left ?
645          (apply_morphism ? ? m2 args1)
646          (apply_morphism ? ? m1 args2).
647   intro;
648   elim In;
649    [ simplify in m1 m2 args1 args2 ⊢ %;
650      change in H1 with
651       (directed_relation_of_argument_class
652         (get_rewrite_direction Right2Left a) a args1 args2);
653      generalize in match H1; clear H1;
654      generalize in match H; clear H;
655      generalize in match args2; clear args2;
656      generalize in match args1; clear args1;
657      generalize in match m2; clear m2;
658      generalize in match m1; clear m1;
659      elim a 0; simplify;
660       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
661         apply H;
662         exact H1
663       | intros 8 (v T1 r Hr m1 m2 args1 args2);
664         cases v; 
665         simplify;
666         intros (H H1);
667         apply (H ? ? H1);
668       | intros;
669         apply H1;
670         exact H2
671       | intros 7 (v);
672         cases v; simplify;
673         intros (H H1);
674         apply H;
675         exact H1
676       | intros;
677         simplify in H1;
678         rewrite > H1;
679         apply H;
680         exact H1
681       ]
682    | change in m1 with
683       (carrier_of_relation_class variance a →
684         function_type_of_morphism_signature n Out);
685      change in m2 with
686       (carrier_of_relation_class variance a →
687         function_type_of_morphism_signature n Out);
688      change in args1 with
689       ((carrier_of_relation_class ? a) × (product_of_arguments n));
690      change in args2 with
691       ((carrier_of_relation_class ? a) × (product_of_arguments n));
692      generalize in match H2; clear H2;
693      elim args2 0; clear args2;
694      elim args1; clear args1;
695      simplify in H2;
696      change in H2:(? ? %) with 
697        (relation_of_product_of_arguments Right2Left n b b1);
698      elim H2; clear H2;
699      change with
700       (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1)
701         (apply_morphism n Out (m2 a1) b));
702      generalize in match H3; clear H3;
703      generalize in match a1; clear a1;
704      generalize in match a2; clear a2;
705      generalize in match H1; clear H1;
706      generalize in match m2; clear m2;
707      generalize in match m1; clear m1;
708      elim a 0;
709       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
710         simplify in H3;
711         change in H1 with
712          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
713      | intro v;
714        elim v 0;
715        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
716          simplify in H3;
717          change in H1 with
718           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
719        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
720          simplify in H3;
721          change in H1 with
722           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
723        ]
724      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
725        simplify in H3;
726        change in H1 with
727         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
728      | intro v;
729        elim v 0;
730         [ intros (T1 r m1 m2 H1 t1 t3 H3);
731           simplify in H3;
732           change in H1 with
733            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
734         | intros (T1 r m1 m2 H1 t1 t3 H3);
735           simplify in H3;
736           change in H1 with
737            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
738         ]
739      | intros (T m1 m2 H1 t1 t3 H3);
740        simplify in H3;
741        change in H1 with
742         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
743        rewrite > H3;
744        simplify in H;
745        apply H;
746         [ apply H1 
747         | assumption
748         ]
749      ] ;
750      simplify in H;
751      apply H;
752       [1,3,5,7,9,11:
753         apply H1;
754         assumption
755       |2,4,6,8,10,12:
756         assumption
757       ]
758    ]
759 qed.
760
761 theorem apply_morphism_compatibility_Left2Right:
762  ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
763   ∀args1,args2: product_of_arguments In.
764      make_compatibility_goal_aux ? ? m1 m2 →
765       relation_of_product_of_arguments Left2Right ? args1 args2 →
766         directed_relation_of_relation_class Left2Right ?
767          (apply_morphism ? ? m1 args1)
768          (apply_morphism ? ? m2 args2).
769   intro; 
770   elim In 0; simplify; intros;
771    [ change in H1 with
772       (directed_relation_of_argument_class
773         (get_rewrite_direction Left2Right a) a args1 args2);
774      generalize in match H1; clear H1;
775      generalize in match H; clear H;
776      generalize in match args2; clear args2;
777      generalize in match args1; clear args1;
778      generalize in match m2; clear m2;
779      generalize in match m1; clear m1;
780      elim a 0; simplify;
781       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
782         apply H;
783         exact H1
784       | intros 8 (v T1 r Hr m1 m2 args1 args2);
785         cases v;
786         intros (H H1);
787         simplify in H1;
788         apply H;
789         exact H1
790       | intros;
791         apply H1;
792         exact H2
793       | intros 7 (v);
794         cases v;
795         intros (H H1);
796         simplify in H1;
797         apply H;
798         exact H1
799       | intros;
800         simplify in H1;
801         rewrite > H1;
802         apply H;
803         exact H1
804       ]
805    | change in m1 with
806       (carrier_of_relation_class variance a →
807         function_type_of_morphism_signature n Out);
808      change in m2 with
809       (carrier_of_relation_class variance a →
810         function_type_of_morphism_signature n Out);
811      change in args1 with
812       ((carrier_of_relation_class ? a) × (product_of_arguments n));
813      change in args2 with
814       ((carrier_of_relation_class ? a) × (product_of_arguments n));
815      generalize in match H2; clear H2;
816      elim args2 0; clear args2;
817      elim args1; clear args1;
818      simplify in H2; change in H2:(? ? %) with
819        (relation_of_product_of_arguments Left2Right n b b1); 
820      elim H2; clear H2;
821      change with
822       (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b)
823         (apply_morphism n Out (m2 a2) b1));
824      generalize in match H3; clear H3;
825      generalize in match a2; clear a2;
826      generalize in match a1; clear a1;
827      generalize in match H1; clear H1;
828      generalize in match m2; clear m2;
829      generalize in match m1; clear m1;
830      elim a 0;
831       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
832         change in H1 with
833          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
834      | intro v;
835        elim v 0;
836        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
837          simplify in H3;
838          change in H1 with
839           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
840        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
841          simplify in H3;
842          change in H1 with
843           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
844        ]
845      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
846        simplify in H3;
847        change in H1 with
848         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
849      | intro v;
850        elim v 0;
851         [ intros (T1 r m1 m2 H1 t1 t3 H3);
852           simplify in H3;
853           change in H1 with
854            (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
855         | intros (T1 r m1 m2 H1 t1 t3 H3);
856           simplify in H3;
857           change in H1 with
858            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
859         ]
860      | intros (T m1 m2 H1 t1 t3 H3);
861        simplify in H3;
862        change in H1 with
863         (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
864        rewrite > H3;
865        simplify in H;
866        apply H;
867         [ apply H1 
868         | assumption
869         ]
870      ] ;
871      simplify in H;
872      apply H;
873       [1,3,5,7,9,11:
874         apply H1;
875         assumption
876       |2,4,6,8,10,12:
877         assumption
878       ]
879    ]
880 qed.
881
882 definition interp :
883  ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
884   Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
885  intros (Hole dir Out dir' H t).
886  apply
887   (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
888     (λxx,L,fcl.product_of_arguments L));
889   intros;
890    [8: apply t
891    |7: skip
892    | exact (apply_morphism ? ? (Function ? ? m) p)
893    | exact H
894    | exact c
895    | exact x
896    | simplify;
897      rewrite <
898        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
899      exact c1
900    | simplify;split;
901       [ rewrite <
902          (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
903         exact c1
904       | exact p
905       ]
906    ]
907 qed.
908
909
910 (*CSC: interp and interp_relation_class_list should be mutually defined. since
911    the proof term of each one contains the proof term of the other one. However
912    I cannot do that interactively (I should write the Fix by hand) *)
913 definition interp_relation_class_list :
914  ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
915   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
916  intros (Hole dir dir' L H t);
917  apply
918   (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
919     (λxx,L,fcl.product_of_arguments L));
920  intros;
921   [8: apply t
922   |7: skip
923   | exact (apply_morphism ? ? (Function ? ? m) p)
924   | exact H
925   | exact c
926   | exact x
927   | simplify;
928      rewrite <
929        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
930      exact c1
931   | simplify; split;
932      [ rewrite <
933         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
934        exact c1
935      | exact p
936      ]
937   ]
938 qed.
939
940 (*
941 Theorem setoid_rewrite:
942  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
943   (E: Morphism_Context Hole dir Out dir').
944    (directed_relation_of_relation_class dir Hole E1 E2) →
945     (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
946  intros.
947  elim E using
948    (@Morphism_Context_rect2 Hole dir
949      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
950      (fun dir'' L fcl =>
951         relation_of_product_of_arguments dir'' ?
952          (interp_relation_class_list E1 fcl)
953          (interp_relation_class_list E2 fcl))); intros.
954    change (directed_relation_of_relation_class dir'0 Out0
955     (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
956     (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
957    destruct dir'0.
958      apply apply_morphism_compatibility_Left2Right.
959        exact (Compat m).
960        exact H0.
961      apply apply_morphism_compatibility_Right2Left.
962        exact (Compat m).
963        exact H0.
964
965    exact H.
966
967    unfold interp. Morphism_Context_rect2.
968    (*CSC: reflexivity used here*)
969    destruct S; destruct dir'0; simpl; (apply r || reflexivity).
970
971    destruct dir'0; exact r.
972
973   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
974    unfold get_rewrite_direction; simpl.
975      destruct dir'0; destruct dir'';
976        (exact H0 ||
977         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
978      (* the following mess with generalize/clear/intros is to help Coq resolving *)
979      (* second order unification problems.                                                                *)
980      generalize m c H0; clear H0 m c; inversion c;
981        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
982          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
983      destruct dir'0; destruct dir'';
984        (exact H0 ||
985         unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
986 (* the following mess with generalize/clear/intros is to help Coq resolving *)
987      (* second order unification problems.                                                                *)
988      generalize m c H0; clear H0 m c; inversion c;
989        generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
990          (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
991      destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
992
993   change
994     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
995        (eq_rect ? (fun T : Type => T) (interp E1 m) ?
996          (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
997        (eq_rect ? (fun T : Type => T) (interp E2 m) ?
998          (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
999      relation_of_product_of_arguments dir'' ?
1000        (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
1001    split.
1002      clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
1003         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
1004         inversion c.
1005           rewrite <- H3; exact H0.
1006           rewrite (opposite_direction_idempotent dir'0); exact H0.
1007         destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
1008         inversion c.
1009           rewrite <- H3; exact H0.
1010           rewrite (opposite_direction_idempotent dir'0); exact H0.
1011         destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
1012      exact H1.
1013 Qed.
1014
1015 (* A FEW EXAMPLES ON iff *)
1016
1017 (* impl IS A MORPHISM *)
1018
1019 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
1020 unfold impl; tautobatch.
1021 Qed.
1022
1023 (* and IS A MORPHISM *)
1024
1025 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
1026  tautobatch.
1027 Qed.
1028
1029 (* or IS A MORPHISM *)
1030
1031 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
1032  tautobatch.
1033 Qed.
1034
1035 (* not IS A MORPHISM *)
1036
1037 Add Morphism not with signature iff ==> iff as Not_Morphism.
1038  tautobatch.
1039 Qed.
1040
1041 (* THE SAME EXAMPLES ON impl *)
1042
1043 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
1044  unfold impl; tautobatch.
1045 Qed.
1046
1047 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
1048  unfold impl; tautobatch.
1049 Qed.
1050
1051 Add Morphism not with signature impl -→ impl as Not_Morphism2.
1052  unfold impl; tautobatch.
1053 Qed.
1054
1055 *)