Unified: INC and BEq removed

contribs: added dependence to ../legacy in the Makefile

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
deleted file mode 100644 (file)
index d36f86a..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
+++ /dev/null
@@ -1,26 +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/LAMBDA-TYPES/Unified-Sub/Inc/defs".
-
-(* DISPLACEMENT INCREMENT RELATION
-*)
-
-include "Term/defs.ma".
-
-inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
-   | inc_bind: \forall r. Inc i true (bind r) (succ i)
-   | inc_skip: \forall r. Inc i false (bind r) i
-   | inc_flat: \forall r,q. Inc i q (flat r) i   
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
index cf29a3562e573ceda4071a0acdaaa88bc62ee32c..af573d3604f64e685edf1de289d02f756ebcb639 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -18,21 +18,29 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "Inc/defs.ma".
+include "Term/defs.ma".
 
 inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
    | lift_sort   : \forall l,q,i,h. 
                    Lift q l i (leaf (sort h)) (leaf (sort h))
-   | lift_skip   : \forall l,i,j. 
+   | lift_lref   : \forall l,i,j. 
                    Lift false l i (leaf (lref j)) (leaf (lref j))
    | lift_lref_lt: \forall l,i,j. j < i \to 
                    Lift true l i (leaf (lref j)) (leaf (lref j))
    | lift_lref_ge: \forall l,i,j1. i <= j1 \to
                    \forall j2. (j1 + l == j2) \to
                    Lift true l i (leaf (lref j1)) (leaf (lref j2))
-   | lift_head   : \forall l,qt,qu,q. (qt -- q == qu) \to
-                   \forall z,iu,it. Inc iu qu z it \to
-                   \forall u1,u2. Lift qu l iu u1 u2 \to
-                   \forall t1,t2. Lift qt l it t1 t2 \to 
-                   Lift qt l iu (head q z u1 t1) (head q z u2 t2)
+   | lift_bind   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
+                   \forall q,t1,t2. Lift q l (succ i) t1 t2 \to 
+                   \forall r.
+                   Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2)
+   | lift_flat   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
+                   \forall q,t1,t2. Lift q l i t1 t2 \to 
+                   \forall r.
+                   Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2)
+   | lift_head   : \forall l,qt,q. (qt = q \to False) \to
+                   \forall i,u1,u2. Lift false l i u1 u2 \to
+                   \forall t1,t2. Lift qt l i t1 t2 \to 
+                   \forall z.
+                   Lift qt l i (head q z u1 t1) (head q z u2 t2)
 .

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
index 21afc1d99dc13929ca06221d5f1594a677c92b00..45f2fb18226f148b1ad92e99730bc22e6971dcc1 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
@@ -22,6 +22,5 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble".
 include "logic/equality.ma".
 include "../../RELATIONAL/NPlus/defs.ma".
 include "../../RELATIONAL/NLE/defs.ma".
-include "../../RELATIONAL/BEq/defs.ma".
 include "../../RELATIONAL/Nat/defs.ma".
 include "../../RELATIONAL/Bool/defs.ma".

diff --git a/matita/contribs/Makefile b/matita/contribs/Makefile
index 8dc8c4626884762b840bfdfd9ce03b8660d82e0e..4fb6a0f11c3af7615bce544ea05ef0d03c917e17 100644 (file)
--- a/matita/contribs/Makefile
+++ b/matita/contribs/Makefile
@@ -1,6 +1,6 @@
 GOALS = all opt clean clean.opt
 
-DEVELS = ../library RELATIONAL LAMBDA-TYPES
+DEVELS = ../library ../legacy RELATIONAL LAMBDA-TYPES
 
 $(GOALS): 
        @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) 

diff --git a/matita/contribs/RELATIONAL/BEq/defs.ma b/matita/contribs/RELATIONAL/BEq/defs.ma
deleted file mode 100644 (file)
index 3ab3b00..0000000
--- a/matita/contribs/RELATIONAL/BEq/defs.ma
+++ /dev/null
@@ -1,32 +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/RELATIONAL/BEq/defs".
-
-include "logic/equality.ma".
-
-include "Bool/defs.ma".
-
-inductive BEq (A:Type) (a1:A): A \to Bool \to Prop \def
-   | beq_true : BEq A a1 a1 true
-   | beq_false: \forall a2. (a1 = a2 -> False) \to BEq A a1 a2 false
-.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "boolean equality" 'beq x y z = 
-   (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) _ x y z).
-
-notation "hvbox(a break -- b break == c)" 
-  non associative with precedence 95
-for @{ 'beq $a $b $c}.