Let's play a bit with NG.

This library is NOT meant to be the final one, just a way to experiment with
features.

diff --git a/helm/software/matita/nlibrary/Makefile b/helm/software/matita/nlibrary/Makefile
new file mode 100644 (file)
index 0000000..33368a3
--- /dev/null
+++ b/helm/software/matita/nlibrary/Makefile
@@ -0,0 +1,19 @@
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+       ../matitac
+$(DIR).opt opt all.opt:
+       ../matitac.opt
+clean:
+       ../matitaclean
+clean.opt:
+       ../matitaclean.opt
+depend:
+       ../matitadep -dot
+depend.opt:
+       ../matitadep.opt -dot
+
+%.mo: 
+       ../matitac $*.ma
+%.mo.opt: 
+       ../matitac.opt $*.ma

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
new file mode 100644 (file)
index 0000000..857215f
--- /dev/null
+++ b/helm/software/matita/nlibrary/depends
@@ -0,0 +1,3 @@
+sets/sets.ma logic/connectives.ma
+logic/connectives.ma logic/pts.ma
+logic/pts.ma 

diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
new file mode 100644 (file)
index 0000000..7104158
--- /dev/null
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -0,0 +1,8 @@
+digraph g {
+  "sets/sets.ma" [];
+  "sets/sets.ma" -> "logic/connectives.ma" [];
+  "logic/connectives.ma" [];
+  "logic/connectives.ma" -> "logic/pts.ma" [];
+  "logic/pts.ma" [];
+  
+  }
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
new file mode 100644 (file)
index 0000000..631218a
Binary files /dev/null and b/helm/software/matita/nlibrary/depends.png differ

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
new file mode 100644 (file)
index 0000000..aca4af4
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+ninductive True: CProp ≝
+  I : True.
+
+ninductive False: CProp ≝.
+
+ndefinition Not: CProp → CProp ≝
+  λA. A → False.
+
+interpretation "logical not" 'not x = (Not x).
+
+ninductive And (A,B:CProp) : CProp ≝
+    conj : A → B → And A B.
+
+interpretation "logical and" 'and x y = (And x y).
+
+ninductive Or (A,B:CProp) : CProp ≝
+     or_introl : A → Or A B
+   | or_intror : B → Or A B.
+
+interpretation "logical or" 'or x y = (Or x y).
+
+(* BUG HERE: WHY IS IT ACCEPTED??? *)
+inductive Ex (A:Type[1]) (P:A \to CProp[1]) : CProp[0] \def
+    ex_intro: \forall x:A. P x \to Ex A P.
+
+interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma
new file mode 100644 (file)
index 0000000..623a87a
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/pts.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+universe constraint Type[0] < Type[1].
+universe constraint CProp[0] < CProp[1].
+universe constraint Type[0] ≤ CProp[0].
+universe constraint CProp[0] ≤ Type[0].
+universe constraint Type[1] ≤ CProp[1].
+universe constraint CProp[1] ≤ Type[1].

diff --git a/helm/software/matita/nlibrary/root b/helm/software/matita/nlibrary/root
new file mode 100644 (file)
index 0000000..8fa6d62
--- /dev/null
+++ b/helm/software/matita/nlibrary/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/ng

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
new file mode 100644 (file)
index 0000000..c06ce33
--- /dev/null
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/connectives.ma".
+
+nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
+(* This is a projection! *)
+ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f].
+
+interpretation "powerset" 'powerset A = (powerset A).
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset ? x).
+
+interpretation "mem" 'mem a S = (mem ? S a).
+
+ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
+
+interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
+
+ntheorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
+ #A; #S; #x; #H; nassumption;
+nqed.
+
+ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
+ #A; #S1; #S2; #S3; #H12; #H23; #x; #H;
+ napply (H23 ??); napply (H12 ??); nassumption;
+nqed.
+
+ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
+
+interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V).
+
+definition intersects:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+  [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
+    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
+  | intros;
+    split; intros 2; simplify in f ⊢ %;
+    [ apply (. (#‡H)‡(#‡H1)); assumption
+    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V).
+
+definition union:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+  [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
+    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
+  | intros;
+    split; intros 2; simplify in f ⊢ %;
+    [ apply (. (#‡H)‡(#‡H1)); assumption
+    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "union" 'union U V = (fun1 ??? (union ?) U V).
+
+definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
+ intros; constructor 1;
+  [ apply (λA:setoid.λa:A.{b | a=b});
+    intros; simplify;
+    split; intro;
+    apply (.= H1);
+     [ apply H | apply (H \sup -1) ]
+  | intros; split; intros 2; simplify in f ⊢ %; apply trans;
+     [ apply a |4: apply a'] try assumption; apply sym; assumption]
+qed.
+
+interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a).
\ No newline at end of file