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