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 "higher_order_defs/relations.ma".
21 include "datatypes/constructors.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 f; clear f;
111 generalize in match f1; clear f1;
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 Out : 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.
155 exact (singl (Leibniz ? a)).
156 exact (cons (Leibniz ? a) IHX).
159 (* every function is a morphism from Leibniz+ to Leibniz *)
160 definition morphism_theory_of_function :
161 ∀(In: nelistT Type) (Out: Type).
162 let In' := list_of_Leibniz_of_list_of_types In in
163 let Out' := Leibniz ? Out in
164 function_type_of_morphism_signature In' Out' →
165 Morphism_Theory In' Out'.
168 induction In; unfold make_compatibility_goal; simpl.
170 intro; apply (IHIn (X x)).
173 (* THE iff RELATION CLASS *)
175 definition Iff_Relation_Class : Relation_Class.
176 eapply (@SymmetricReflexive unit ? iff).
181 (* THE impl RELATION CLASS *)
183 definition impl (A B: Prop) := A → B.
185 Theorem impl_refl: reflexive ? impl.
186 hnf; unfold impl; tauto.
189 definition Impl_Relation_Class : Relation_Class.
190 eapply (@AsymmetricReflexive unit tt ? impl).
194 (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
196 definition equality_morphism_of_symmetric_areflexive_transitive_relation:
197 ∀(A: Type)(Aeq: relation A)(sym: symmetric ? Aeq)(trans: transitive ? Aeq).
198 let ASetoidClass := SymmetricAreflexive ? sym in
199 (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
202 unfold make_compatibility_goal; simpl; split; eauto.
205 definition equality_morphism_of_symmetric_reflexive_transitive_relation:
206 ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(sym: symmetric ? Aeq)
207 (trans: transitive ? Aeq). let ASetoidClass := SymmetricReflexive ? sym refl in
208 (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
211 unfold make_compatibility_goal; simpl; split; eauto.
214 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
215 ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
216 let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
217 let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
218 (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
221 unfold make_compatibility_goal; simpl; unfold impl; eauto.
224 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
225 ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
226 let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
227 let ASetoidClass2 := AsymmetricReflexive Covariant refl in
228 (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
231 unfold make_compatibility_goal; simpl; unfold impl; eauto.
234 (* iff AS A RELATION *)
236 Add Relation Prop iff
237 reflexivity proved by iff_refl
238 symmetry proved by iff_sym
239 transitivity proved by iff_trans
242 (* every predicate is morphism from Leibniz+ to Iff_Relation_Class *)
243 definition morphism_theory_of_predicate :
245 let In' := list_of_Leibniz_of_list_of_types In in
246 function_type_of_morphism_signature In' Iff_Relation_Class →
247 Morphism_Theory In' Iff_Relation_Class.
250 induction In; unfold make_compatibility_goal; simpl.
251 intro; apply iff_refl.
252 intro; apply (IHIn (X x)).
255 (* impl AS A RELATION *)
257 Theorem impl_trans: transitive ? impl.
258 hnf; unfold impl; tauto.
261 Add Relation Prop impl
262 reflexivity proved by impl_refl
263 transitivity proved by impl_trans
266 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
268 inductive rewrite_direction : Type :=
272 Implicit Type dir: rewrite_direction.
274 definition variance_of_argument_class : Argument_Class → option variance.
283 definition opposite_direction :=
286 Left2Right => Right2Left
287 | Right2Left => Left2Right
290 Lemma opposite_direction_idempotent:
291 ∀dir. (opposite_direction (opposite_direction dir)) = dir.
292 destruct dir; reflexivity.
295 inductive check_if_variance_is_respected :
296 option variance → rewrite_direction → rewrite_direction → Prop
298 MSNone : ∀dir dir'. check_if_variance_is_respected None dir dir'
299 | MSCovariant : ∀dir. check_if_variance_is_respected (Some Covariant) dir dir
302 check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
304 definition relation_class_of_reflexive_relation_class:
305 Reflexive_Relation_Class → Relation_Class.
307 exact (SymmetricReflexive ? s r).
308 exact (AsymmetricReflexive tt r).
312 definition relation_class_of_areflexive_relation_class:
313 Areflexive_Relation_Class → Relation_Class.
315 exact (SymmetricAreflexive ? s).
316 exact (AsymmetricAreflexive tt Aeq).
319 definition carrier_of_reflexive_relation_class :=
320 fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
322 definition carrier_of_areflexive_relation_class :=
323 fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
325 definition relation_of_areflexive_relation_class :=
326 fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
328 inductive Morphism_Context Hole dir : Relation_Class → rewrite_direction → Type :=
331 Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
332 Morphism_Context Hole dir Out dir'
333 | ToReplace : Morphism_Context Hole dir Hole dir
336 carrier_of_reflexive_relation_class S →
337 Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
338 | ProperElementToKeep :
339 ∀S dir' (x: carrier_of_areflexive_relation_class S).
340 relation_of_areflexive_relation_class S x x →
341 Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
342 with Morphism_Context_List Hole dir :
343 rewrite_direction → Arguments → Type
347 check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
348 Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
349 Morphism_Context_List Hole dir dir'' (singl S)
352 check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
353 Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
354 Morphism_Context_List Hole dir dir'' L →
355 Morphism_Context_List Hole dir dir'' (cons S L).
357 Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type
358 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
360 definition product_of_arguments : Arguments → Type.
362 exact (carrier_of_relation_class a).
363 exact (prod (carrier_of_relation_class a) IHX).
366 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
368 destruct (variance_of_argument_class R).
370 exact dir. (* covariant *)
371 exact (opposite_direction dir). (* contravariant *)
372 exact dir. (* symmetric relation *)
375 definition directed_relation_of_relation_class:
376 ∀dir (R: Relation_Class).
377 carrier_of_relation_class R → carrier_of_relation_class R → Prop.
379 exact (@relation_of_relation_class unit).
380 intros; exact (relation_of_relation_class ? X0 X).
383 definition directed_relation_of_argument_class:
384 ∀dir (R: Argument_Class).
385 carrier_of_relation_class R → carrier_of_relation_class R → Prop.
388 (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
389 exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
393 definition relation_of_product_of_arguments:
395 product_of_arguments In → product_of_arguments In → Prop.
398 exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
401 destruct X; destruct X0.
404 (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0).
408 definition apply_morphism:
409 ∀In Out (m: function_type_of_morphism_signature In Out)
410 (args: product_of_arguments In). carrier_of_relation_class Out.
416 exact (IHIn (m c) p).
419 Theorem apply_morphism_compatibility_Right2Left:
420 ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
421 (args1 args2: product_of_arguments In).
422 make_compatibility_goal_aux ? ? m1 m2 →
423 relation_of_product_of_arguments Right2Left ? args1 args2 →
424 directed_relation_of_relation_class Right2Left ?
425 (apply_morphism ? ? m2 args1)
426 (apply_morphism ? ? m1 args2).
427 induction In; intros.
428 simpl in m1. m2. args1. args2. H0 |- *.
429 destruct a; simpl in H; hnf in H0.
431 destruct v; simpl in H0; apply H; exact H0.
433 destruct v; simpl in H0; apply H; exact H0.
434 rewrite H0; apply H; exact H0.
436 simpl in m1. m2. args1. args2. H0 |- *.
437 destruct args1; destruct args2; simpl.
440 destruct a; simpl in H.
461 rewrite H0; apply IHIn.
466 Theorem apply_morphism_compatibility_Left2Right:
467 ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
468 (args1 args2: product_of_arguments In).
469 make_compatibility_goal_aux ? ? m1 m2 →
470 relation_of_product_of_arguments Left2Right ? args1 args2 →
471 directed_relation_of_relation_class Left2Right ?
472 (apply_morphism ? ? m1 args1)
473 (apply_morphism ? ? m2 args2).
474 induction In; intros.
475 simpl in m1. m2. args1. args2. H0 |- *.
476 destruct a; simpl in H; hnf in H0.
478 destruct v; simpl in H0; apply H; exact H0.
480 destruct v; simpl in H0; apply H; exact H0.
481 rewrite H0; apply H; exact H0.
483 simpl in m1. m2. args1. args2. H0 |- *.
484 destruct args1; destruct args2; simpl.
487 destruct a; simpl in H.
502 destruct v; simpl in H. H0; apply H; exact H0.
504 rewrite H0; apply IHIn.
510 ∀Hole dir Out dir'. carrier_of_relation_class Hole →
511 Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
512 intros Hole dir Out dir' H t.
514 (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
515 (fun ? L fcl => product_of_arguments L));
517 exact (apply_morphism ? ? (Function m) X).
523 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
527 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
532 (*CSC: interp and interp_relation_class_list should be mutually defined. since
533 the proof term of each one contains the proof term of the other one. However
534 I cannot do that interactively (I should write the Fix by hand) *)
535 definition interp_relation_class_list :
536 ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
537 Morphism_Context_List Hole dir dir' L → product_of_arguments L.
538 intros Hole dir dir' L H t.
540 (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
541 (fun ? L fcl => product_of_arguments L));
543 exact (apply_morphism ? ? (Function m) X).
549 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
553 (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
558 Theorem setoid_rewrite:
559 ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
560 (E: Morphism_Context Hole dir Out dir').
561 (directed_relation_of_relation_class dir Hole E1 E2) →
562 (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
565 (@Morphism_Context_rect2 Hole dir
566 (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
568 relation_of_product_of_arguments dir'' ?
569 (interp_relation_class_list E1 fcl)
570 (interp_relation_class_list E2 fcl))); intros.
571 change (directed_relation_of_relation_class dir'0 Out0
572 (apply_morphism ? ? (Function m) (interp_relation_class_list E1 m0))
573 (apply_morphism ? ? (Function m) (interp_relation_class_list E2 m0))).
575 apply apply_morphism_compatibility_Left2Right.
578 apply apply_morphism_compatibility_Right2Left.
584 unfold interp. Morphism_Context_rect2.
585 (*CSC: reflexivity used here*)
586 destruct S; destruct dir'0; simpl; (apply r || reflexivity).
588 destruct dir'0; exact r.
590 destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
591 unfold get_rewrite_direction; simpl.
592 destruct dir'0; destruct dir'';
594 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
595 (* the following mess with generalize/clear/intros is to help Coq resolving *)
596 (* second order unification problems. *)
597 generalize m c H0; clear H0 m c; inversion c;
598 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
599 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
600 destruct dir'0; destruct dir'';
602 unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
603 (* the following mess with generalize/clear/intros is to help Coq resolving *)
604 (* second order unification problems. *)
605 generalize m c H0; clear H0 m c; inversion c;
606 generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
607 (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
608 destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
611 (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
612 (eq_rect ? (fun T : Type => T) (interp E1 m) ?
613 (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
614 (eq_rect ? (fun T : Type => T) (interp E2 m) ?
615 (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
616 relation_of_product_of_arguments dir'' ?
617 (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
619 clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
620 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
622 rewrite <- H3; exact H0.
623 rewrite (opposite_direction_idempotent dir'0); exact H0.
624 destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
626 rewrite <- H3; exact H0.
627 rewrite (opposite_direction_idempotent dir'0); exact H0.
628 destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
632 (* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
634 record Setoid_Theory (A: Type) (Aeq: relation A) : Prop :=
635 {Seq_refl : ∀x:A. Aeq x x;
636 Seq_sym : ∀x y:A. Aeq x y → Aeq y x;
637 Seq_trans : ∀x y z:A. Aeq x y → Aeq y z → Aeq x z}.
639 (* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
641 (* A FEW EXAMPLES ON iff *)
643 (* impl IS A MORPHISM *)
645 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
649 (* and IS A MORPHISM *)
651 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
655 (* or IS A MORPHISM *)
657 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
661 (* not IS A MORPHISM *)
663 Add Morphism not with signature iff ==> iff as Not_Morphism.
667 (* THE SAME EXAMPLES ON impl *)
669 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
673 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
677 Add Morphism not with signature impl -→ impl as Not_Morphism2.
681 (* FOR BACKWARD COMPATIBILITY *)
682 Implicit Arguments Setoid_Theory [].
683 Implicit Arguments Seq_refl [].
684 Implicit Arguments Seq_sym [].
685 Implicit Arguments Seq_trans [].
688 (* Some tactics for manipulating Setoid Theory not officially
689 declared as Setoid. *)
691 Ltac trans_st x := match goal with
692 | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
693 apply (Seq_trans ? ? H) with x; auto
696 Ltac sym_st := match goal with
697 | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
698 apply (Seq_sym ? ? H); auto
701 Ltac refl_st := match goal with
702 | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
703 apply (Seq_refl ? ? H); auto
706 definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
707 Proof. constructor; congruence. Qed.