(* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
(* Original author: Claudio Sacerdoti Coen. for the Coq system *)
-set "baseuri" "cic:/matita/technicalities/setoids".
-
include "datatypes/constructors.ma".
-include "logic/connectives2.ma".
include "logic/coimplication.ma".
+include "logic/connectives2.ma".
(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
definition function_type_of_morphism_signature :
Arguments → Relation_Class → Type.
intros (In Out); elim In;
- [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
- | exact (carrier_of_relation_class ? t → T)
+ [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
+ | exact (carrier_of_relation_class ? a → T)
]
qed.
generalize in match f; clear f;
[ elim a; simplify in f f1;
[ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
- | cases t;
+ | cases x;
[ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
| exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
]
| exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
- | cases t;
+ | cases x;
[ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
| exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
]
| exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
]
| change with
- ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
- (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
+ ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
+ (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
Prop).
- elim t; simplify in f f1;
+ elim a; simplify in f f1;
[1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- |2,4: cases t1;
+ |2,4: cases x;
[1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
|2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
]
definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
intro;
elim n;
- [ apply (singl ? (Leibniz ? t))
- | apply (cons ? (Leibniz ? t) a)
+ [ apply (singl ? (Leibniz ? a))
+ | apply (cons ? (Leibniz ? a) a1)
]
qed.
Morphism_Theory In' Out'.
intros;
apply (mk_Morphism_Theory ? ? f);
- unfold In' in f; clear In';
- unfold Out' in f; clear Out';
+ unfold In' in f ⊢ %; clear In';
+ unfold Out' in f ⊢ %; clear Out';
generalize in match f; clear f;
elim In;
[ unfold make_compatibility_goal;
- simplify;
- intros;
- whd;
+ whd; intros;
reflexivity
| simplify;
intro;
apply mk_Morphism_Theory;
[ exact Aeq
| unfold make_compatibility_goal;
- simplify;
+ simplify; unfold ASetoidClass; simplify;
intros;
split;
unfold transitive in H;
unfold symmetric in sym;
intro;
- auto new
+ [ apply (H x2 x1 x3 ? ?);
+ [apply (sym x1 x2 ?).
+ apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
+ | apply (H x1 x3 x ? ?);
+ [apply (H x1 x2 x3 ? ?);
+ [apply (H1).
+ |apply (H3).
+ ]
+ |apply (sym x x3 ?).
+ apply (H2).
+ ]
+ ]
].
qed.
(Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
intros;
apply mk_Morphism_Theory;
- reduce;
+ normalize;
[ exact Aeq
| intros;
split;
intro;
unfold transitive in H;
unfold symmetric in sym;
- auto depth=4.
+ [ apply (H x2 x1 x3 ? ?);
+ [apply (sym x1 x2 ?).
+ apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
+ | apply (H x1 x2 x ? ?);
+ [apply (H1).
+ |apply (H x2 x3 x ? ?);
+ [apply (H3).
+ |apply (sym x x3 ?).
+ apply (H x x3 x3 ? ?);
+ [apply (H2).
+ |apply (refl x3).
+ ]
+ ]
+ ]
+ ]
]
qed.
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intros;
- auto
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intro;
- auto
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
| generalize in match f; clear f;
unfold In'; clear In';
elim In;
- [ reduce;
+ [ normalize;
intro;
apply iff_refl
| simplify;
whd;
unfold impl;
intros;
- auto.
+ apply (H1 ?).apply (H ?).apply (H2).
+ autobatch.
qed.
(*DA PORTARE: Add Relation Prop impl
intros;
elim a;
[ apply None
- | apply (Some ? t)
+ | apply (Some ? x)
| apply None
- | apply (Some ? t)
+ | apply (Some ? x)
| apply None
]
qed.
definition product_of_arguments : Arguments → Type.
intro;
elim a;
- [ apply (carrier_of_relation_class ? t)
- | apply (Prod (carrier_of_relation_class ? t) T)
+ [ apply (carrier_of_relation_class ? a1)
+ | apply (Prod (carrier_of_relation_class ? a1) T)
]
qed.
elim In 0;
[ simplify;
intro;
- exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
+ exact (directed_relation_of_argument_class (get_rewrite_direction r a) a)
| intros;
- change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
- change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+ change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
+ change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
cases p (c p2);
cases p1 (c1 p3);
apply And;
[ exact
- (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+ (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
| exact (R p2 p3)
]
]
intro;
elim In;
[ exact (f p)
- | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+ | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
elim p;
- change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
- exact (f ? (f1 t1) t2)
+ change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out);
+ exact (f ? (f1 a1) b)
]
qed.
[ simplify in m1 m2 args1 args2 ⊢ %;
change in H1 with
(directed_relation_of_argument_class
- (get_rewrite_direction Right2Left t) t args1 args2);
+ (get_rewrite_direction Right2Left a) a args1 args2);
generalize in match H1; clear H1;
generalize in match H; clear H;
generalize in match args2; clear args2;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim a 0; simplify;
[ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
- simplify in H;
- simplify in H1;
- simplify;
apply H;
exact H1
| intros 8 (v T1 r Hr m1 m2 args1 args2);
- cases v;
+ cases v;
+ simplify;
intros (H H1);
- simplify in H1;
- apply H;
- exact H1
+ apply (H ? ? H1);
| intros;
apply H1;
exact H2
| intros 7 (v);
- cases v;
+ cases v; simplify;
intros (H H1);
- simplify in H1;
apply H;
exact H1
| intros;
exact H1
]
| change in m1 with
- (carrier_of_relation_class variance t →
+ (carrier_of_relation_class variance a →
function_type_of_morphism_signature n Out);
change in m2 with
- (carrier_of_relation_class variance t →
+ (carrier_of_relation_class variance a →
function_type_of_morphism_signature n Out);
change in args1 with
- ((carrier_of_relation_class ? t) × (product_of_arguments n));
+ ((carrier_of_relation_class ? a) × (product_of_arguments n));
change in args2 with
- ((carrier_of_relation_class ? t) × (product_of_arguments n));
+ ((carrier_of_relation_class ? a) × (product_of_arguments n));
generalize in match H2; clear H2;
elim args2 0; clear args2;
elim args1; clear args1;
+ simplify in H2;
+ change in H2:(? ? %) with
+ (relation_of_product_of_arguments Right2Left n b b1);
elim H2; clear H2;
- change in H4 with
- (relation_of_product_of_arguments Right2Left n t2 t4);
change with
- (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
- (apply_morphism n Out (m2 t1) t2));
+ (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1)
+ (apply_morphism n Out (m2 a1) b));
generalize in match H3; clear H3;
- generalize in match t3; clear t3;
- generalize in match t1; clear t1;
+ generalize in match a1; clear a1;
+ generalize in match a2; clear a2;
generalize in match H1; clear H1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim a 0;
[ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
simplify in H3;
change in H1 with
directed_relation_of_relation_class Left2Right ?
(apply_morphism ? ? m1 args1)
(apply_morphism ? ? m2 args2).
- intro;
- elim In;
- [ simplify in m1 m2 args1 args2 ⊢ %;
- change in H1 with
+ intro;
+ elim In 0; simplify; intros;
+ [ change in H1 with
(directed_relation_of_argument_class
- (get_rewrite_direction Left2Right t) t args1 args2);
+ (get_rewrite_direction Left2Right a) a args1 args2);
generalize in match H1; clear H1;
generalize in match H; clear H;
generalize in match args2; clear args2;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim a 0; simplify;
[ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
- simplify in H;
- simplify in H1;
- simplify;
apply H;
exact H1
| intros 8 (v T1 r Hr m1 m2 args1 args2);
exact H1
]
| change in m1 with
- (carrier_of_relation_class variance t →
+ (carrier_of_relation_class variance a →
function_type_of_morphism_signature n Out);
change in m2 with
- (carrier_of_relation_class variance t →
+ (carrier_of_relation_class variance a →
function_type_of_morphism_signature n Out);
change in args1 with
- ((carrier_of_relation_class ? t) × (product_of_arguments n));
+ ((carrier_of_relation_class ? a) × (product_of_arguments n));
change in args2 with
- ((carrier_of_relation_class ? t) × (product_of_arguments n));
+ ((carrier_of_relation_class ? a) × (product_of_arguments n));
generalize in match H2; clear H2;
elim args2 0; clear args2;
elim args1; clear args1;
+ simplify in H2; change in H2:(? ? %) with
+ (relation_of_product_of_arguments Left2Right n b b1);
elim H2; clear H2;
- change in H4 with
- (relation_of_product_of_arguments Left2Right n t2 t4);
change with
- (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
- (apply_morphism n Out (m2 t3) t4));
+ (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b)
+ (apply_morphism n Out (m2 a2) b1));
generalize in match H3; clear H3;
- generalize in match t3; clear t3;
- generalize in match t1; clear t1;
+ generalize in match a2; clear a2;
+ generalize in match a1; clear a1;
generalize in match H1; clear H1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim a 0;
[ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
- simplify in H3;
change in H1 with
(∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
| intro v;
rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
exact c1
- | split;
+ | simplify;split;
[ rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
exact c1
rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
exact c1
- | split;
+ | simplify; split;
[ rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
exact c1
(* impl IS A MORPHISM *)
Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-unfold impl; tauto.
+unfold impl; tautobatch.
Qed.
(* and IS A MORPHISM *)
Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
+ tautobatch.
Qed.
(* or IS A MORPHISM *)
Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
- tauto.
+ tautobatch.
Qed.
(* not IS A MORPHISM *)
Add Morphism not with signature iff ==> iff as Not_Morphism.
- tauto.
+ tautobatch.
Qed.
(* THE SAME EXAMPLES ON impl *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
Add Morphism not with signature impl -→ impl as Not_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
*)