From e0b576827e1d1dd243f304e68cda6b0c7cc21978 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 24 Jul 2007 11:52:05 +0000 Subject: [PATCH] New developement LOGIC about the cut elimination of implication for Sambin's basic logic; one of the rules must be corrected (work is in progress) --- .../matita/contribs/LOGIC/CLE/defs.ma | 14 +++ .../matita/contribs/LOGIC/Insert/defs.ma | 26 +++++ .../matita/contribs/LOGIC/Insert/fun.ma | 33 +++++++ .../matita/contribs/LOGIC/Insert/inv.ma | 56 +++++++++++ .../matita/contribs/LOGIC/Insert/props.ma | 72 ++++++++++++++ .../matita/contribs/LOGIC/Track/defs.ma | 43 +++++++++ .../matita/contribs/LOGIC/Track/inv.ma | 75 +++++++++++++++ .../matita/contribs/LOGIC/Track/order.ma | 95 +++++++++++++++++++ .../matita/contribs/LOGIC/Track/props.ma | 53 +++++++++++ .../contribs/LOGIC/datatypes/Context.ma | 31 ++++++ .../contribs/LOGIC/datatypes/Formula.ma | 27 ++++++ .../matita/contribs/LOGIC/datatypes/Proof.ma | 33 +++++++ .../contribs/LOGIC/datatypes/Sequent.ma | 46 +++++++++ helm/software/matita/contribs/LOGIC/makefile | 39 ++++++++ .../matita/contribs/LOGIC/preamble.ma | 22 +++++ helm/software/matita/contribs/Makefile | 2 +- .../software/matita/contribs/developments.txt | 1 + helm/software/matita/contribs/prova.ma | 38 ++++++++ 18 files changed, 705 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/contribs/LOGIC/CLE/defs.ma create mode 100644 helm/software/matita/contribs/LOGIC/Insert/defs.ma create mode 100644 helm/software/matita/contribs/LOGIC/Insert/fun.ma create mode 100644 helm/software/matita/contribs/LOGIC/Insert/inv.ma create mode 100644 helm/software/matita/contribs/LOGIC/Insert/props.ma create mode 100644 helm/software/matita/contribs/LOGIC/Track/defs.ma create mode 100644 helm/software/matita/contribs/LOGIC/Track/inv.ma create mode 100644 helm/software/matita/contribs/LOGIC/Track/order.ma create mode 100644 helm/software/matita/contribs/LOGIC/Track/props.ma create mode 100644 helm/software/matita/contribs/LOGIC/datatypes/Context.ma create mode 100644 helm/software/matita/contribs/LOGIC/datatypes/Formula.ma create mode 100644 helm/software/matita/contribs/LOGIC/datatypes/Proof.ma create mode 100644 helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma create mode 100644 helm/software/matita/contribs/LOGIC/makefile create mode 100644 helm/software/matita/contribs/LOGIC/preamble.ma diff --git a/helm/software/matita/contribs/LOGIC/CLE/defs.ma b/helm/software/matita/contribs/LOGIC/CLE/defs.ma new file mode 100644 index 000000000..7a2c7606c --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/CLE/defs.ma @@ -0,0 +1,14 @@ +set "baseuri" "cic:/matita/LOGIC/CLE/defs". + +(* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS +*) + +include "datatypes/Context.ma". + +inductive CLE: Nat \to Context \to Prop \def + | cle_zero: \forall Q. CLE zero Q + | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R) +. + +interpretation "order relation between positions and contexts" + 'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y). diff --git a/helm/software/matita/contribs/LOGIC/Insert/defs.ma b/helm/software/matita/contribs/LOGIC/Insert/defs.ma new file mode 100644 index 000000000..7b72c5c7c --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Insert/defs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Insert/defs". + +(* INSERT RELATION FOR CONTEXTS +*) + +include "datatypes/Context.ma". + +inductive Insert (S:Sequent): Nat \to Context \to Context \to Prop \def + | insert_zero: \forall P. Insert S zero P (abst P S) + | insert_succ: \forall P,Q,R,i. + Insert S i P Q \to Insert S (succ i) (abst P R) (abst Q R) +. diff --git a/helm/software/matita/contribs/LOGIC/Insert/fun.ma b/helm/software/matita/contribs/LOGIC/Insert/fun.ma new file mode 100644 index 000000000..5661c0a27 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Insert/fun.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Insert/fun". + +include "CLE/defs.ma". +include "Insert/inv.ma". + +(* Functional properties ****************************************************) + +theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q. + intros 4; elim H; clear H i P; + decompose; autobatch. +qed. + +theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to + \forall S2. Insert S2 i P Q \to S1 = S2. + intros 5; elim H; clear H i P Q; + [ lapply linear insert_inv_zero to H1; subst; autobatch + | lapply linear insert_inv_succ to H3; decompose; subst; autobatch + ]. +qed. diff --git a/helm/software/matita/contribs/LOGIC/Insert/inv.ma b/helm/software/matita/contribs/LOGIC/Insert/inv.ma new file mode 100644 index 000000000..229b9cc33 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Insert/inv.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Insert/inv". + +(* +*) + +include "Insert/defs.ma". + +theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S. + intros; inversion H; clear H; intros; subst; autobatch. +qed. + +theorem insert_inv_succ: \forall S,Q1,Q2,i. Insert S (succ i) Q1 Q2 \to + \exists P1,P2,R. Insert S i P1 P2 \land + Q1 = abst P1 R \land Q2 = abst P2 R. + intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. +qed. + +theorem insert_inv_leaf_1: \forall Q,S,i. Insert S i leaf Q \to + i = zero \land Q = S. + intros. inversion H; clear H; intros; subst. autobatch. +qed. + +theorem insert_inv_abst_1: \forall P,Q,R,S,i. Insert S i (abst P R) Q \to + (i = zero \land Q = (abst (abst P R) S)) \lor + \exists n, c1. + i = succ n \land Q = abst c1 R \land + Insert S n P c1. + intros. inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. +qed. + +theorem insert_inv_leaf_2: \forall P,S,i. Insert S i P leaf \to False. + intros. inversion H; clear H; intros; subst. +qed. + +theorem insert_inv_abst_2: \forall P,i. \forall R,S:Sequent. + Insert S i P R \to + i = zero \land P = leaf \land R = S. + intros. inversion H; clear H; intros; subst; + [ autobatch + | clear H1. lapply linear insert_inv_leaf_2 to H. decompose + ]. +qed. diff --git a/helm/software/matita/contribs/LOGIC/Insert/props.ma b/helm/software/matita/contribs/LOGIC/Insert/props.ma new file mode 100644 index 000000000..1e0bc5454 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Insert/props.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Insert/props". + +(* +*) + +include "Insert/fun.ma". + +theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to + \forall Q2,S2,i2. Insert S2 i2 P Q2 \to + \exists Q,j1,j2. + Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q. + intros 5. elim H; clear H i1 P Q1; + [ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8 + | lapply linear insert_inv_abst_1 to H3. decompose; subst; + [ autobatch depth = 7 size = 8 + | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8 + ] + ]. +qed. + +theorem insert_trans: \forall P1,Q1,S1,i1. Insert S1 i1 P1 Q1 \to + \forall Q2,S2,i2. Insert S2 i2 Q1 Q2 \to + \exists P2,j1,j2. + Insert S2 j2 P1 P2 \land Insert S1 j1 P2 Q2. + intros 5. elim H; clear H i1 P1 Q1; + [ lapply linear insert_inv_abst_1 to H1. decompose; subst; autobatch depth = 6 size = 7 + | lapply linear insert_inv_abst_1 to H3. decompose; subst; + [ clear H2. autobatch depth = 7 size = 8 + | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8 + ] + ]. +qed. + +theorem insert_conf_rev: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to + \forall P2,S2,i2. Insert S2 i2 P2 Q \to + (i1 = i2 \land P1 = P2) \lor + \exists Q1,Q2,j1,j2. + Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2. + intros 5; elim H; clear H i1 P1 Q; + [ inversion H1; clear H1; intros; subst; autobatch depth = 7 size = 8 + | inversion H3; clear H3; intros; subst; + [ autobatch depth = 7 size = 8 + | clear H3; lapply linear H2 to H; decompose; subst; + autobatch depth = 8 size = 10 + ] + ]. +qed. + +theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to + \forall P2,S2,i2. Insert S2 i2 P2 Q \to + (S1 = S2 \land i1 = i2 \land P1 = P2) \lor + \exists Q1,Q2,j1,j2. + Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2. + intros; lapply insert_conf_rev to H, H1; decompose; subst; + [ lapply linear insert_inj to H, H1; subst; autobatch depth = 4 + | autobatch depth = 7 size = 8 + ]. +qed. diff --git a/helm/software/matita/contribs/LOGIC/Track/defs.ma b/helm/software/matita/contribs/LOGIC/Track/defs.ma new file mode 100644 index 000000000..ef83e6706 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Track/defs.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/defs". + +(* PROOF TREE TRACKS +*) + +include "datatypes/Proof.ma". +include "Insert/defs.ma". + +inductive Track: Context \to Proof \to Sequent \to Prop \def + | track_proj: \forall P,Q,S,i. Insert S i P Q \to Track Q (lref i) S + | track_posr: \forall P,h. + Track P (parx h) (pair (posr h) (posr h)) + | track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to + Track P (impw r) (pair (impl a b) D) + | track_impi: \forall P,r. \forall a,b:Formula. + Track P r (pair a b) \to + Track P (impi r) (pair lleaf (impl a b)) + | track_impe: \forall P,Q,r,D,i. \forall a,b:Formula. + Track Q r (pair lleaf D) \to + Insert (pair a b) i P Q \to + Track P (impe r) (pair (impl a b) D) +(* + | track_impe: \forall P,p,q,r,A,B,D,a,b. + Track P p (pair A (rinj a)) \to + Track P q (pair (linj b) B) \to + Track (abst P (pair A B)) r (pair lleaf D) \to + Track P (impe p q r) (pair (linj (impl a b)) D) +*) +. diff --git a/helm/software/matita/contribs/LOGIC/Track/inv.ma b/helm/software/matita/contribs/LOGIC/Track/inv.ma new file mode 100644 index 000000000..db945de13 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Track/inv.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/inv". + +include "Track/defs.ma". + +theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to + \exists P. Insert S i P Q. + intros. inversion H; clear H; intros; subst. autobatch. +qed. + +theorem track_inv_parx: \forall P,S,h. Track P (parx h) S \to + S = pair (posr h) (posr h). + intros. inversion H; clear H; intros; subst. autobatch. +qed. + +theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to + \exists B,a,b. + S = pair (impl a b) B \land + Track P p (pair lleaf B). + intros. inversion H; clear H; intros; subst. autobatch depth = 5. +qed. + +theorem track_inv_impi: \forall P,p,S. Track P (impi p) S \to + \exists a,b:Formula. + S = pair lleaf (impl a b) \land + Track P p (pair a b). + intros. inversion H; clear H; intros; subst. autobatch depth = 4. +qed. + +theorem track_inv_impe: \forall P,r,S. Track P (impe r) S \to + \exists Q,D,i. \exists a,b:Formula. + S = pair (impl a b) D \land + Track Q r (pair lleaf D) \land + Insert (pair a b) i P Q. + intros. inversion H; clear H; intros; subst. autobatch depth = 8 size = 10. +qed. + +theorem track_inv_lleaf_impl: + \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to + (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor + (\exists r. p = impi r \land Track Q r (pair a b)). + intros. inversion H; clear H; intros; subst; + [ autobatch depth = 5 + | subst. autobatch depth = 4 + ]. +qed. +(* +theorem track_inv_impe: \forall P,p,q,r,S. Track P (impe p q r) S \to + \exists A,B,D. \exists a,b:Formula. + S = pair (impl a b) D \land + Track P p (pair A a) \land + Track P q (pair b B) \land + Track (abst P (pair A B)) r (pair lleaf D). + intros. inversion H; clear H; intros; subst; + [ destruct H2 + | destruct H1 + | destruct H3 + | destruct H3 + | destruct H7. clear H7. subst. autobatch depth = 9 + ]. +qed. +*) diff --git a/helm/software/matita/contribs/LOGIC/Track/order.ma b/helm/software/matita/contribs/LOGIC/Track/order.ma new file mode 100644 index 000000000..ee813d62c --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Track/order.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/order". + +include "Track/props.ma". + +(* Order properties *********************************************************) + +theorem track_refl: \forall P. \forall c:Formula. \exists r. + Track P r (pair c c). + intros. elim c; clear c; + [ autobatch + | lapply (insert_total (pair f f1) zero P); [2:autobatch]; + decompose. autobatch depth = 5 + ]. +qed. + +theorem track_trans: \forall p,q,A,B. \forall c:Formula. + Track leaf p (pair A c) \to Track leaf q (pair c B) \to + \exists r. Track leaf r (pair A B). + intros 1; elim p names 0; clear p; + [ intros. clear H1. + lapply linear track_inv_lref to H. decompose. + lapply insert_inv_leaf_2 to H. decompose + | intros. + lapply linear track_inv_parx to H. subst. autobatch. + | intros. + lapply linear track_inv_impw to H1. + decompose. subst. + lapply linear H to H4, H2. decompose. autobatch + | intros 3. elim q; clear q; + [ clear H H1. + lapply linear track_inv_lref to H2. decompose. + lapply insert_inv_leaf_2 to H. decompose + | lapply linear track_inv_parx to H2. subst. autobatch + | clear H H1. + lapply linear track_inv_impi to H2. + lapply linear track_inv_impw to H3. + decompose. subst. autobatch + | clear H H1 H2. + lapply linear track_inv_impi to H3. + decompose. subst + | clear H H1. + lapply linear track_inv_impi to H2. + lapply linear track_inv_impe to H3. + decompose. subst. autobatch + ] + | intros 3. elim q; clear q; + [ clear H H1. + lapply linear track_inv_lref to H2. decompose. + lapply insert_inv_leaf_2 to H. decompose + | clear H. + lapply linear track_inv_parx to H2. + subst. autobatch + | clear H H1. + lapply linear track_inv_impe to H2. + lapply linear track_inv_impw to H3. + decompose. subst. autobatch + | clear H H1 H2. + lapply linear track_inv_impi to H3. decompose. subst + | clear H H1. + lapply linear track_inv_impe to H2. + lapply linear track_inv_impe to H3. + decompose. subst. + lapply linear track_inv_lleaf_impl to H5. decompose; subst; + [ clear H4 H6. + lapply linear insert_inv_leaf_1 to H3. decompose. subst. + lapply linear insert_inv_abst_2 to H2. decompose. subst + | lapply insert_conf to H3, H4. clear H4. decompose. + lapply linear track_weak to H6, H4. decompose. + lapply linear track_comp to H2, H, H1. decompose. autobatch + ] + ] + ]. +qed. +(* + | lapply linear track_inv_impi to H4. + lapply linear track_inv_impe to H5. + decompose. subst. + destruct H4. destruct H5. clear H4 H5. subst. + unfold linj in Hcut. unfold rinj in Hcut3. destruct Hcut. destruct Hcut3. clear Hcut Hcut3. subst. + destruct Hcut2. clear Hcut2. subst. +*) diff --git a/helm/software/matita/contribs/LOGIC/Track/props.ma b/helm/software/matita/contribs/LOGIC/Track/props.ma new file mode 100644 index 000000000..a7d79f571 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/Track/props.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/props". + +include "Insert/props.ma". +include "Track/inv.ma". + +theorem track_weak: \forall R,p,P,Q,S,i. + Track P p S \to Insert R i P Q \to + \exists q. Track Q q S. + intros 2. elim p; clear p; + [ lapply linear track_inv_lref to H as H0; decompose; + lapply linear insert_trans to H, H1; decompose; autobatch + | lapply linear track_inv_parx to H. subst. autobatch + | lapply linear track_inv_impw to H1. decompose. subst. + lapply linear H to H4, H2. decompose. autobatch + | lapply linear track_inv_impi to H1. decompose. subst. + lapply linear H to H4, H2. decompose. autobatch + | lapply linear track_inv_impe to H1. decompose. subst. + lapply linear insert_conf to H2, H4. decompose. + lapply linear H to H5, H3. decompose. autobatch + ] +qed. + +theorem track_comp: \forall R,q,p,P,Q,S,i. + Track P p R \to Track Q q S \to Insert R i P Q \to + \exists r. Track P r S. + intros 2. elim q; clear q; + [ lapply linear track_inv_lref to H1 as H0; decompose; + lapply linear insert_conf_rev_full to H1,H2; decompose; subst; autobatch + | lapply linear track_inv_parx to H1. subst. autobatch + | lapply linear track_inv_impw to H2. decompose. subst. + lapply linear H to H1, H5, H3. decompose. autobatch + | lapply linear track_inv_impi to H2. decompose. subst. + lapply linear H to H1, H5, H3. decompose. autobatch + | lapply linear track_inv_impe to H2. decompose. subst. + lapply linear insert_trans to H3, H5. decompose. + lapply track_weak to H1, H3. clear H1. decompose. + lapply linear H to H1, H6, H4. decompose. autobatch + ]. +qed. diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma b/helm/software/matita/contribs/LOGIC/datatypes/Context.ma new file mode 100644 index 000000000..0de237801 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/datatypes/Context.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/datatypes/Context". + +(* FLAT CONTEXTS + - Naming policy: + - contexts: P Q +*) + +include "datatypes/Sequent.ma". + +inductive Context: Type \def + | leaf: Context + | abst: Context \to Sequent \to Context +. + +definition inj: Sequent \to Context \def abst leaf. + +coercion cic:/matita/LOGIC/datatypes/Context/inj.con. diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma b/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma new file mode 100644 index 000000000..64025957e --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/datatypes/Formula". + +(* FORMULAE + - Naming policy: + - formulae: a b c d +*) + +include "preamble.ma". + +inductive Formula: Type \def + | posr: Nat \to Formula + | impl: Formula \to Formula \to Formula +. diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma new file mode 100644 index 000000000..8643eb826 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/datatypes/Proof". + +(* PROOFS + - Naming policy: + - proofs: p q r s +*) + +include "preamble.ma". + +inductive Proof: Type \def + | lref: Nat \to Proof + | parx: Nat \to Proof + | impw: Proof \to Proof + | impi: Proof \to Proof + | impe: Proof \to Proof +(* + | impe: Proof \to Proof \to Proof \to Proof +*) +. diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma new file mode 100644 index 000000000..d78ac503a --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/datatypes/Sequent". + +(* SEQUENTS + - Naming policy: + - left hand sides (lhs): A C + - right hand sides (rhs): B D + - sequents : R S +*) + +include "datatypes/Formula.ma". + +inductive LHS: Type \def + | lleaf: LHS + | labst: LHS \to Formula \to LHS +. + +inductive RHS: Type \def + | rleaf: RHS + | rabst: Formula \to RHS \to RHS +. + +inductive Sequent: Type \def + | pair: LHS \to RHS \to Sequent +. + +definition linj: Formula \to LHS \def labst lleaf. + +definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf. + +coercion cic:/matita/LOGIC/datatypes/Sequent/linj.con. + +coercion cic:/matita/LOGIC/datatypes/Sequent/rinj.con. diff --git a/helm/software/matita/contribs/LOGIC/makefile b/helm/software/matita/contribs/LOGIC/makefile new file mode 100644 index 000000000..e5ac91fc8 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/makefile @@ -0,0 +1,39 @@ +H=@ + +RT_BASEDIR=../../ +OPTIONS=-bench +MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) +CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) +MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) +CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) + +devel:=$(shell basename `pwd`) + +ifneq "$(SRC)" "" + XXX="SRC=$(SRC)" +endif + +all: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) +clean: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) +cleanall: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all + +all.opt opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) +clean.opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) +cleanall.opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all + +%.mo: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ +%.mo.opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) + +preall: + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) + +preall.opt: + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) diff --git a/helm/software/matita/contribs/LOGIC/preamble.ma b/helm/software/matita/contribs/LOGIC/preamble.ma new file mode 100644 index 000000000..a2d3b8304 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/preamble.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* Project started Sat Apr 7, 2007 ****************************************) + +set "baseuri" "cic:/matita/LOGIC/preamble". + +(* PREAMBLE +*) + +include "../LAMBDA-TYPES/Unified-Sub/preamble.ma". diff --git a/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile index 4fb6a0f11..9c104f361 100644 --- a/helm/software/matita/contribs/Makefile +++ b/helm/software/matita/contribs/Makefile @@ -1,6 +1,6 @@ GOALS = all opt clean clean.opt -DEVELS = ../library ../legacy RELATIONAL LAMBDA-TYPES +DEVELS = ../library ../legacy RELATIONAL LOGIC LAMBDA-TYPES $(GOALS): @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) diff --git a/helm/software/matita/contribs/developments.txt b/helm/software/matita/contribs/developments.txt index ff8bf2c36..f7e03520b 100644 --- a/helm/software/matita/contribs/developments.txt +++ b/helm/software/matita/contribs/developments.txt @@ -7,6 +7,7 @@ software/matita/tests software/matita/dama software/matita/contribs/PREDICATIVE-TOPOLOGY software/matita/contribs/RELATIONAL +software/matita/contribs/LOGIC software/matita/contribs/LAMBDA-TYPES/Unified-Sub software/matita/contribs/LAMBDA-TYPES/Base-1 software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1 diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma index fc8f9d854..a0cab9867 100644 --- a/helm/software/matita/contribs/prova.ma +++ b/helm/software/matita/contribs/prova.ma @@ -14,6 +14,22 @@ set "baseuri" "cic:/matita/test/prova". +include "../legacy/coq.ma". + +theorem pippo: \forall (A,B:Prop). A \land B \to A. + intros; decompose; assumption. +qed. + +inline procedural "cic:/matita/test/prova/pippo.con". + +alias id "plus" = "cic:/Coq/Init/Peano/plus.con". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". +theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n). + intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". +apply plus_comm. +qed. +(* include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma". alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)". alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con". @@ -195,4 +211,26 @@ apply H6(* assumption *) |apply H(* assumption *) ]. qed. +*) +(* +include "nat/orders.ma". +theorem le_inv: + \forall P:nat \to Prop + .\forall p2 + .\forall p1 + .p2 <= p1 \to + (p1 = p2 \to P p2) \to + (\forall n1 + .p2 <= n1 \to + (p1 = n1 \to P n1) \to + p1 = S n1 \to P (S n1)) \to + P p1. + intros 4; elim H names 0; clear H p1; intros; + [ apply H; reflexivity + | apply H3; clear H3; intros; + [ apply H | apply H1; clear H1; intros; subst; + [ apply H2; apply H3 | ] + | reflexivity + ] +*) -- 2.39.2