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".
23 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
25 (* X will be used to distinguish covariant arguments whose type is an *)
26 (* Asymmetric* relation from contravariant arguments of the same type *)
27 inductive X_Relation_Class (X: Type) : Type ≝
29 ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → X_Relation_Class X
30 | AsymmetricReflexive : X → ∀A,Aeq. reflexive A Aeq → X_Relation_Class X
31 | SymmetricAreflexive : ∀A,Aeq. symmetric A Aeq → X_Relation_Class X
32 | AsymmetricAreflexive : X → ∀A.∀Aeq : relation A. X_Relation_Class X
33 | Leibniz : Type → X_Relation_Class X.
35 inductive variance : Set ≝
37 | Contravariant : variance.
39 definition Argument_Class ≝ X_Relation_Class variance.
40 definition Relation_Class ≝ X_Relation_Class unit.
42 inductive Reflexive_Relation_Class : Type :=
44 ∀A,Aeq. symmetric A Aeq → reflexive ? Aeq → Reflexive_Relation_Class
46 ∀A,Aeq. reflexive A Aeq → Reflexive_Relation_Class
47 | RLeibniz : Type → Reflexive_Relation_Class.
49 inductive Areflexive_Relation_Class : Type :=
50 | ASymmetric : ∀A,Aeq. symmetric A Aeq → Areflexive_Relation_Class
51 | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
53 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
57 [ apply (SymmetricReflexive ? ? ? H H1)
58 | apply (AsymmetricReflexive ? something ? ? H)
59 | apply (SymmetricAreflexive ? ? ? H)
60 | apply (AsymmetricAreflexive ? something ? r)
61 | apply (Leibniz ? T1)
65 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
71 definition relation_of_relation_class :
72 ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
76 [1,2: intros 4; apply r
77 |3,4: intros 3; apply r
82 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
84 carrier_of_relation_class ? (relation_class_of_argument_class R) =
85 carrier_of_relation_class ? R.
91 inductive nelistT (A : Type) : Type :=
93 | cons : A → nelistT A → nelistT A.
95 definition Arguments := nelistT Argument_Class.
97 definition function_type_of_morphism_signature :
98 Arguments → Relation_Class → Type.
101 [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
102 | exact (carrier_of_relation_class ? t → T)
106 definition make_compatibility_goal_aux:
107 ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
109 elim In (a); simplify in f f1;
110 generalize in match f1; clear f1;
111 generalize in match f; clear f;
112 [ elim a; simplify in f f1;
113 [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
115 [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
116 | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
118 | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
120 [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
121 | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
123 | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
126 ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
127 (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
129 elim t; simplify in f f1;
130 [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
132 [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
133 | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
135 | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
137 [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
138 | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
140 | exact (∀x. R (f x) (f1 x))
145 definition make_compatibility_goal :=
146 λIn,Out,f. make_compatibility_goal_aux In Out f f.
148 record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
149 { Function : function_type_of_morphism_signature In Out;
150 Compat : make_compatibility_goal In Out Function
153 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
156 [ apply (singl ? (Leibniz ? t))
157 | apply (cons ? (Leibniz ? t) a)
161 (* every function is a morphism from Leibniz+ to Leibniz *)
162 definition morphism_theory_of_function :
163 ∀In: nelistT Type.∀Out: Type.
164 let In' := list_of_Leibniz_of_list_of_types In in
165 let Out' := Leibniz ? Out in
166 function_type_of_morphism_signature In' Out' →
167 Morphism_Theory In' Out'.
169 apply (mk_Morphism_Theory ? ? f);
170 unfold In' in f; clear In';
171 unfold Out' in f; clear Out';
172 generalize in match f; clear f;
174 [ unfold make_compatibility_goal;
187 (* THE iff RELATION CLASS *)
189 definition Iff_Relation_Class : Relation_Class.
190 apply (SymmetricReflexive unit ? iff);
191 [ exact symmetric_iff
192 | exact reflexive_iff
196 (* THE impl RELATION CLASS *)
198 definition impl \def \lambda A,B:Prop. A → B.
200 theorem impl_refl: reflexive ? impl.
208 definition Impl_Relation_Class : Relation_Class.
209 unfold Relation_Class;
210 apply (AsymmetricReflexive unit something ? impl);
214 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
216 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
217 ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq.
218 let ASetoidClass := SymmetricAreflexive ? ? ? sym in
219 (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass))
222 apply mk_Morphism_Theory;
224 | unfold make_compatibility_goal;
228 unfold transitive in H;
229 unfold symmetric in sym;
235 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
236 ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq.
237 ∀trans: transitive ? Aeq.
238 let ASetoidClass := SymmetricReflexive ? ? ? sym refl in
239 (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
241 apply mk_Morphism_Theory;
247 unfold transitive in H;
248 unfold symmetric in sym;
253 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
254 ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
255 let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
256 let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
257 (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
259 apply mk_Morphism_Theory;
270 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
271 ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
272 let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
273 let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
274 (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
276 apply mk_Morphism_Theory;
287 (* iff AS A RELATION *)
289 (*DA PORTARE:Add Relation Prop iff
290 reflexivity proved by iff_refl
291 symmetry proved by iff_sym
292 transitivity proved by iff_trans
295 (* every predicate is morphism from Leibniz+ to Iff_Relation_Class *)
296 definition morphism_theory_of_predicate :
298 let In' := list_of_Leibniz_of_list_of_types In in
299 function_type_of_morphism_signature In' Iff_Relation_Class →
300 Morphism_Theory In' Iff_Relation_Class.
302 apply mk_Morphism_Theory;
304 | generalize in match f; clear f;
305 unfold In'; clear In';
309 alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
318 (* impl AS A RELATION *)
320 theorem impl_trans: transitive ? impl.
327 (*DA PORTARE: Add Relation Prop impl
328 reflexivity proved by impl_refl
329 transitivity proved by impl_trans
332 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
334 inductive rewrite_direction : Type :=
335 Left2Right: rewrite_direction
336 | Right2Left: rewrite_direction.
338 definition variance_of_argument_class : Argument_Class → option variance.
349 definition opposite_direction :=
352 [ Left2Right ⇒ Right2Left
353 | Right2Left ⇒ Left2Right
356 lemma opposite_direction_idempotent:
357 ∀dir. opposite_direction (opposite_direction dir) = dir.
363 inductive check_if_variance_is_respected :
364 option variance → rewrite_direction → rewrite_direction → Prop
366 MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
367 | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
370 check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
372 definition relation_class_of_reflexive_relation_class:
373 Reflexive_Relation_Class → Relation_Class.
376 [ apply (SymmetricReflexive ? ? ? H H1)
377 | apply (AsymmetricReflexive ? something ? ? H)
378 | apply (Leibniz ? T)
382 definition relation_class_of_areflexive_relation_class:
383 Areflexive_Relation_Class → Relation_Class.
386 [ apply (SymmetricAreflexive ? ? ? H)
387 | apply (AsymmetricAreflexive ? something ? r)
391 definition carrier_of_reflexive_relation_class :=
392 λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
394 definition carrier_of_areflexive_relation_class :=
395 λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
397 definition relation_of_areflexive_relation_class :=
398 λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
400 inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction → Type :=
403 Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
404 Morphism_Context Hole dir Out dir
405 | ToReplace : Morphism_Context Hole dir Hole dir
408 carrier_of_reflexive_relation_class S →
409 Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
410 | ProperElementToKeep :
411 ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
412 relation_of_areflexive_relation_class S x x →
413 Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
414 with Morphism_Context_List :
415 rewrite_direction → Arguments → Type
419 check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
420 Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
421 Morphism_Context_List Hole dir dir'' (singl ? S)
424 check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
425 Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
426 Morphism_Context_List Hole dir dir'' L →
427 Morphism_Context_List Hole dir dir'' (cons ? S L).
429 definition product_of_arguments : Arguments → Type.
432 [ apply (carrier_of_relation_class ? t)
433 | apply (Prod (carrier_of_relation_class ? t) T)
437 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
439 cases (variance_of_argument_class R);
441 [ exact dir (* covariant *)
442 | exact (opposite_direction dir) (* contravariant *)
444 | exact dir (* symmetric relation *)
448 definition directed_relation_of_relation_class:
449 ∀dir:rewrite_direction.∀R: Relation_Class.
450 carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
453 [ exact (relation_of_relation_class ? ? c c1)
454 | apply (relation_of_relation_class ? ? c1 c)
458 definition directed_relation_of_argument_class:
459 ∀dir:rewrite_direction.∀R: Argument_Class.
460 carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
463 (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
465 apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
466 apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
472 definition relation_of_product_of_arguments:
473 ∀dir:rewrite_direction.∀In.
474 product_of_arguments In → product_of_arguments In → Prop.
479 exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
481 change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
482 change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
487 (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
494 definition apply_morphism:
495 ∀In Out (m: function_type_of_morphism_signature In Out)
496 (args: product_of_arguments In). carrier_of_relation_class Out.
502 exact (IHIn (m c) p).
505 Theorem apply_morphism_compatibility_Right2Left:
506 ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
507 (args1 args2: product_of_arguments In).
508 make_compatibility_goal_aux ? ? m1 m2 →
509 relation_of_product_of_arguments Right2Left ? args1 args2 →
510 directed_relation_of_relation_class Right2Left ?
511 (apply_morphism ? ? m2 args1)
512 (apply_morphism ? ? m1 args2).
513 induction In; intros.
514 simpl in m1. m2. args1. args2. H0 |- *.
515 destruct a; simpl in H; hnf in H0.
517 destruct v; simpl in H0; apply H; exact H0.
519 destruct v; simpl in H0; apply H; exact H0.
520 rewrite H0; apply H; exact H0.
522 simpl in m1. m2. args1. args2. H0 |- *.
523 destruct args1; destruct args2; simpl.
526 destruct a; simpl in H.
547 rewrite H0; apply IHIn.
552 Theorem apply_morphism_compatibility_Left2Right:
553 ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
554 (args1 args2: product_of_arguments In).
555 make_compatibility_goal_aux ? ? m1 m2 →
556 relation_of_product_of_arguments Left2Right ? args1 args2 →
557 directed_relation_of_relation_class Left2Right ?
558 (apply_morphism ? ? m1 args1)
559 (apply_morphism ? ? m2 args2).
560 induction In; intros.
561 simpl in m1. m2. args1. args2. H0 |- *.
562 destruct a; simpl in H; hnf in H0.
564 destruct v; simpl in H0; apply H; exact H0.
566 destruct v; simpl in H0; apply H; exact H0.
567 rewrite H0; apply H; exact H0.
569 simpl in m1. m2. args1. args2. H0 |- *.
570 destruct args1; destruct args2; simpl.
573 destruct a; simpl in H.
588 destruct v; simpl in H. H0; apply H; exact H0.
590 rewrite H0; apply IHIn.
596 ∀Hole dir Out dir'. carrier_of_relation_class Hole →
597 Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
598 intros Hole dir Out dir' H t.
600 (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
601 (fun ? L fcl => product_of_arguments L));
603 exact (apply_morphism ? ? (Function m) X).
609 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
613 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
618 (*CSC: interp and interp_relation_class_list should be mutually defined. since
619 the proof term of each one contains the proof term of the other one. However
620 I cannot do that interactively (I should write the Fix by hand) *)
621 definition interp_relation_class_list :
622 ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
623 Morphism_Context_List Hole dir dir' L → product_of_arguments L.
624 intros Hole dir dir' L H t.
626 (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
627 (fun ? L fcl => product_of_arguments L));
629 exact (apply_morphism ? ? (Function m) X).
635 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
639 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
644 Theorem setoid_rewrite:
645 ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
646 (E: Morphism_Context Hole dir Out dir').
647 (directed_relation_of_relation_class dir Hole E1 E2) →
648 (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
651 (@Morphism_Context_rect2 Hole dir
652 (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
654 relation_of_product_of_arguments dir'' ?
655 (interp_relation_class_list E1 fcl)
656 (interp_relation_class_list E2 fcl))); intros.
657 change (directed_relation_of_relation_class dir'0 Out0
658 (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
659 (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
661 apply apply_morphism_compatibility_Left2Right.
664 apply apply_morphism_compatibility_Right2Left.
670 unfold interp. Morphism_Context_rect2.
671 (*CSC: reflexivity used here*)
672 destruct S; destruct dir'0; simpl; (apply r || reflexivity).
674 destruct dir'0; exact r.
676 destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
677 unfold get_rewrite_direction; simpl.
678 destruct dir'0; destruct dir'';
680 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
681 (* the following mess with generalize/clear/intros is to help Coq resolving *)
682 (* second order unification problems. *)
683 generalize m c H0; clear H0 m c; inversion c;
684 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
685 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
686 destruct dir'0; destruct dir'';
688 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
689 (* the following mess with generalize/clear/intros is to help Coq resolving *)
690 (* second order unification problems. *)
691 generalize m c H0; clear H0 m c; inversion c;
692 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
693 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
694 destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
697 (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
698 (eq_rect ? (fun T : Type => T) (interp E1 m) ?
699 (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
700 (eq_rect ? (fun T : Type => T) (interp E2 m) ?
701 (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
702 relation_of_product_of_arguments dir'' ?
703 (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
705 clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
706 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
708 rewrite <- H3; exact H0.
709 rewrite (opposite_direction_idempotent dir'0); exact H0.
710 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
712 rewrite <- H3; exact H0.
713 rewrite (opposite_direction_idempotent dir'0); exact H0.
714 destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
718 (* A FEW EXAMPLES ON iff *)
720 (* impl IS A MORPHISM *)
722 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
726 (* and IS A MORPHISM *)
728 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
732 (* or IS A MORPHISM *)
734 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
738 (* not IS A MORPHISM *)
740 Add Morphism not with signature iff ==> iff as Not_Morphism.
744 (* THE SAME EXAMPLES ON impl *)
746 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
750 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
754 Add Morphism not with signature impl -→ impl as Not_Morphism2.