From 00c99933872f0eb457e62354cc1a317e4359188e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Jul 2008 08:00:09 +0000
Subject: [PATCH] In some universe, membership is a morphism.

---
 helm/software/matita/library/demo/toolbox.ma | 110 ++++++++++++++-----
 1 file changed, 83 insertions(+), 27 deletions(-)

diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma
index 81ed8b065..7ee9e5da7 100644
--- a/helm/software/matita/library/demo/toolbox.ma
+++ b/helm/software/matita/library/demo/toolbox.ma
@@ -82,15 +82,15 @@ qed.
 
 record function_space (A,B: setoid): Type ≝
  { f:1> A → B;
-   f_ok: ∀a,a':A. eq ? a a' → eq ? (f a) (f a')
+   f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  }.
  
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "function_space" 'Imply a b = (function_space a b).
 
-record function_space1 (A: setoid) (B: setoid1): Type ≝
+record function_space1 (A: setoid1) (B: setoid1): Type ≝
  { f1:1> A → B;
-   f1_ok: ∀a,a':A. eq ? a a' → eq1 ? (f1 a) (f1 a')
+   f1_ok: ∀a,a':A. proofs (eq1 ? a a') → proofs (eq1 ? (f1 a) (f1 a'))
  }.
  
 definition function_space_setoid: setoid → setoid → setoid.
@@ -98,29 +98,56 @@ definition function_space_setoid: setoid → setoid → setoid.
  constructor 1;
   [ apply (A ⇒ B);
   | intros;
-    apply (∀a:A. eq ? (f a) (f1 a));
+    apply (∀a:A. proofs (eq ? (f a) (f1 a)));
   | simplify;
     intros;
     apply (f_ok ? ? x);
+    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;
     intros;
+    unfold carr; unfold proofs; simplify;
     apply (sym B);
-    apply (H a)
+    apply (f a)
   | simplify;
     intros;
+    unfold carr; unfold proofs; simplify;
     apply (trans B ? (y a));
-    [ apply (H a)
-    | apply (H1 a)]]
+    [ apply (f a)
+    | apply (f1 a)]]
 qed.
     
 interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b).
 
+definition function_space_setoid1: setoid1 → setoid1 → setoid.
+ intros (A B);
+ constructor 1;
+  [ apply (function_space1 A B);
+  | intros;
+    apply (∀a:A. proofs (eq1 ? (f a) (f1 a)));
+  | simplify;
+    intros;
+    apply (f1_ok ? ? x);
+    unfold proofs; simplify;
+    apply (refl1 A)
+  | simplify;
+    intros;
+    unfold proofs; simplify;
+    apply (sym1 B);
+    apply (f a)
+  | simplify;
+    intros;
+    unfold carr; unfold proofs; simplify;
+    apply (trans1 B ? (y a));
+    [ apply (f a)
+    | apply (f1 a)]]
+qed.
+
 record isomorphism (A,B: setoid): Type ≝
  { map1:> A ⇒ B;
    map2:> B ⇒ A;
-   inv1: ∀a:A. eq ? (map2 (map1 a)) a;
-   inv2: ∀b:B. eq ? (map1 (map2 b)) b
+   inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
+   inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
  }.
 
 interpretation "isomorphism" 'iff x y = (isomorphism x y).
@@ -139,36 +166,65 @@ definition setoids: setoid1.
      |3,4:
        intros;
        simplify;
+       unfold carr; unfold proofs; simplify;
        apply refl;]
   |*: elim daemon]
 qed.
 
-record dependent_product (A:setoid)  (B: function_space1 A setoids): Type ≝
+definition setoid1_of_setoid: setoid → setoid1.
+ intro;
+ constructor 1;
+  [ apply (carr s)
+  | apply (eq s)
+  | apply (refl s)
+  | apply (sym s)
+  | apply (trans s)
+  ]
+qed.
+
+coercion setoid1_of_setoid.
+
+(*
+record dependent_product (A:setoid1)  (B: function_space1 A setoids): Type ≝
  { dp:> ∀a:A.carr (B a);
-   dp_ok: ∀a,a':A. ∀p:eq ? a a'. eq ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a'))
+   dp_ok: ∀a,a':A. ∀p:proofs (eq1 ? a a'). proofs (eq1 ? (dp a) (map2 ?? (f1_ok A ? B ?? p) (dp a')))
  }.
+*)
 
-record forall (A:setoid)  (B: function_space1 A CCProp): Type ≝
+record forall (A:setoid)  (B: function_space1 A CCProp): CProp ≝
  { fo:> ∀a:A.proofs (B a)
  }.
 
-record subset (A: setoid) : Type ≝
+record subset (A: setoid) : CProp ≝
  { mem: function_space1 A CCProp
  }.
- 
-definition subset_eq ≝ λA:setoid.λU,V: subset A. ∀a:A. mem ? U a \liff mem ? V a.
 
-lemma mem_ok:
- ∀A:setoid.∀a,a':A.∀U,V: subset A.
-  eq ? a a' → subset_eq ? U V → mem ? U a \liff mem ? V a'.
- intros;
- cases (H1 a);
- split; intro H4;
-  [ lapply (H2 H4); clear H2 H3 H4;
-    apply (if ?? (f1_ok ?? (mem ? V) ?? H));
+definition ssubset: setoid → setoid1.
+ intro;
+ constructor 1;
+  [ apply (subset s);
+  | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
+  | simplify;
+    intros;
+    split;
+    intro;
     assumption
-  | apply H3; clear H2 H3;
-    apply (fi ?? (f1_ok ?? (mem ? V) ?? H));
-    apply H4;]
+  | simplify;
+    elim daemon
+  | elim daemon]
 qed.
-   
+ 
+definition mmem: ∀A:setoid. function_space_setoid1 (ssubset A) (function_space_setoid1 A CCProp).
+ intros;
+ constructor 1;
+  [ apply mem; 
+  | unfold function_space_setoid1; simplify;
+    intros (b b');
+    change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
+    unfold proofs; simplify; intros;
+    unfold proofs in c; simplify in c;
+    unfold ssubset in c; simplify in c;
+    cases (c a); clear c;
+    split;
+    assumption]
+qed.
\ No newline at end of file
-- 
2.39.2