Sambin's & Valentini's toolbox (???)

diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma
new file mode 100644 (file)
index 0000000..81ed8b0
--- /dev/null
+++ b/helm/software/matita/library/demo/toolbox.ma
@@ -0,0 +1,174 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/cprop_connectives.ma".
+
+record iff (A,B: CProp) : CProp ≝
+ { if: A → B;
+   fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).
+
+record setoid : Type ≝
+ { carr:> Type;
+   eq: carr → carr → CProp;
+   refl: reflexive ? eq;
+   sym: symmetric ? eq;
+   trans: transitive ? eq
+ }.
+
+definition proofs: CProp → setoid.
+ 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.
+
+record setoid1 : Type ≝
+ { carr1:> Type;
+   eq1: carr1 → carr1 → CProp;
+   refl1: reflexive ? eq1;
+   sym1: symmetric ? eq1;
+   trans1: transitive ? eq1
+ }.
+
+definition CCProp: setoid1.
+ constructor 1;
+  [ apply CProp
+  | apply iff
+  | intro;
+    split;
+    intro;
+    assumption
+  | intros 3;
+    cases H; clear H;
+    split;
+    assumption
+  | intros 5;
+    cases H; cases H1; clear H H1;
+    split;
+    intros;
+    [ apply (H4 (H2 H))
+    | apply (H3 (H5 H))]]
+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')
+ }.
+ 
+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 ≝
+ { f1:1> A → B;
+   f1_ok: ∀a,a':A. eq ? a a' → eq1 ? (f1 a) (f1 a')
+ }.
+ 
+definition function_space_setoid: setoid → setoid → setoid.
+ intros (A B);
+ constructor 1;
+  [ apply (A ⇒ B);
+  | intros;
+    apply (∀a:A. eq ? (f a) (f1 a));
+  | simplify;
+    intros;
+    apply (f_ok ? ? x);
+    apply (refl A)
+  | simplify;
+    intros;
+    apply (sym B);
+    apply (H a)
+  | simplify;
+    intros;
+    apply (trans B ? (y a));
+    [ apply (H a)
+    | apply (H1 a)]]
+qed.
+    
+interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b).
+
+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
+ }.
+
+interpretation "isomorphism" 'iff x y = (isomorphism x y).
+
+axiom daemon: False.
+
+definition setoids: setoid1.
+ constructor 1;
+  [ apply setoid;
+  | apply isomorphism;
+  | intro;
+    split;
+     [1,2: constructor 1;
+        [1,3: intro; assumption;
+        |*: intros; assumption]
+     |3,4:
+       intros;
+       simplify;
+       apply refl;]
+  |*: elim daemon]
+qed.
+
+record dependent_product (A:setoid)  (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'))
+ }.
+
+record forall (A:setoid)  (B: function_space1 A CCProp): Type ≝
+ { fo:> ∀a:A.proofs (B a)
+ }.
+
+record subset (A: setoid) : Type ≝
+ { 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));
+    assumption
+  | apply H3; clear H2 H3;
+    apply (fi ?? (f1_ok ?? (mem ? V) ?? H));
+    apply H4;]
+qed.
+