]> matita.cs.unibo.it Git - helm.git/commitdiff
New developement LOGIC about the cut elimination of implication for Sambin's basic...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 24 Jul 2007 11:52:05 +0000 (11:52 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 24 Jul 2007 11:52:05 +0000 (11:52 +0000)
18 files changed:
helm/software/matita/contribs/LOGIC/CLE/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Insert/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Insert/fun.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Insert/inv.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Insert/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Track/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Track/inv.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Track/order.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/Track/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/datatypes/Context.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/datatypes/Formula.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/datatypes/Proof.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/makefile [new file with mode: 0644]
helm/software/matita/contribs/LOGIC/preamble.ma [new file with mode: 0644]
helm/software/matita/contribs/Makefile
helm/software/matita/contribs/developments.txt
helm/software/matita/contribs/prova.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 (file)
index 0000000..7a2c760
--- /dev/null
@@ -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 (file)
index 0000000..7b72c5c
--- /dev/null
@@ -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 (file)
index 0000000..5661c0a
--- /dev/null
@@ -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 (file)
index 0000000..229b9cc
--- /dev/null
@@ -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 (file)
index 0000000..1e0bc54
--- /dev/null
@@ -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 (file)
index 0000000..ef83e67
--- /dev/null
@@ -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 (file)
index 0000000..db945de
--- /dev/null
@@ -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 (file)
index 0000000..ee813d6
--- /dev/null
@@ -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 (file)
index 0000000..a7d79f5
--- /dev/null
@@ -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 (file)
index 0000000..0de2378
--- /dev/null
@@ -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 (file)
index 0000000..6402595
--- /dev/null
@@ -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 (file)
index 0000000..8643eb8
--- /dev/null
@@ -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 (file)
index 0000000..d78ac50
--- /dev/null
@@ -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 (file)
index 0000000..e5ac91f
--- /dev/null
@@ -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 (file)
index 0000000..a2d3b83
--- /dev/null
@@ -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".
index 4fb6a0f11c3af7615bce544ea05ef0d03c917e17..9c104f361e6c6aac6d6eeac493e31f334f5327ba 100644 (file)
@@ -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) $@;) 
index ff8bf2c365140776e69eb695673a65f2c7171154..f7e03520b498611ea1e049e6a62f5a3657b54356 100644 (file)
@@ -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
index fc8f9d854bbe7e0dd2095641165b5b40057a88a0..a0cab98679b4c713b6857a62b473e7ef8d997c5b 100644 (file)
 
 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
+ ]
+*)