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))
]
elim In;
[ reduce;
intro;
- alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
apply iff_refl
| simplify;
intro x;
]
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;
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.
]
]
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).
apply
- (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class S)
+ (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
(λxx,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;
+ [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
+ | 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
+ | 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').
projects / helm.git / blobdiff