From 143c97a8fe657eb7b041dec2747b0e67b5899762 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 5 Jun 2013 21:54:08 +0000
Subject: [PATCH] some work on extended reduction ...

---
 .../contribs/lambdadelta/basic_2/names.txt    |  6 +-
 .../contribs/lambdadelta/basic_2/notation.ma  | 12 ++++
 .../basic_2/reduction/{xpr.ma => cpx.ma}      | 37 ++++-------
 .../basic_2/reduction/cpx_ldrop.ma            | 64 +++++++++++++++++++
 .../lambdadelta/basic_2/relocation/fsupq.ma   | 32 ++++++++++
 matita/matita/lib/basics/relations.ma         |  6 ++
 matita/matita/lib/basics/star.ma              |  2 +-
 matita/matita/predefined_virtuals.ml          |  1 +
 8 files changed, 132 insertions(+), 28 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/reduction/{xpr.ma => cpx.ma} (60%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 1e1fc78cc..003b33747 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -51,9 +51,10 @@ NAMING CONVENTIONS FOR TRANSFORMATIONS
 
 - first letter
 
+c: contex-sensitive for terms
 f: context-freee for closures
-l: sn contex-sensitive for terms
-r: dx contex-sensitive for terms
+l: sn contex-sensitive for local environments
+r: dx contex-sensitive for local environments
 t: context-free for terms
 
 -second letter
@@ -73,4 +74,5 @@ x: extended reduction
 - forth letter (if present)
 
 p: non-reflexive transitive closure
+q: reflexive closure
 s: reflexive transitive closure
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index d53b103c8..b956f9049 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -150,6 +150,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ break ⦃ term 46 L2 ,
    non associative with precedence 45
    for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
 
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⸮ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'SupTermOpt $L1 $T1 $L2 $T2 }.
+
 notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
    non associative with precedence 45
    for @{ 'ICM $L $T $k }.
@@ -254,6 +258,14 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'PRedSn $L1 $L2 }.
 
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRed $h $g $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ ➡ break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedAlt $h $g $L $T1 $T2 }.
+
 (* Computation **************************************************************)
 
 notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
similarity index 60%
rename from matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 8cec0b050..0c6d10fa1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -15,41 +15,33 @@
 include "basic_2/static/ssta.ma".
 include "basic_2/reduction/cpr.ma".
 
-lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
-#x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
-qed-.
-
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
 
-notation "hvbox( ⦃term 46 h, break term 46 L⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'XPRed $h $g $L $T1 $T2 }.
-
-inductive xpr (h) (g): lenv → relation term ≝
-| xpr_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → xpr h g L (⓪{I}) U2
-| xpr_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → xpr h g L (⓪{I}) U2
-| xpr_bind: ∀a,I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g (L.ⓑ{I}V1) T1 T2 →
-            L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → xpr h g L (ⓑ{a,I}V1.T1) U2
-| xpr_flat: ∀I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g L T1 T2 →
-            L ⊢ ⓕ{I}V2.T2 ➡ U2 → xpr h g L (ⓕ{I}V1.T1) U2
+inductive cpx (h) (g): lenv → relation term ≝
+| cpx_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → cpx h g L (⓪{I}) U2
+| cpx_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → cpx h g L (⓪{I}) U2
+| cpx_bind: ∀a,I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g (L.ⓑ{I}V1) T1 T2 →
+            L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → cpx h g L (ⓑ{a,I}V1.T1) U2
+| cpx_flat: ∀I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g L T1 T2 →
+            L ⊢ ⓕ{I}V2.T2 ➡ U2 → cpx h g L (ⓕ{I}V1.T1) U2
 .
 
 interpretation
    "context-sensitive extended parallel reduction (term)"
-   'XPRed h g L T1 T2 = (xpr h g L T1 T2).
+   'PRed h g L T1 T2 = (cpx h g L T1 T2).
 
 (* Basic properties *********************************************************)
 
-(* Note: this is "∀h,g,L. reflexive … (xpr h g L)" *)
-lemma xpr_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
+(* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *)
+lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
 #h #g #T elim T -T /2 width=1/ * /2 width=5/
 qed.
 
-lemma cpr_xpr: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+lemma cpr_cpx: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
 #h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
 qed.
 
-lemma ssta_xpr: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+lemma ssta_cpx: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
 #h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
 [ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
   elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
@@ -59,8 +51,3 @@ lemma ssta_xpr: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃
   lapply (ssta_inv_cast1 … H) -H /3 width=5/
 ]
 qed.
-
-include "basic_2/relocation/lift_lift.ma".
-include "basic_2/relocation/fsup.ma".
-include "basic_2/substitution/lpss_ldrop.ma".
-
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
new file mode 100644
index 000000000..20445e154
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+include "basic_2/substitution/lpss_ldrop.ma".
+include "basic_2/substitution/fsups.ma".
+
+lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
+                       ∃∃U1. L1 ⊢ T1 ▶* U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ]
+[ * #L1
+  [ #V2 #U2 #HVU2
+    elim (lift_total U2 0 1) #W2 #HUW2
+    @(ex2_intro … W2) /2 width=7/
+    @(fsup_ldrop … L1 … HUW2) /2 width=1/
+  | #W #U2 #H  
+    @(ex2_intro … (#0)) /2 width=7/
+  
+| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+  elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
+  elim (lift_total T d e) #U #HTU
+  lapply (cpss_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+]
+qed-.
+
+
+
+(*
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/substitution/fsups.ma".
+*)
+(*
+lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                       ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+                       ∃∃L,U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
+
+*)
+lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                       ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+                       ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
+#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
+[ * #L1 #V1 #U2 #l #H
+  elim (lift_total U2 0 1) #W2 #HUW2
+(*
+  [ @(ex2_intro … W2) [ @(cpx_ssta … l) @(ssta_ldef … H) //
+                      | @(fsups_ldrop … L1 … HUW2) /2 width=1/ 
+*)
+|
+| #a #I #L1 #V1 #T1 #U2 #l #HT1
+  @(ex2_intro … (ⓑ{a,I}V1.U2)) /2 width=1/  
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
new file mode 100644
index 000000000..9400a84d7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basic_2/relocation/fsup.ma".
+
+(* OPTIONAL SUPCLOSURE ******************************************************)
+
+definition fsupq: bi_relation lenv term ≝ bi_RC … fsup.
+
+interpretation
+   "optional structural successor (closure)"
+   'SupTermOpt L1 T1 L2 T2 = (fsup L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fsupq_refl: bi_reflexive … fsupq.
+/2 width=1/ qed.
+
+lemma fsup_fsupq: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄.
+/2 width=1/ qed.
+
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 84dd7c362..d40856195 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -191,3 +191,9 @@ definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
 definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
                           ∀a1,a,b1,b. R a1 b1 a b →
                           ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
+
+definition bi_RC: ∀A,B:Type[0]. bi_relation A B → bi_relation A B ≝
+                  λA,B,R,x1,y1,x2,y2. R … x1 y1 x2 y2 ∨ (x1 = x2 ∧ y1 = y2).
+
+lemma bi_RC_reflexive: ∀A,B,R. bi_reflexive A B (bi_RC … R).
+/3 width=1/ qed.
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 36aee8fe4..f935f0070 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -142,7 +142,7 @@ lemma star_ind_l: ∀A,R,a2. ∀P:predicate A.
 @(star_ind_l_aux … H1 H2 … Ha12) //
 qed.
 
-(* RC and star *)
+(* TC and star *)
 
 lemma TC_to_star: ∀A,R,a,b.TC A R a b → star A R a b.
 #R #A #a #b #TCH (elim TCH) /2/
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index d8da251bb..6cf8ab99f 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1504,6 +1504,7 @@ let load_predefined_virtuals () =
 
 let predefined_classes = [
  ["!"; "¡"; ]; 
+ ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
  ["#"; "♯"; "⌘"; ];
-- 
2.39.5