From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 6 Feb 2009 17:56:27 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4208
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddc0a7b3f0acd57f879e540e696f69ca0c20bbf5;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
index 7b10b4b9f..e52a42074 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
@@ -96,3 +96,27 @@ constructor 1;
 | intros; apply (id_neutral_right2 C2 ?? (ℳ_2 a));
 | intros; apply (id_neutral_left2 C2 ?? (ℳ_2 a));]
 qed.
+
+definition faithful ≝  
+   λC1,C2.λF:arrows3 CAT2 C1 C2.∀S,T.∀f,g:arrows2 C1 S T.
+     map_arrows2 ?? F ?? f = map_arrows2 ?? F ?? g → f=g.
+
+definition Ylppa : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.
+  faithful ?? F →  let rC2 ≝ Apply ?? F in arrows3 CAT2 rC2 C1.
+intros; constructor 1;
+[ intro; apply (ℱ_1 o);
+| intros; constructor 1; 
+  [ intros; apply (ℳ_1 c);
+  | apply hide; intros; apply f;  change in e with (ℳ_2 a = ℳ_2 a');
+    lapply (FmP ????? a) as H1; lapply (FmP ????? a') as H2;
+    cut (REW ????? (map_arrows2 ?? F ?? (ℳ_1 a)) = 
+         REW ????? (map_arrows2 ?? F ?? (ℳ_1 a')));[2:
+      apply (.= H1); apply (.= e); apply H2^-1;]
+    clear H1 H2 e; cases S in a a' Hcut; cases T;
+    cases H; cases H1; simplify; intros; assumption;]
+| intro; apply rule #;
+| intros; simplify; apply rule #;]
+qed.
+
+
+
diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
index 9e85452d5..3e2fe8f35 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
@@ -126,7 +126,8 @@ theorem BP_to_OBP_faithful:
  apply e;
 qed.
 
-theorem BP_to_OBP_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
+theorem BP_to_OBP_full: 
+   ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
  intros; 
  cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
  cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);
diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 1522dee22..a50ed8cc2 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -19,6 +19,115 @@ definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
 
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
+lemma category2_of_category1_respects_comp_r:
+ ∀C:category1.∀o1,o2,o3:C.
+  ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+   (comp1 ???? f g) =_\ID (comp2 (category2_of_category1 C) o1 o2 o3 f g).
+ intros; constructor 1; 
+qed.
+
+lemma category2_of_category1_respects_comp:
+ ∀C:category1.∀o1,o2,o3:C.
+  ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+   (comp2 (category2_of_category1 C) o1 o2 o3 f g) =_\ID (comp1 ???? f g).
+ intros; constructor 1; 
+qed.
+
+lemma POW_full': 
+  ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+   arrows1 REL S T.
+ intros;
+ constructor 1; constructor 1;
+  [ intros (x y); apply (y ∈ c {(x)});
+  | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+    apply (e1ࠠe); ]
+qed.
+
+(*
+lemma POW_full_image: 
+  ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+   exT22 ? (λg:arrows1 REL S T.or_f ?? (map_arrows2 ?? POW S T g) = f).
+ intros; letin g ≝ (? : carr1 (arrows1 REL S T)); [
+ constructor 1; constructor 1;
+  [ intros (x y); apply (y ∈ f {(x)});
+  | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+    apply (e1ࠠe); ]]
+exists [apply g]
+intro; split; intro; simplify; intro; 
+[ whd in f1; change in f1:(? ? (λ_:?.? ? ? ? ? % ?)) with (a1 ∈ f {(x)});
+  cases f1; cases x; clear f1 x; change with (a1 ∈ f a);
+  lapply (f_image_monotone ?? (map_arrows2 ?? POW S T g) (singleton ? w) a ? a1);
+  [2: whd in Hletin;
+      change in Hletin:(? ? (λ_:?.? ? ? ? ? % ?))
+      with (a1 ∈ f {(x)}); cases Hletin; cases x;
+           [ intros 2; change in f3 with (eq1 ? w a2); change with (a2 ∈ a);
+             apply (. f3^-1‡#); assumption;
+           | assumption; ]
+           
+           
+           
+  lapply (. (or_prop3 ?? (map_arrows2 ?? POW S T g) (singleton ? a1) a)^-1);
+   [ whd in Hletin:(? ? ? ? ? ? %);
+     change in Hletin:(? ? ? ? ? ? (? ? (? ? ? (λ_:?.? ? (λ_:?.? ? ? ? ? % ?)) ?)))
+     with (y ∈ f {(x)});
+     cases Hletin; cases x1; cases x2; 
+  
+   [ cases Hletin; change in x with (eq1 ? a1 w1); apply (. x‡#); assumption;
+   | exists; [apply w] assumption ]
+
+
+  clear g;
+ cases f1; cases x; simplify in f2; change with (a1 ∈ (f a));
+  lapply depth=0 (let x ≝ POW in or_prop3 (POW S) (POW T) (map_arrows2 ?? POW S T g));
+  lapply (Hletin {(w)} {(a1)}).
+  lapply (if ?? Hletin1); [2: clear Hletin Hletin1;
+    exists; [apply a1] [whd; exists[apply w] split; [assumption;|change with (w = w); apply rule #]]
+    change with (a1=a1); apply rule #;]
+  clear Hletin Hletin1; cases Hletin2; whd in x2; 
+qed.
+*)
+lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+ intros;
+ constructor 1;
+  [ apply (b c);
+  | intros; apply (#‡e); ]
+qed.
+
+notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+interpretation "map arrows 2" 'map_arrows F x = (fun12 _ _ (map_arrows2 _ _ F _ _) x).
+
+definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+constructor 1; constructor 1;
+[ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
+  apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
+| intros (a b H); split; intro E; cases E; clear E; exists; [1,3:apply w]
+  [ apply (. #‡(H^-1‡#)); | apply (. #‡(H‡#));] assumption]
+qed.
+
+alias symbol "singl" = "singleton".
+lemma eq_cones_to_eq_rel: 
+  ∀S,T. ∀f,g: arrows1 REL S T.
+   (∀x. curry ??? (image ??) f {(x)} = curry ??? (image ??) g {(x)}) → f = g.
+intros; intros 2 (a b); split; intro;
+[ cases (f1 a); lapply depth=0 (s b); clear s s1;
+  lapply (Hletin); clear Hletin;
+   [ cases Hletin1; cases x; change in f4 with (a = w);
+     change with (a ♮g b); apply (. f4‡#); assumption;
+   | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]
+| cases (f1 a); lapply depth=0 (s1 b); clear s s1;
+  lapply (Hletin); clear Hletin;
+   [ cases Hletin1; cases x; change in f4 with (a = w);
+     change with (a ♮f b); apply (. f4‡#); assumption;
+   | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]]
+qed.
+
+variant eq_cones_to_eq_rel': 
+  ∀S,T. ∀f,g: arrows1 REL S T.
+   (∀x:S. or_f ?? (map_arrows2 ?? POW S T f) {(x)} = or_f ?? (map_arrows2 ?? POW S T g) {(x)}) →
+    f = g
+≝ eq_cones_to_eq_rel.
+
 lemma rOR_full : 
   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
     exT22 ? (λg:arrows2 rOBP s t.
@@ -32,39 +141,33 @@ 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)));
- [2:
-   exists;
+intro; whd in s_1 t_1; 
+letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1))); 
+[2:
+  exists;
     [ constructor 1;
        [2: simplify; apply R;
        | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
        | simplify; apply rule #; ]]
    simplify;
- | constructor 1;
-    [2: constructor 1; constructor 1;
-      [ intros (x y); apply (y ∈ f (singleton ? x));
-      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
-        unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
-        apply rule #; ]
-    |1: constructor 1; constructor 1;
-      [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
-      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
-        unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
-        apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
-    | whd; simplify; intros; simplify;
-      whd in ⊢ (? % %); simplify in ⊢ (? % %);
-      lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
-       [ cases Hletin; clear Hletin;
-         lapply (s y); clear s;
-whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
-whd in Hletin; simplify in Hletin;
-         lapply (s1 y); clear s1;      
-     split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
-      cases f1; clear f1; cases x1; clear x1;
-       [
-       | exists;
-       ]
+|1: constructor 1;   
+    [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
+    |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
+        letin r ≝ (u ∘ (or_f ?? f));
+        letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
+        letin r' ≝ (r ∘ xxx); clearbody r';
+        apply (POW_full' (concr s_1) (concr t_1) r');    
+    | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
+      apply eq_cones_to_eq_rel'; intro;
+      apply
+       (cic:/matita/logic/equality/eq_elim_r''.con ?????
+         (category2_of_category1_respects_comp_r : ?));
+      apply rule (.= (#‡#));
+      apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#); 
+      apply sym2;
+      apply (.= (respects_comp2 ?? POW (concr s_1) (form s_1) (form t_1) (⊩\sub s_1) (pi1exT22 ?? (POW_full (form s_1) (form t_1) (Ocont_rel ?? f)))));
+      apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
+      apply sym2;      
  ]
 
 STOP;
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index af3015eb3..bc13ecfd7 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -182,6 +182,23 @@ theorem POW_faithful:
   |*: cases Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;]
 qed.
 
+
+lemma currify: ∀A,B,C. binary_morphism1 A B C → A → unary_morphism1 B C.
+intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
+qed.
+
+(*
+alias symbol "singl" = "singleton".
+alias symbol "eq" = "setoid eq".
+lemma in_singleton_to_eq : ∀A:setoid.∀y,x:A.y ∈ {(x)} → (eq1 A) y x.
+intros; apply sym1; apply f;
+qed.  
+
+lemma eq_to_in_singleton : ∀A:setoid.∀y,x:A.eq1 A y x → y ∈ {(x)}.
+intros; apply (e^-1);
+qed.
+*)
+
 interpretation "lifting singl" 'singl x = 
  (fun11 _ (objs2 (POW _))  (singleton _) x).