1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti. C.Sacerdoti Coen. *)
8 (* ||A|| E.Tassi. S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
16 (* Original author: Claudio Sacerdoti Coen. for the Coq system *)
18 set "baseuri" "cic:/matita/technicalities/setoids".
20 include "datatypes/constructors.ma".
21 include "logic/connectives2.ma".
22 include "logic/coimplication.ma".
24 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
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 ≝
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.
36 inductive variance : Set ≝
38 | Contravariant : variance.
40 definition Argument_Class ≝ X_Relation_Class variance.
41 definition Relation_Class ≝ X_Relation_Class unit.
43 inductive Reflexive_Relation_Class : Type :=
45 ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
47 ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
48 | RLeibniz : Type → Reflexive_Relation_Class.
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.
54 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
56 [ apply (SymmetricReflexive ? ? ? H H1)
57 | apply (AsymmetricReflexive ? something ? ? H)
58 | apply (SymmetricAreflexive ? ? ? H)
59 | apply (AsymmetricAreflexive ? something ? r)
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.
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) ]
73 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
75 carrier_of_relation_class ? (relation_class_of_argument_class R) =
76 carrier_of_relation_class ? R.
77 intro; cases R; reflexivity.
80 inductive nelistT (A : Type) : Type :=
82 | cons : A → nelistT A → nelistT A.
84 definition Arguments := nelistT Argument_Class.
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)
94 definition make_compatibility_goal_aux:
95 ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
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))
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))
106 | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
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))
111 | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
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) →
117 elim t; simplify in f f1;
118 [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
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))
123 | exact (∀x. R (f x) (f1 x))
128 definition make_compatibility_goal :=
129 λIn,Out,f. make_compatibility_goal_aux In Out f f.
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
136 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
139 [ apply (singl ? (Leibniz ? t))
140 | apply (cons ? (Leibniz ? t) a)
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'.
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;
157 [ unfold make_compatibility_goal;
168 (* THE iff RELATION CLASS *)
170 definition Iff_Relation_Class : Relation_Class.
171 apply (SymmetricReflexive unit ? iff);
172 [ exact symmetric_iff
173 | exact reflexive_iff
177 (* THE impl RELATION CLASS *)
179 definition impl \def \lambda A,B:Prop. A → B.
181 theorem impl_refl: reflexive ? impl.
189 definition Impl_Relation_Class : Relation_Class.
190 unfold Relation_Class;
191 apply (AsymmetricReflexive unit something ? impl);
195 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
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))
203 apply mk_Morphism_Theory;
205 | unfold make_compatibility_goal;
209 unfold transitive in H;
210 unfold symmetric in sym;
212 [ apply (H x2 x1 x3 ? ?);
213 [apply (sym x1 x2 ?).
215 |apply (H x1 x x3 ? ?);
220 | apply (H x1 x3 x ? ?);
221 [apply (H x1 x2 x3 ? ?);
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).
238 apply mk_Morphism_Theory;
244 unfold transitive in H;
245 unfold symmetric in sym;
246 [ apply (H x2 x1 x3 ? ?);
247 [apply (sym x1 x2 ?).
249 |apply (H x1 x x3 ? ?);
254 | apply (H x1 x2 x ? ?);
256 |apply (H x2 x3 x ? ?);
259 apply (H x x3 x3 ? ?);
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).
275 apply mk_Morphism_Theory;
282 apply (H x2 x1 x3 ? ?);
284 |apply (H x1 x x3 ? ?);
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).
298 apply mk_Morphism_Theory;
305 apply (H x2 x1 x3 ? ?);
307 |apply (H x1 x x3 ? ?);
315 (* iff AS A RELATION *)
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
323 (* every predicate is morphism from Leibniz+ to Iff_Relation_Class *)
324 definition morphism_theory_of_predicate :
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.
330 apply mk_Morphism_Theory;
332 | generalize in match f; clear f;
333 unfold In'; clear In';
345 (* impl AS A RELATION *)
347 theorem impl_trans: transitive ? impl.
351 apply (H1 ?).apply (H ?).apply (H2).
355 (*DA PORTARE: Add Relation Prop impl
356 reflexivity proved by impl_refl
357 transitivity proved by impl_trans
360 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
362 inductive rewrite_direction : Type :=
363 Left2Right: rewrite_direction
364 | Right2Left: rewrite_direction.
366 definition variance_of_argument_class : Argument_Class → option variance.
377 definition opposite_direction :=
380 [ Left2Right ⇒ Right2Left
381 | Right2Left ⇒ Left2Right
384 lemma opposite_direction_idempotent:
385 ∀dir. opposite_direction (opposite_direction dir) = dir.
391 inductive check_if_variance_is_respected :
392 option variance → rewrite_direction → rewrite_direction → Prop
394 MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
395 | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
398 check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
400 definition relation_class_of_reflexive_relation_class:
401 Reflexive_Relation_Class → Relation_Class.
404 [ apply (SymmetricReflexive ? ? ? H H1)
405 | apply (AsymmetricReflexive ? something ? ? H)
406 | apply (Leibniz ? T)
410 definition relation_class_of_areflexive_relation_class:
411 Areflexive_Relation_Class → Relation_Class.
414 [ apply (SymmetricAreflexive ? ? ? H)
415 | apply (AsymmetricAreflexive ? something ? r)
419 definition carrier_of_reflexive_relation_class :=
420 λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
422 definition carrier_of_areflexive_relation_class :=
423 λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
425 definition relation_of_areflexive_relation_class :=
426 λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
428 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction → Type :=
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
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
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)
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).
457 lemma Morphism_Context_rect2:
460 ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
462 ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
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.
489 λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
491 F (rc:Relation_Class) (r0:rewrite_direction)
492 (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
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)
497 | ToKeep S dir' c ⇒ f1 S dir' c
498 | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
501 F0 (r:rewrite_direction) (a:Arguments)
502 (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
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)
513 lemma Morphism_Context_List_rect2:
516 ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
518 ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
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.
545 λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
547 F (rc:Relation_Class) (r0:rewrite_direction)
548 (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
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)
553 | ToKeep S dir' c ⇒ f1 S dir' c
554 | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
557 F0 (r:rewrite_direction) (a:Arguments)
558 (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
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)
569 definition product_of_arguments : Arguments → Type.
572 [ apply (carrier_of_relation_class ? t)
573 | apply (Prod (carrier_of_relation_class ? t) T)
577 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
579 cases (variance_of_argument_class R) (a);
582 [ exact dir (* covariant *)
583 | exact (opposite_direction dir) (* contravariant *)
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.
593 [ exact (relation_of_relation_class ? ? c c1)
594 | apply (relation_of_relation_class ? ? c1 c)
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.
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).
607 definition relation_of_product_of_arguments:
608 ∀dir:rewrite_direction.∀In.
609 product_of_arguments In → product_of_arguments In → Prop.
614 exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
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));
622 (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
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.
634 | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
636 change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
637 exact (f ? (f1 t1) t2)
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).
651 [ simplify in m1 m2 args1 args2 ⊢ %;
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;
662 [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
665 | intros 8 (v T1 r Hr m1 m2 args1 args2);
685 (carrier_of_relation_class variance t →
686 function_type_of_morphism_signature n Out);
688 (carrier_of_relation_class variance t →
689 function_type_of_morphism_signature n Out);
691 ((carrier_of_relation_class ? t) × (product_of_arguments n));
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;
699 (relation_of_product_of_arguments Right2Left n t2 t4);
701 (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
702 (apply_morphism n Out (m2 t1) t2));
703 generalize in match H3; clear H3;
704 generalize in match t3; clear t3;
705 generalize in match t1; clear t1;
706 generalize in match H1; clear H1;
707 generalize in match m2; clear m2;
708 generalize in match m1; clear m1;
710 [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
713 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
716 [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
719 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
720 | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
723 (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
725 | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
728 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
731 [ intros (T1 r m1 m2 H1 t1 t3 H3);
734 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
735 | intros (T1 r m1 m2 H1 t1 t3 H3);
738 (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
740 | intros (T m1 m2 H1 t1 t3 H3);
743 (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
762 theorem apply_morphism_compatibility_Left2Right:
763 ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
764 ∀args1,args2: product_of_arguments In.
765 make_compatibility_goal_aux ? ? m1 m2 →
766 relation_of_product_of_arguments Left2Right ? args1 args2 →
767 directed_relation_of_relation_class Left2Right ?
768 (apply_morphism ? ? m1 args1)
769 (apply_morphism ? ? m2 args2).
771 elim In 0; simplify; intros;
773 (directed_relation_of_argument_class
774 (get_rewrite_direction Left2Right t) t args1 args2);
775 generalize in match H1; clear H1;
776 generalize in match H; clear H;
777 generalize in match args2; clear args2;
778 generalize in match args1; clear args1;
779 generalize in match m2; clear m2;
780 generalize in match m1; clear m1;
782 [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
785 | intros 8 (v T1 r Hr m1 m2 args1 args2);
807 (carrier_of_relation_class variance t →
808 function_type_of_morphism_signature n Out);
810 (carrier_of_relation_class variance t →
811 function_type_of_morphism_signature n Out);
813 ((carrier_of_relation_class ? t) × (product_of_arguments n));
815 ((carrier_of_relation_class ? t) × (product_of_arguments n));
816 generalize in match H2; clear H2;
817 elim args2 0; clear args2;
818 elim args1; clear args1;
821 (relation_of_product_of_arguments Left2Right n t2 t4);
823 (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
824 (apply_morphism n Out (m2 t3) t4));
825 generalize in match H3; clear H3;
826 generalize in match t3; clear t3;
827 generalize in match t1; clear t1;
828 generalize in match H1; clear H1;
829 generalize in match m2; clear m2;
830 generalize in match m1; clear m1;
832 [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
834 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
837 [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
840 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
841 | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
844 (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
846 | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
849 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
852 [ intros (T1 r m1 m2 H1 t1 t3 H3);
855 (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
856 | intros (T1 r m1 m2 H1 t1 t3 H3);
859 (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
861 | intros (T m1 m2 H1 t1 t3 H3);
864 (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
884 ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
885 Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
886 intros (Hole dir Out dir' H t).
888 (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
889 (λxx,L,fcl.product_of_arguments L));
893 | exact (apply_morphism ? ? (Function ? ? m) p)
899 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
903 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
911 (*CSC: interp and interp_relation_class_list should be mutually defined. since
912 the proof term of each one contains the proof term of the other one. However
913 I cannot do that interactively (I should write the Fix by hand) *)
914 definition interp_relation_class_list :
915 ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
916 Morphism_Context_List Hole dir dir' L → product_of_arguments L.
917 intros (Hole dir dir' L H t);
919 (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
920 (λxx,L,fcl.product_of_arguments L));
924 | exact (apply_morphism ? ? (Function ? ? m) p)
930 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
934 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
942 Theorem setoid_rewrite:
943 ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
944 (E: Morphism_Context Hole dir Out dir').
945 (directed_relation_of_relation_class dir Hole E1 E2) →
946 (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
949 (@Morphism_Context_rect2 Hole dir
950 (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
952 relation_of_product_of_arguments dir'' ?
953 (interp_relation_class_list E1 fcl)
954 (interp_relation_class_list E2 fcl))); intros.
955 change (directed_relation_of_relation_class dir'0 Out0
956 (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
957 (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
959 apply apply_morphism_compatibility_Left2Right.
962 apply apply_morphism_compatibility_Right2Left.
968 unfold interp. Morphism_Context_rect2.
969 (*CSC: reflexivity used here*)
970 destruct S; destruct dir'0; simpl; (apply r || reflexivity).
972 destruct dir'0; exact r.
974 destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
975 unfold get_rewrite_direction; simpl.
976 destruct dir'0; destruct dir'';
978 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
979 (* the following mess with generalize/clear/intros is to help Coq resolving *)
980 (* second order unification problems. *)
981 generalize m c H0; clear H0 m c; inversion c;
982 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
983 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
984 destruct dir'0; destruct dir'';
986 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
987 (* the following mess with generalize/clear/intros is to help Coq resolving *)
988 (* second order unification problems. *)
989 generalize m c H0; clear H0 m c; inversion c;
990 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
991 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
992 destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
995 (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
996 (eq_rect ? (fun T : Type => T) (interp E1 m) ?
997 (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
998 (eq_rect ? (fun T : Type => T) (interp E2 m) ?
999 (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
1000 relation_of_product_of_arguments dir'' ?
1001 (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
1003 clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
1004 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
1006 rewrite <- H3; exact H0.
1007 rewrite (opposite_direction_idempotent dir'0); exact H0.
1008 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
1010 rewrite <- H3; exact H0.
1011 rewrite (opposite_direction_idempotent dir'0); exact H0.
1012 destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
1016 (* A FEW EXAMPLES ON iff *)
1018 (* impl IS A MORPHISM *)
1020 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
1021 unfold impl; tautobatch.
1024 (* and IS A MORPHISM *)
1026 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
1030 (* or IS A MORPHISM *)
1032 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
1036 (* not IS A MORPHISM *)
1038 Add Morphism not with signature iff ==> iff as Not_Morphism.
1042 (* THE SAME EXAMPLES ON impl *)
1044 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
1045 unfold impl; tautobatch.
1048 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
1049 unfold impl; tautobatch.
1052 Add Morphism not with signature impl -→ impl as Not_Morphism2.
1053 unfold impl; tautobatch.