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 *)
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.
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.
intros;
whd;
intros;
- auto
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
intros;
whd;
intro;
- auto
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
whd;
unfold impl;
intros;
- auto.
+ apply (H1 ?).apply (H ?).apply (H2).
+ autobatch.
qed.
(*DA PORTARE: Add Relation Prop impl
(* 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.
*)