1. CProp_n fixed to be equal to Type_n to better understand what is happening

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index c99239bebf18d663d0f9eb28c368a4d71a750203..f5141a2ed3bf34098ca92ea27126b90d515c2d95 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -174,34 +174,69 @@ lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (e
     assumption]
 qed.
 *)
-axiom daemon: False.
+(* senza questo exT "fresco", universe inconsistency *)
+inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
+  ex_introT: ∀w:A. P w → exT A P.
+
+lemma hint: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
+ [ apply setoid1_of_SET; apply U
+ | intros; apply c;]
+qed.
+coercion hint.
+
 (* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) ?(*(Ω \sup V)*).
-cases daemon; qed.
+definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
-    intros; simplify; split; intro; cases H; exists [1,3: apply w]
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | (*∃x:U. x ♮r y ∧ x ∈ S*)
+      exT ? (λx:carr U.x ♮r y ∧ x ∈ S) });
+    intros; simplify; split; intro; cases e1; exists [1,3: apply w]
      [ apply (. (#‡e)‡#); assumption
      | apply (. (#‡e ^ -1)‡#); assumption]
-  | intros; split; simplify; intros; cases H; exists [1,3: apply w]
+  | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
      [ apply (. #‡(#‡e1)); cases x; split; try assumption;
        apply (if ?? (e ??)); assumption
      | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
        apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
-(*
 (* the same as □ for a basic pair *)
 definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
-    intros; simplify; split; intros; apply H1;
-     [ apply (. #‡H \sup -1); assumption
-     | apply (. #‡H); assumption]
-  | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
-    apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:carr U. x ♮r y → x ∈ S});
+    intros; simplify; split; intros; apply f;
+     [ apply (. #‡e ^ -1); assumption
+     | apply (. #‡e); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+    apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
+qed.
+
+(* the same as * for a basic pair *)
+definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+ intros; constructor 1;
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S});
+    intros; simplify; split; intros; apply f;
+     [ apply (. e ^ -1‡#); assumption
+     | apply (. e‡#); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+    apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
+qed.
+
+(* the same as - for a basic pair *)
+definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+ intros; constructor 1;
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
+      exT ? (λy:carr V.x ♮r y ∧ y ∈ S) });
+    intros; simplify; split; intro; cases e1; exists [1,3: apply w]
+     [ apply (. (e‡#)‡#); assumption
+     | apply (. (e ^ -1‡#)‡#); assumption]
+  | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
+     [ apply (. #‡(#‡e1)); cases x; split; try assumption;
+       apply (if ?? (e ??)); assumption
+     | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
+       apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
+(*
 (* minus_image is the same as ext *)
 
 theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
@@ -263,12 +298,37 @@ include "o-algebra.ma".
 definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (SUBSETS o1) (SUBSETS o2).
  intros;
  constructor 1;
-  [ 
-  |
-  |
-  |
-  |
-  |
-  |
-  ]
-qed.
\ No newline at end of file
+  [ constructor 1;
+     [ apply (λU.image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.minus_star_image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.star_image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.minus_image ?? t U);
+     | intros; apply (#‡e); ]
+  | intros; split; intro;
+     [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
+       change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+       intros 4; apply f; exists; [apply a] split; assumption;
+     | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+       change with (∀a. a ∈ image ?? t p → a ∈ q);
+       intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+  | intros; split; intro;
+     [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+       change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+       intros 4; apply f; exists; [apply a] split; assumption;
+     | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+       change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+       intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+  | intros; split; intro; cases f; clear f;
+     [ cases x; cases x2; clear x x2; exists; [apply w1]
+        [ assumption;
+        | exists; [apply w] split; assumption]
+     | cases x1; cases x2; clear x1 x2; exists; [apply w1]
+        [ exists; [apply w] split; assumption;
+        | assumption; ]]]
+qed. sistemare anche l'hint da un'altra parte e capire l'exT (doppio!)
\ No newline at end of file