(* 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/coimplication.ma".
include "logic/connectives2.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 ? a → carrier_of_relation_class ? Out)
+ | exact (carrier_of_relation_class ? a → 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 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))
- | elim 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;
- [ 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))
+ elim a; simplify in f f1;
+ [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+ |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))
]
| exact (∀x. R (f x) (f1 x))
]
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;
- alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
apply iff_refl
| simplify;
intro x;
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.
App :
∀In,Out,dir'.
Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
- Morphism_Context Hole dir Out dir
+ Morphism_Context Hole dir Out dir'
| ToReplace : Morphism_Context Hole dir Hole dir
| ToKeep :
∀S,dir'.
Morphism_Context_List Hole dir dir'' L →
Morphism_Context_List Hole dir dir'' (cons ? S L).
+lemma Morphism_Context_rect2:
+ ∀Hole,dir.
+ ∀P:
+ ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
+ ∀P0:
+ ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
+ (∀In,Out,dir'.
+ ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
+ P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
+ P Hole dir (ToReplace Hole dir) →
+ (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
+ P (relation_class_of_reflexive_relation_class S) dir'
+ (ToKeep Hole dir S dir' c)) →
+ (∀S:Areflexive_Relation_Class.∀dir'.
+ ∀x:carrier_of_areflexive_relation_class S.
+ ∀r:relation_of_areflexive_relation_class S x x.
+ P (relation_class_of_areflexive_relation_class S) dir'
+ (ProperElementToKeep Hole dir S dir' x r)) →
+ (∀S:Argument_Class.∀dir',dir''.
+ ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+ ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+ P (relation_class_of_argument_class S) dir' m ->
+ P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
+ (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
+ ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+ ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+ P (relation_class_of_argument_class S) dir' m →
+ ∀m0:Morphism_Context_List Hole dir dir'' L.
+ P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
+ ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
+ P r r0 m
+≝
+ λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
+ let rec
+ F (rc:Relation_Class) (r0:rewrite_direction)
+ (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
+ ≝
+ match m return λrc.λr0.λm0.P rc r0 m0 with
+ [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
+ | ToReplace ⇒ f0
+ | ToKeep S dir' c ⇒ f1 S dir' c
+ | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
+ ]
+ and
+ F0 (r:rewrite_direction) (a:Arguments)
+ (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
+ ≝
+ match m return λr.λa.λm0.P0 r a m0 with
+ [ fcl_singl S dir' dir'' c m0 ⇒
+ f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+ | fcl_cons S L dir' dir'' c m0 m1 ⇒
+ f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+ m1 (F0 dir'' L m1)
+ ]
+in F.
+
+lemma Morphism_Context_List_rect2:
+ ∀Hole,dir.
+ ∀P:
+ ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
+ ∀P0:
+ ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
+ (∀In,Out,dir'.
+ ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
+ P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
+ P Hole dir (ToReplace Hole dir) →
+ (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
+ P (relation_class_of_reflexive_relation_class S) dir'
+ (ToKeep Hole dir S dir' c)) →
+ (∀S:Areflexive_Relation_Class.∀dir'.
+ ∀x:carrier_of_areflexive_relation_class S.
+ ∀r:relation_of_areflexive_relation_class S x x.
+ P (relation_class_of_areflexive_relation_class S) dir'
+ (ProperElementToKeep Hole dir S dir' x r)) →
+ (∀S:Argument_Class.∀dir',dir''.
+ ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+ ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+ P (relation_class_of_argument_class S) dir' m ->
+ P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
+ (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
+ ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+ ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+ P (relation_class_of_argument_class S) dir' m →
+ ∀m0:Morphism_Context_List Hole dir dir'' L.
+ P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
+ ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
+ P0 r a m
+≝
+ λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
+ let rec
+ F (rc:Relation_Class) (r0:rewrite_direction)
+ (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
+ ≝
+ match m return λrc.λr0.λm0.P rc r0 m0 with
+ [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
+ | ToReplace ⇒ f0
+ | ToKeep S dir' c ⇒ f1 S dir' c
+ | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
+ ]
+ and
+ F0 (r:rewrite_direction) (a:Arguments)
+ (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
+ ≝
+ match m return λr.λa.λm0.P0 r a m0 with
+ [ fcl_singl S dir' dir'' c m0 ⇒
+ f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+ | fcl_cons S L dir' dir'' c m0 m1 ⇒
+ f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+ m1 (F0 dir'' L m1)
+ ]
+in F0.
+
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.
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.
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));
- cases p;
- cases p1;
+ 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 a a1)
- | exact (R b b1)
+ (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
+ | exact (R p2 p3)
]
]
qed.
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
]
qed.
-(*
-Theorem apply_morphism_compatibility_Left2Right:
- ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
- (args1 args2: product_of_arguments In).
+theorem apply_morphism_compatibility_Left2Right:
+ ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
+ ∀args1,args2: product_of_arguments In.
make_compatibility_goal_aux ? ? m1 m2 →
relation_of_product_of_arguments Left2Right ? args1 args2 →
directed_relation_of_relation_class Left2Right ?
(apply_morphism ? ? m1 args1)
(apply_morphism ? ? m2 args2).
- induction In; intros.
- simpl in m1. m2. args1. args2. H0 |- *.
- destruct a; simpl in H; hnf in H0.
- apply H; exact H0.
- destruct v; simpl in H0; apply H; exact H0.
- apply H; exact H0.
- destruct v; simpl in H0; apply H; exact H0.
- rewrite H0; apply H; exact H0.
-
- simpl in m1. m2. args1. args2. H0 |- *.
- destruct args1; destruct args2; simpl.
- destruct H0.
- simpl in H.
- destruct a; simpl in H.
- apply IHIn.
- apply H; exact H0.
- exact H1.
- destruct v.
- apply IHIn.
- apply H; exact H0.
- exact H1.
- apply IHIn.
- apply H; exact H0.
- exact H1.
- apply IHIn.
- apply H; exact H0.
- exact H1.
- apply IHIn.
- destruct v; simpl in H. H0; apply H; exact H0.
- exact H1.
- rewrite H0; apply IHIn.
- apply H.
- exact H1.
-Qed.
+ intro;
+ elim In 0; simplify; intros;
+ [ change in H1 with
+ (directed_relation_of_argument_class
+ (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 a 0; simplify;
+ [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
+ apply H;
+ exact H1
+ | intros 8 (v T1 r Hr m1 m2 args1 args2);
+ cases v;
+ intros (H H1);
+ simplify in H1;
+ apply H;
+ exact H1
+ | intros;
+ apply H1;
+ exact H2
+ | intros 7 (v);
+ cases v;
+ intros (H H1);
+ simplify in H1;
+ apply H;
+ exact H1
+ | intros;
+ simplify in H1;
+ rewrite > H1;
+ apply H;
+ exact H1
+ ]
+ | change in m1 with
+ (carrier_of_relation_class variance a →
+ function_type_of_morphism_signature n Out);
+ change in m2 with
+ (carrier_of_relation_class variance a →
+ function_type_of_morphism_signature n Out);
+ change in args1 with
+ ((carrier_of_relation_class ? a) × (product_of_arguments n));
+ change in args2 with
+ ((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 with
+ (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 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 a 0;
+ [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
+ change in H1 with
+ (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+ | intro v;
+ elim v 0;
+ [ intros (T1 r 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));
+ | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
+ simplify in H3;
+ change in H1 with
+ (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+ ]
+ | intros (T1 r Hs 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;
+ elim v 0;
+ [ intros (T1 r 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));
+ | intros (T1 r m1 m2 H1 t1 t3 H3);
+ simplify in H3;
+ change in H1 with
+ (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+ ]
+ | intros (T m1 m2 H1 t1 t3 H3);
+ simplify in H3;
+ change in H1 with
+ (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
+ rewrite > H3;
+ simplify in H;
+ apply H;
+ [ apply H1
+ | assumption
+ ]
+ ] ;
+ simplify in H;
+ apply H;
+ [1,3,5,7,9,11:
+ apply H1;
+ assumption
+ |2,4,6,8,10,12:
+ assumption
+ ]
+ ]
+qed.
definition interp :
- ∀Hole dir Out dir'. carrier_of_relation_class Hole →
- Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
- intros Hole dir Out dir' H t.
- elim t using
- (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
- (fun ? L fcl => product_of_arguments L));
- intros.
- exact (apply_morphism ? ? (Function m) X).
- exact H.
- exact c.
- exact x.
- simpl;
- rewrite <-
- (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
- exact X.
- split.
- rewrite <-
+ ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
+ Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
+ intros (Hole dir Out dir' H t).
+ apply
+ (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
+ (λxx,L,fcl.product_of_arguments L));
+ intros;
+ [8: apply t
+ |7: skip
+ | exact (apply_morphism ? ? (Function ? ? m) p)
+ | exact H
+ | exact c
+ | exact x
+ | simplify;
+ rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
- exact X.
- exact X0.
+ exact c1
+ | simplify;split;
+ [ rewrite <
+ (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+ exact c1
+ | exact p
+ ]
+ ]
qed.
+
(*CSC: interp and interp_relation_class_list should be mutually defined. since
the proof term of each one contains the proof term of the other one. However
I cannot do that interactively (I should write the Fix by hand) *)
definition interp_relation_class_list :
- ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
+ ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
Morphism_Context_List Hole dir dir' L → product_of_arguments L.
- intros Hole dir dir' L H t.
- elim t using
- (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
- (fun ? L fcl => product_of_arguments L));
- intros.
- exact (apply_morphism ? ? (Function m) X).
- exact H.
- exact c.
- exact x.
- simpl;
- rewrite <-
- (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
- exact X.
- split.
- rewrite <-
+ intros (Hole dir dir' L H t);
+ apply
+ (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
+ (λxx,L,fcl.product_of_arguments L));
+ intros;
+ [8: apply t
+ |7: skip
+ | exact (apply_morphism ? ? (Function ? ? m) p)
+ | exact H
+ | exact c
+ | exact x
+ | simplify;
+ rewrite <
(about_carrier_of_relation_class_and_relation_class_of_argument_class S);
- exact X.
- exact X0.
+ exact c1
+ | simplify; split;
+ [ rewrite <
+ (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+ exact c1
+ | exact p
+ ]
+ ]
qed.
+(*
Theorem setoid_rewrite:
∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
(E: Morphism_Context Hole dir Out dir').
(* 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.
*)