include "datatypes/constructors.ma".
include "logic/connectives2.ma".
+include "logic/coimplication.ma".
(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
| AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
definition relation_class_of_argument_class : Argument_Class → Relation_Class.
- intro;
- unfold in a ⊢ %;
- elim a;
+ intros (a); cases a;
[ apply (SymmetricReflexive ? ? ? H H1)
| apply (AsymmetricReflexive ? something ? ? H)
| apply (SymmetricAreflexive ? ? ? H)
| apply (AsymmetricAreflexive ? something ? r)
- | apply (Leibniz ? T1)
+ | apply (Leibniz ? T)
]
qed.
definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros;
- elim x;
- [1,2,3,4,5: exact T1]
+ intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
qed.
-definition relation_of_relation_class :
+definition relation_of_relation_class:
∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2;
- elim R 0;
- simplify;
- [1,2: intros 4; apply r
- |3,4: intros 3; apply r
- | apply eq
- ]
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
qed.
lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
∀R.
carrier_of_relation_class ? (relation_class_of_argument_class R) =
carrier_of_relation_class ? R.
- intro;
- elim R;
- reflexivity.
- qed.
+intro; cases R; reflexivity.
+qed.
inductive nelistT (A : Type) : Type :=
singl : A → nelistT A
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)
- ]
+ intros (In Out); elim In;
+ [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
+ | exact (carrier_of_relation_class ? t → T)
+ ]
qed.
definition make_compatibility_goal_aux:
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))
- | elim t;
+ | cases t;
[ 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))
- | elim t;
+ | cases t;
[ 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))
]
(carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
Prop).
elim t; simplify in f f1;
- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | elim t1;
- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
- ]
- | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | elim t1;
- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
+ [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+ |2,4: cases t1;
+ [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))
]
| exact (∀x. R (f x) (f1 x))
]
generalize in match f; clear f;
elim In;
[ unfold make_compatibility_goal;
- simplify;
- intros;
- whd;
+ whd; intros;
reflexivity
| simplify;
intro;
unfold transitive in H;
unfold symmetric in sym;
intro;
- auto new
+ autobatch new
].
qed.
intro;
unfold transitive in H;
unfold symmetric in sym;
- auto depth=4.
+ autobatch depth=4.
]
qed.
intros;
whd;
intros;
- auto
+ autobatch
].
qed.
intros;
whd;
intro;
- auto
+ autobatch
].
qed.
elim In;
[ reduce;
intro;
- alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
apply iff_refl
| simplify;
intro x;
whd;
unfold impl;
intros;
- auto.
+ autobatch.
qed.
(*DA PORTARE: Add Relation Prop impl
definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
intros (dir R);
- cases (variance_of_argument_class R);
+ cases (variance_of_argument_class R) (a);
[ exact dir
| cases a;
[ exact dir (* covariant *)
definition directed_relation_of_argument_class:
∀dir:rewrite_direction.∀R: Argument_Class.
carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
- intros (dir R);
- generalize in match
- (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
- intro H;
- apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
- apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
- [ apply c
- | apply c1
- ]
+ intros (dir R c c1);
+ rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class R) in c c1;
+ exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R) c c1).
qed.
+
definition relation_of_product_of_arguments:
∀dir:rewrite_direction.∀In.
product_of_arguments In → product_of_arguments In → Prop.
| 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));
- cases p;
- cases p1;
+ cases p (c p2);
+ cases p1 (c1 p3);
apply And;
[ exact
- (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
- | exact (R b b1)
+ (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+ | exact (R p2 p3)
]
]
qed.
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim t 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;
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);
generalize in match H1; clear H1;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
- elim t 0;
+ elim t 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);
generalize in match m1; clear m1;
elim t 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;
(* 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.
*)