refactoring

diff --git a/helm/software/matita/contribs/LOGIC/Track/pred.ma b/helm/software/matita/contribs/LOGIC/Track/pred.ma
index c4e65c05d3c45c50dffbb7a0f56b4a92c144793e..d190f17fdd1661638514621af5a7fcd5594269dd 100644 (file)
--- a/helm/software/matita/contribs/LOGIC/Track/pred.ma
+++ b/helm/software/matita/contribs/LOGIC/Track/pred.ma
@@ -33,7 +33,10 @@ theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. [Q1, p1, S1] => [Q2, p2, S2] \to
  | lapply linear track_inv_scut to H4; decompose; destruct;
    lapply linear track_inv_lref to H5; decompose; autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;
-   lapply linear track_inv_prin to H5; destruct; autobatch
+   lapply linear track_inv_prin to H5; destruct;
+   lapply linear rinj_inj to Hcut1;
+   rewrite < Hcut1 in H4; clear Hcut1 a2;
+   autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;
    lapply linear track_inv_prin to H4; destruct; autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;

diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma b/helm/software/matita/contribs/LOGIC/datatypes/Context.ma
deleted file mode 100644 (file)
index 44d6266..0000000
--- a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/Proof.ma".
-include "datatypes/Sequent.ma".
-
-inductive Context: Type \def
-   | leaf: Context
-   | abst: Context \to Proof \to Proof \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
deleted file mode 100644 (file)
index 6402595..0000000
--- a/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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
deleted file mode 100644 (file)
index f6260b0..0000000
--- a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
+++ /dev/null
@@ -1,31 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                       (* projection         *)
-   | prin: Nat \to Proof                       (* pos rel inhabitant *)
-   | impw: Proof \to Proof                     (* weakening          *)
-   | impr: Proof \to Proof                     (* right introduction *)
-   | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)
-   | scut: Proof \to Proof \to Proof           (* symmetric cut      *)
-.

diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma
deleted file mode 100644 (file)
index d78ac50..0000000
--- a/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma
+++ /dev/null
@@ -1,46 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/datatypes_defs/Context.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Context.ma
new file mode 100644 (file)
index 0000000..e5dba4a
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Context.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_defs/Context".
+
+(* FLAT CONTEXTS
+   - Naming policy:
+     - contexts: P Q
+*)
+
+include "datatypes_defs/Proof.ma".
+include "datatypes_defs/Sequent.ma".
+
+inductive Context: Type \def
+   | leaf: Context
+   | abst: Context \to Proof \to Proof \to Sequent \to Context
+.
+(*
+definition inj: Sequent \to Context \def abst leaf.
+
+coercion cic:/matita/LOGIC/datatypes_defs/Context/inj.con.
+*)

diff --git a/helm/software/matita/contribs/LOGIC/datatypes_defs/Formula.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Formula.ma
new file mode 100644 (file)
index 0000000..ec6441d
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/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_defs/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_defs/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Proof.ma
new file mode 100644 (file)
index 0000000..fa2c29f
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Proof.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_defs/Proof".
+
+(* PROOFS
+   - Naming policy:
+     - proofs: p q r s
+*)
+
+include "preamble.ma".
+
+inductive Proof: Type \def
+   | lref: Nat \to Proof                       (* projection         *)
+   | prin: Nat \to Proof                       (* pos rel inhabitant *)
+   | impw: Proof \to Proof                     (* weakening          *)
+   | impr: Proof \to Proof                     (* right introduction *)
+   | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)
+   | scut: Proof \to Proof \to Proof           (* symmetric cut      *)
+.

diff --git a/helm/software/matita/contribs/LOGIC/datatypes_defs/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Sequent.ma
new file mode 100644 (file)
index 0000000..09d8269
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/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_defs/Sequent".
+
+(* SEQUENTS
+   - Naming policy:
+     - left hand sides  (lhs): A C
+     - right hand sides (rhs): B D
+     - sequents              : R S
+*)
+
+include "datatypes_defs/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_defs/Sequent/linj.con.
+
+coercion cic:/matita/LOGIC/datatypes_defs/Sequent/rinj.con.

diff --git a/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma
new file mode 100644 (file)
index 0000000..1b0ea6c
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_props/Sequent".
+
+include "datatypes_defs/Sequent.ma".
+
+theorem rinj_inj: \forall b,d. rinj b = rinj d \to b = d.