Universe levels fixed.

diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma
index 7ee9e5da7f3d4fa4fb81e1078fa759f85d974cb8..2b076ee7f970bbe672e36bee7f3d1434cf6cfa71 100644 (file)
--- a/helm/software/matita/library/demo/toolbox.ma
+++ b/helm/software/matita/library/demo/toolbox.ma
@@ -14,6 +14,8 @@
 
 include "logic/cprop_connectives.ma".
 
+axiom daemon: False.
+
 record iff (A,B: CProp) : CProp ≝
  { if: A → B;
    fi: B → A
@@ -29,6 +31,10 @@ for @{ 'iff $a $b }.
 
 interpretation "logical iff" 'iff x y = (iff x y).
 
+definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+
 record setoid : Type ≝
  { carr:> Type;
    eq: carr → carr → CProp;
@@ -55,11 +61,26 @@ qed.
 record setoid1 : Type ≝
  { carr1:> Type;
    eq1: carr1 → carr1 → CProp;
-   refl1: reflexive ? eq1;
-   sym1: symmetric ? eq1;
-   trans1: transitive ? eq1
+   refl1: reflexive1 ? eq1;
+   sym1: symmetric1 ? eq1;
+   trans1: transitive1 ? eq1
  }.
 
+definition proofs1: CProp → setoid1.
+ intro;
+ constructor 1;
+  [ apply A
+  | intros;
+    alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+    apply True
+  | intro;
+    constructor 1
+  | intros 3;
+    constructor 1
+  | intros 5;
+    constructor 1]
+qed.
+
 definition CCProp: setoid1.
  constructor 1;
   [ apply CProp
@@ -86,17 +107,16 @@ record function_space (A,B: setoid): Type ≝
  }.
  
 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: setoid1) (B: setoid1): Type ≝
  { f1:1> A → B;
-   f1_ok: ∀a,a':A. proofs (eq1 ? a a') → proofs (eq1 ? (f1 a) (f1 a'))
+   f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
  }.
- 
+
 definition function_space_setoid: setoid → setoid → setoid.
  intros (A B);
  constructor 1;
-  [ apply (A ⇒ B);
+  [ apply (function_space A B);
   | intros;
     apply (∀a:A. proofs (eq ? (f a) (f1 a)));
   | simplify;
@@ -116,16 +136,14 @@ definition function_space_setoid: setoid → setoid → setoid.
     [ 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.
+definition function_space_setoid1: setoid1 → setoid1 → setoid1.
  intros (A B);
  constructor 1;
   [ apply (function_space1 A B);
   | intros;
-    apply (∀a:A. proofs (eq1 ? (f a) (f1 a)));
-  | simplify;
+    apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
+  |*: cases daemon] (* simplify;
     intros;
     apply (f1_ok ? ? x);
     unfold proofs; simplify;
@@ -140,20 +158,20 @@ definition function_space_setoid1: setoid1 → setoid1 → setoid.
     unfold carr; unfold proofs; simplify;
     apply (trans1 B ? (y a));
     [ apply (f a)
-    | apply (f1 a)]]
+    | apply (f1 a)]] *)
 qed.
 
+interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
+
 record isomorphism (A,B: setoid): Type ≝
- { map1:> A ⇒ B;
-   map2:> B ⇒ A;
+ { map1:> function_space_setoid A B;
+   map2:> function_space_setoid B A;
    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).
 
-axiom daemon: False.
-
 definition setoids: setoid1.
  constructor 1;
   [ apply setoid;
@@ -166,9 +184,9 @@ definition setoids: setoid1.
      |3,4:
        intros;
        simplify;
-       unfold carr; unfold proofs; simplify;
+       unfold proofs; simplify;
        apply refl;]
-  |*: elim daemon]
+  |*: cases daemon]
 qed.
 
 definition setoid1_of_setoid: setoid → setoid1.
@@ -178,26 +196,22 @@ definition setoid1_of_setoid: setoid → setoid1.
   | apply (eq s)
   | apply (refl s)
   | apply (sym s)
-  | apply (trans s)
-  ]
+  | apply (trans s)]
 qed.
 
 coercion setoid1_of_setoid.
 
 (*
-record dependent_product (A:setoid1)  (B: function_space1 A setoids): Type ≝
+record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
  { dp:> ∀a:A.carr (B a);
-   dp_ok: ∀a,a':A. ∀p:proofs (eq1 ? a a'). proofs (eq1 ? (dp a) (map2 ?? (f1_ok A ? B ?? p) (dp a')))
- }.
-*)
+   dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
+ }.*)
 
-record forall (A:setoid)  (B: function_space1 A CCProp): CProp ≝
- { fo:> ∀a:A.proofs (B a)
- }.
+record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
+ { fo:> ∀a:A.proofs (B a) }.
 
 record subset (A: setoid) : CProp ≝
- { mem: function_space1 A CCProp
- }.
+ { mem: A ⇒ CCProp }.
 
 definition ssubset: setoid → setoid1.
  intro;
@@ -210,21 +224,39 @@ definition ssubset: setoid → setoid1.
     intro;
     assumption
   | simplify;
-    elim daemon
-  | elim daemon]
+    cases daemon
+  | cases daemon]
 qed.
- 
-definition mmem: ∀A:setoid. function_space_setoid1 (ssubset A) (function_space_setoid1 A CCProp).
+
+definition mmem: ∀A:setoid. (ssubset A) ⇒ 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 proofs1; simplify; intros;
+    unfold proofs1 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
+qed.
+
+(*
+definition sand: CCProp ⇒ CCProp.
+
+definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
+ intro;
+ constructor 1;
+  [ intro;
+    constructor 1;
+     [ intro;
+       constructor 1;
+       constructor 1;
+       intro;
+       apply (mem ? c c2 ∧ mem ? c1 c2);
+     |
+  |
+  |
+*)
\ No newline at end of file