From: Claudio Sacerdoti Coen Date: Tue, 7 Jul 2009 13:15:30 +0000 (+0000) Subject: Let's play a bit with NG. X-Git-Tag: make_still_working~3745 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a9b394943d524181128816a4b02152aa79929fe;p=helm.git 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 index 000000000..33368a32d --- /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 index 000000000..857215f68 --- /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 index 000000000..710415825 --- /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 index 000000000..631218af1 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 index 000000000..aca4af449 --- /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 index 000000000..623a87a18 --- /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 index 000000000..8fa6d62d3 --- /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 index 000000000..c06ce33f6 --- /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