apply (H1 \sup -1);]
qed.
-definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
- intros;
- constructor 1;
- [ intros (r r1);
+lemma relation_pair_composition:
+ ∀o1,o2,o3: basic_pair.
+ relation_pair_setoid o1 o2 → relation_pair_setoid o2 o3 → relation_pair_setoid o1 o3.
+intros 3 (o1 o2 o3);
+ intros (r r1);
constructor 1;
[ apply (r1 \sub\c ∘ r \sub\c)
| apply (r1 \sub\f ∘ r \sub\f)
apply (.= ASSOC ^ -1);
apply (.= H‡#);
apply ASSOC]
- | intros;
+qed.
+
+lemma relation_pair_composition_is_morphism:
+ ∀o1,o2,o3: basic_pair.
+ ∀a,a':relation_pair_setoid o1 o2.
+ ∀b,b':relation_pair_setoid o2 o3.
+ a=a' → b=b' →
+ relation_pair_composition o1 o2 o3 a b
+ = relation_pair_composition o1 o2 o3 a' b'.
+intros 3 (o1 o2 o3);
+ intros;
change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
apply (.= e‡#);
apply (.= ASSOC);
apply (.= #‡(commute ?? b')\sup -1);
- apply (ASSOC ^ -1)]
+ apply (ASSOC ^ -1);
qed.
-
-definition BP: category1.
+
+definition relation_pair_composition_morphism:
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ intros;
constructor 1;
- [ apply basic_pair
- | apply relation_pair_setoid
- | apply id_relation_pair
- | apply relation_pair_composition
- | intros;
+ [ apply relation_pair_composition;
+ | apply relation_pair_composition_is_morphism;]
+qed.
+
+lemma relation_pair_composition_morphism_assoc:
+Πo1:basic_pair
+.Πo2:basic_pair
+ .Πo3:basic_pair
+ .Πo4:basic_pair
+ .Πa12:relation_pair_setoid o1 o2
+ .Πa23:relation_pair_setoid o2 o3
+ .Πa34:relation_pair_setoid o3 o4
+ .relation_pair_composition_morphism o1 o3 o4
+ (relation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =relation_pair_composition_morphism o1 o2 o4 a12
+ (relation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;
change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
alias symbol "refl" = "refl1".
alias symbol "prop2" = "prop21".
apply (ASSOC‡#);
- | intros;
+qed.
+
+lemma relation_pair_composition_morphism_respects_id:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o1 o2 (id_relation_pair o1) a=a.
+ intros;
change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
- apply ((id_neutral_right1 ????)‡#);
- | intros;
+ apply ((id_neutral_right1 ????)‡#);
+qed.
+
+lemma relation_pair_composition_morphism_respects_id_r:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o2 o2 a (id_relation_pair o2)=a.
+ intros;
change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
- apply ((id_neutral_left1 ????)‡#);]
+ apply ((id_neutral_left1 ????)‡#);
qed.
+definition BP: category1.
+ constructor 1;
+ [ apply basic_pair
+ | apply relation_pair_setoid
+ | apply id_relation_pair
+ | apply relation_pair_composition_morphism
+ | apply relation_pair_composition_morphism_assoc;
+ | apply relation_pair_composition_morphism_respects_id;
+ | apply relation_pair_composition_morphism_respects_id_r;]
+qed.
+
definition basic_pair_of_BP : objs1 BP → basic_pair ≝ λx.x.
coercion basic_pair_of_BP.
| apply commute;]]
qed.
-definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
- constructor 1;
- [ apply o_basic_pair_of_basic_pair;
- | intros; constructor 1;
- [ apply (o_relation_pair_of_relation_pair S T);
- | intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify;
+lemma o_relation_pair_of_relation_pair_is_morphism :
+ ∀S,T:category2_of_category1 BP.
+ ∀a,b:arrows2 (category2_of_category1 BP) S T.a=b →
+ (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T)))
+ (o_relation_pair_of_relation_pair S T a) (o_relation_pair_of_relation_pair S T b).
+intros 2 (S T);
+ intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify;
unfold o_basic_pair_of_basic_pair; simplify;
[ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
| change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
apply sym2;
apply prop12;
apply Eab;
- ]
- | simplify; intros; whd; split;
+qed.
+
+lemma o_relation_pair_of_relation_pair_morphism :
+ ∀S,T:category2_of_category1 BP.
+ unary_morphism2 (arrows2 (category2_of_category1 BP) S T)
+ (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T)).
+intros (S T);
+ constructor 1;
+ [ apply (o_relation_pair_of_relation_pair S T);
+ | apply (o_relation_pair_of_relation_pair_is_morphism S T)]
+qed.
+
+lemma o_relation_pair_of_relation_pair_morphism_respects_id:
+ ∀o:category2_of_category1 BP.
+ o_relation_pair_of_relation_pair_morphism o o (id2 (category2_of_category1 BP) o)
+ = id2 OBP (o_basic_pair_of_basic_pair o).
+ simplify; intros; whd; split;
[ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
| change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
| change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
simplify;
apply prop12;
apply prop22;[2,4,6,8: apply rule #;]
- apply (respects_id2 ?? POW (concr o));
- | simplify; intros; whd; split;
+ apply (respects_id2 ?? POW (concr o));
+qed.
+
+lemma o_relation_pair_of_relation_pair_morphism_respects_comp:
+ ∀o1,o2,o3:category2_of_category1 BP.
+ ∀f1:arrows2 (category2_of_category1 BP) o1 o2.
+ ∀f2:arrows2 (category2_of_category1 BP) o2 o3.
+ (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair o1) (o_basic_pair_of_basic_pair o3)))
+ (o_relation_pair_of_relation_pair_morphism o1 o3 (f2 ∘ f1))
+ (comp2 OBP ???
+ (o_relation_pair_of_relation_pair_morphism o1 o2 f1)
+ (o_relation_pair_of_relation_pair_morphism o2 o3 f2)).
+ simplify; intros; whd; split;
[ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
| change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
| change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
simplify;
apply prop12;
apply prop22;[2,4,6,8: apply rule #;]
- apply (respects_comp2 ?? POW (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);]
+ apply (respects_comp2 ?? POW (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);
+qed.
+
+definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
+ constructor 1;
+ [ apply o_basic_pair_of_basic_pair;
+ | intros; apply o_relation_pair_of_relation_pair_morphism;
+ | apply o_relation_pair_of_relation_pair_morphism_respects_id;
+ | apply o_relation_pair_of_relation_pair_morphism_respects_comp;]
qed.
theorem BP_to_OBP_faithful:
apply (H1 \sup -1);]
qed.
-definition Orelation_pair_composition:
- ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3).
- intros;
- constructor 1;
- [ intros (r r1);
+lemma Orelation_pair_composition:
+ ∀o1,o2,o3:Obasic_pair.
+ Orelation_pair_setoid o1 o2 → Orelation_pair_setoid o2 o3→Orelation_pair_setoid o1 o3.
+intros 3 (o1 o2 o3);
+ intros (r r1);
constructor 1;
[ apply (r1 \sub\c ∘ r \sub\c)
| apply (r1 \sub\f ∘ r \sub\f)
apply rule (.= ASSOC ^ -1);
apply (.= H‡#);
apply rule ASSOC]
- | intros;
+qed.
+
+
+lemma Orelation_pair_composition_is_morphism:
+ ∀o1,o2,o3:Obasic_pair.
+ Πa,a':Orelation_pair_setoid o1 o2.Πb,b':Orelation_pair_setoid o2 o3.
+ a=a' →b=b' →
+ Orelation_pair_composition o1 o2 o3 a b
+ = Orelation_pair_composition o1 o2 o3 a' b'.
+intros;
change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
apply (.= e‡#);
apply rule (.= ASSOC);
apply (.= #‡(Ocommute ?? b')\sup -1);
- apply rule (ASSOC \sup -1)]
+ apply rule (ASSOC \sup -1);
qed.
-
-definition OBP: category2.
- constructor 1;
- [ apply Obasic_pair
- | apply Orelation_pair_setoid
- | apply Oid_relation_pair
- | apply Orelation_pair_composition
- | intros;
+
+definition Orelation_pair_composition_morphism:
+ ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3).
+intros; constructor 1;
+[ apply Orelation_pair_composition;
+| apply Orelation_pair_composition_is_morphism;]
+qed.
+
+lemma Orelation_pair_composition_morphism_assoc:
+∀o1,o2,o3,o4:Obasic_pair
+ .Πa12:Orelation_pair_setoid o1 o2
+ .Πa23:Orelation_pair_setoid o2 o3
+ .Πa34:Orelation_pair_setoid o3 o4
+ .Orelation_pair_composition_morphism o1 o3 o4
+ (Orelation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =Orelation_pair_composition_morphism o1 o2 o4 a12
+ (Orelation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;
change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
apply rule (ASSOC‡#);
- | intros;
+qed.
+
+lemma Orelation_pair_composition_morphism_respects_id:
+Πo1:Obasic_pair
+.Πo2:Obasic_pair
+ .Πa:Orelation_pair_setoid o1 o2
+ .Orelation_pair_composition_morphism o1 o1 o2 (Oid_relation_pair o1) a=a.
+ intros;
change with (⊩ ∘ (a\sub\c ∘ (Oid_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
apply ((id_neutral_right2 ????)‡#);
- | intros;
+qed.
+
+lemma Orelation_pair_composition_morphism_respects_id_r:
+Πo1:Obasic_pair
+.Πo2:Obasic_pair
+ .Πa:Orelation_pair_setoid o1 o2
+ .Orelation_pair_composition_morphism o1 o2 o2 a (Oid_relation_pair o2)=a.
+intros;
change with (⊩ ∘ ((Oid_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
- apply ((id_neutral_left2 ????)‡#);]
+ apply ((id_neutral_left2 ????)‡#);
+qed.
+
+definition OBP: category2.
+ constructor 1;
+ [ apply Obasic_pair
+ | apply Orelation_pair_setoid
+ | apply Oid_relation_pair
+ | apply Orelation_pair_composition_morphism
+ | apply Orelation_pair_composition_morphism_assoc;
+ | apply Orelation_pair_composition_morphism_respects_id;
+ | apply Orelation_pair_composition_morphism_respects_id_r;]
qed.
definition Obasic_pair_of_objs2_OBP: objs2 OBP → Obasic_pair ≝ λx.x.
lemma rOR_full :
∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
exT22 ? (λg:arrows2 rOBP s t.
- map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intro; cases s (s_2 s_1 s_eq); clear s;
-whd in ⊢ (?→? (? ? (? ?? ? %) ?)→?);
-whd in ⊢ (?→?→? ? (λ_:?.? ? ? (? ? ? (? ? ? (? ? ? ? % ?) ?)) ?));;
-include "logic/equality.ma".
-lapply (
-match s_eq in eq return
- (λright_1:?.(λmatched:(eq (objs2 OBP) (map_objs2 (category2_of_category1 BP) OBP BP_to_OBP s_1) right_1).
- (∀t:(objs2 rOBP).
- (∀f:(carr2 (arrows2 OBTop (map_objs2 OBP OBTop OR right_1) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))).
- (exT22 (carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t))
- (λg:(carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)).
- (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
- (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
- (carr1_OF_Ocontinuous_relation
- (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP (*XXX*)right_1 s_1 matched)))
- (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
- (fun12
- (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
- (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))
- (map_arrows2 OBP OBTop OR right_1 (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
- (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t g)))
- ?)))))))
- with
- [ refl_eq ⇒ ?
-]);
- STOP.
- (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
- (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
- (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (fun12 (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) (map_arrows2 OBP OBTop OR ? (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched) t g)))
- (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) f)))))))) with
- [ refl_eq ⇒ ?
-]);
-cases s_eq; clear s_eq s_2;
-intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
+ map_arrows2 ?? OR ?? (ℳ_2 g) = f).
+intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
+change in match (F2 ??? (mk_Fo ??????)) with s_2;
+cases s_eq; clear s_eq s_2;
+letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
+cases t (t_2 t_1 t_eq); clear t;
+change in match (F2 ??? (mk_Fo ??????)) with t_2;
+cases t_eq; clear t_eq t_2;
+letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
intro; whd in s_1 t_1;
letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
| whd; simplify; intros; simplify;
whd in ⊢ (? % %); simplify in ⊢ (? % %);
lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
- [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin;
+ [ cases Hletin; clear Hletin;
lapply (s y); clear s;
whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
whd in Hletin; simplify in Hletin;
0.5.7 - .../01/2009 - Pàdoa release
+ * cases tactic speedup in the simplest case of an inductive type
+ hose right parameters have all to be abstracted when the outtype is
+ built
* maction support added to output notation (adopted for "=" that
expands to "= \sub T" to show the equality type)
* generation of derived lemmas rewritten to be based on hooks that
projects / helm.git / commitdiff