- we introduced the pointer_step rc in the perspective of proving

results on head normal forms
- some renaming

diff --git a/matita/matita/contribs/lambda/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/labeled_sequential_computation.ma
new file mode 100644 (file)
index 0000000..4c2a6fc
--- /dev/null
+++ b/matita/matita/contribs/lambda/labeled_sequential_computation.ma
@@ -0,0 +1,145 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "pointer_list.ma".
+include "parallel_computation.ma".
+
+(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
+
+definition lsreds: ptrl → relation term ≝ lstar … lsred.
+
+interpretation "labelled sequential computation"
+   'SeqRedStar M s N = (lsreds s M N).
+
+notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
+   non associative with precedence 45
+   for @{ 'SeqRedStar $M $s $N }.
+
+lemma lsreds_refl: reflexive … (lsreds (◊)).
+//
+qed.
+
+lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
+/2 width=3/
+qed-.
+
+lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
+/2 width=3/
+qed-.
+
+lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
+/2 width=1/
+qed.
+
+lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
+/2 width=5 by lstar_inv_nil/
+qed-.
+
+lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
+                       ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
+/2 width=3 by lstar_inv_cons/
+qed-.
+
+lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
+/2 width=1 by lstar_inv_step/
+qed-.
+
+lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
+                      ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma lsred_compatible_rc: ho_compatible_rc lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_lift: ∀s. liftable (lsreds s).
+/2 width=1/
+qed.
+
+lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
+/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
+qed-.
+
+lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
+/2 width=1/
+qed.
+
+theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
+/3 width=7 by lstar_singlevalued, lsred_mono/
+qed-.
+
+theorem lsreds_trans: ltransitive … lsreds.
+/2 width=3 by lstar_ltransitive/
+qed-.
+
+lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+                              @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.A1)) /2 width=1/
+qed.
+
+lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+                              @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
+@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
+qed.
+
+(* Note: "|s|" should be unparetesized *)
+lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lsred_fwd_mult … HM1) -p #HM1
+@(transitive_le … IHM2) -M2
+/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
+qed-.
+
+theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2
+@(preds_step_sn … IHM2) -M2 /2 width=2/
+qed.
+
+lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M1 -M2 /2 width=2/
+[ #A1 #A2 #_ * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+qed-.
+
+theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M2 /2 width=2/
+#M #M2 #_ #HM2 * #r #HM1
+elim (pred_lsreds … HM2) -HM2 #s #HM2
+lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
+qed-.
+
+theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
+                     ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
+#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
+lapply (lsreds_preds … HM01) -s1 #HM01
+lapply (lsreds_preds … HM02) -s2 #HM02
+elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
+elim (preds_lsreds … HM1) -HM1
+elim (preds_lsreds … HM2) -HM2 /2 width=5/
+qed-.

diff --git a/matita/matita/contribs/lambda/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma
new file mode 100644 (file)
index 0000000..7dd2bcc
--- /dev/null
+++ b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma
@@ -0,0 +1,143 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "pointer.ma".
+include "multiplicity.ma".
+
+(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************)
+
+(* Note: the application "(A B)" is represented by "@B.A" following:
+         F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
+         Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
+*)
+inductive lsred: ptr → relation term ≝
+| lsred_beta   : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A)
+| lsred_abst   : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::p) (𝛌.A1) (𝛌.A2) 
+| lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A)
+| lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2)
+.
+
+interpretation "labelled sequential reduction"
+   'SeqRed M p N = (lsred p M N).
+
+(* Note: we do not use → since it is reserved by CIC *)
+notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
+   non associative with precedence 45
+   for @{ 'SeqRed $M $p $N }.
+
+lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥.
+#p #M #N * -p -M -N
+[ #B #A #i #H destruct
+| #p #A1 #A2 #_ #i #H destruct
+| #p #B1 #B2 #A #_ #i #H destruct
+| #p #B #A1 #A2 #_ #i #H destruct
+]
+qed-.
+
+lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p →
+                     ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N.
+#p #M #N * -p -M -N
+[ #B #A #_ destruct /2 width=4/
+| #p #A1 #A2 #_ #H destruct
+| #p #B1 #B2 #A #_ #H destruct
+| #p #B #A1 #A2 #_ #H destruct
+]
+qed-.
+
+lemma lsred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p →
+                    ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p →
+                    ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #_ #q #H destruct
+| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p →
+                    ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #_ #q #H destruct
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
+]
+qed-.
+
+lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}.
+#p #M #N #H elim H -p -M -N
+[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) //
+  normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) 
+| //
+| #p #B #D #A #_ #IHBD
+  @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p
+| #p #B #A #C #_ #IHAC
+  @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p
+]
+@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ]
+>distributive_times_plus normalize /2 width=1/
+qed-.
+
+lemma lsred_lift: ∀p. liftable (lsred p).
+#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma lsred_inv_lift: ∀p. deliftable_sn (lsred p).
+#p #h #N1 #N2 #H elim H -p -N1 -N2
+[ #D #C #d #M1 #H
+  elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
+  elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
+| #p #C1 #C2 #_ #IHC12 #d #M1 #H
+  elim (lift_inv_abst … H) -H #A1 #HAC1 #H
+  elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+  @(ex2_intro … (𝛌.A2)) // /2 width=1/
+| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
+  elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
+  elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
+  @(ex2_intro … (@B2.A)) // /2 width=1/
+| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+  elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
+  elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+  @(ex2_intro … (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
+#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+qed.
+
+theorem lsred_mono: ∀p. singlevalued … (lsred p).
+#p #M #N1 #H elim H -p -M -N1
+[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H //
+  #D #C #H #HN2 destruct //
+| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+]
+qed-.

diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
deleted file mode 100644 (file)
index f628648..0000000
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ /dev/null
@@ -1,145 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "pointer_list.ma".
-include "parallel_computation.ma".
-
-(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
-
-definition lsreds: ptrl → relation term ≝ lstar … lsred.
-
-interpretation "labelled sequential computation"
-   'SeqRedStar M s N = (lsreds s M N).
-
-notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
-   non associative with precedence 45
-   for @{ 'SeqRedStar $M $s $N }.
-
-lemma lsreds_refl: reflexive … (lsreds (◊)).
-//
-qed.
-
-lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
-/2 width=1/
-qed.
-
-lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
-/2 width=5 by lstar_inv_nil/
-qed-.
-
-lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
-                       ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
-/2 width=3 by lstar_inv_cons/
-qed-.
-
-lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
-/2 width=1 by lstar_inv_step/
-qed-.
-
-lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
-                      ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
-/2 width=1 by lstar_inv_pos/
-qed-.
-
-lemma lsred_compatible_rc: ho_compatible_rc lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_lift: ∀s. liftable (lsreds s).
-/2 width=1/
-qed.
-
-lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
-/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
-qed-.
-
-lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
-/2 width=1/
-qed.
-
-theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
-/3 width=7 by lstar_singlevalued, lsred_mono/
-qed-.
-
-theorem lsreds_trans: ltransitive … lsreds.
-/2 width=3 by lstar_ltransitive/
-qed-.
-
-lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
-                              @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans … (@B2.A1)) /2 width=1/
-qed.
-
-lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
-                              @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::sn:::s)@◊::◊] [↙B2] A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
-@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
-qed.
-
-(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
-#p #s #M1 #M #HM1 #_ #IHM2
-lapply (lsred_fwd_mult … HM1) -p #HM1
-@(transitive_le … IHM2) -M2
-/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
-qed-.
-
-theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
-#a #s #M1 #M #HM1 #_ #IHM2
-@(preds_step_sn … IHM2) -M2 /2 width=2/
-qed.
-
-lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
-#M1 #M2 #H elim H -M1 -M2 /2 width=2/
-[ #A1 #A2 #_ * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-qed-.
-
-theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
-#M1 #M2 #H elim H -M2 /2 width=2/
-#M #M2 #_ #HM2 * #r #HM1
-elim (pred_lsreds … HM2) -HM2 #s #HM2
-lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
-qed-.
-
-theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
-                     ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
-#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
-lapply (lsreds_preds … HM01) -s1 #HM01
-lapply (lsreds_preds … HM02) -s2 #HM02
-elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
-elim (preds_lsreds … HM1) -HM1
-elim (preds_lsreds … HM2) -HM2 /2 width=5/
-qed-.

diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
deleted file mode 100644 (file)
index 40d5188..0000000
--- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
+++ /dev/null
@@ -1,136 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "pointer.ma".
-include "multiplicity.ma".
-
-(* LABELLED SEQUENTIAL REDUCTION (SINGLE STEP) ******************************)
-
-(* Note: the application "(A B)" is represented by "@B.A" following:
-         F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
-         Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
-*)
-inductive lsred: ptr → relation term ≝
-| lsred_beta   : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A)
-| lsred_abst   : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::p) (𝛌.A1) (𝛌.A2) 
-| lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A)
-| lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2)
-.
-
-interpretation "labelled sequential reduction"
-   'SeqRed M p N = (lsred p M N).
-
-(* Note: we do not use → since it is reserved by CIC *)
-notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
-   non associative with precedence 45
-   for @{ 'SeqRed $M $p $N }.
-
-lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥.
-#p #M #N * -p -M -N
-[ #B #A #i #H destruct
-| #p #A1 #A2 #_ #i #H destruct
-| #p #B1 #B2 #A #_ #i #H destruct
-| #p #B #A1 #A2 #_ #i #H destruct
-]
-qed-.
-
-lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p →
-                     ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N.
-#p #M #N * -p -M -N
-[ #B #A #_ destruct /2 width=4/
-| #p #A1 #A2 #_ #H destruct
-| #p #B1 #B2 #A #_ #H destruct
-| #p #B #A1 #A2 #_ #H destruct
-]
-qed-.
-
-lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p →
-                    (∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨
-                    ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #HA12 #q #H destruct /3 width=5/
-| #p #B1 #B2 #A #HB12 #q #H destruct /3 width=6/
-| #p #B #A1 #A2 #_ #q #H destruct
-]
-qed-.
-
-lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p →
-                    ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #_ #q #H destruct
-| #p #B1 #B2 #A #_ #q #H destruct
-| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
-]
-qed-.
-
-lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}.
-#p #M #N #H elim H -p -M -N
-[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) //
-  normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) 
-| //
-| #p #B #D #A #_ #IHBD
-  @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p
-| #p #B #A #C #_ #IHAC
-  @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p
-]
-@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ]
->distributive_times_plus normalize /2 width=1/
-qed-.
-
-lemma lsred_lift: ∀p. liftable (lsred p).
-#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#B #A #d <dsubst_lift_le //
-qed.
-
-lemma lsred_inv_lift: ∀p. deliftable_sn (lsred p).
-#p #h #N1 #N2 #H elim H -p -N1 -N2
-[ #D #C #d #M1 #H
-  elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
-  elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
-| #p #C1 #C2 #_ #IHC12 #d #M1 #H
-  elim (lift_inv_abst … H) -H #A1 #HAC1 #H
-  elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
-  @(ex2_intro … (𝛌.A2)) // /2 width=1/
-| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
-  elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
-  elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
-  @(ex2_intro … (@B2.A)) // /2 width=1/
-| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
-  elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
-  elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
-  @(ex2_intro … (@B.A2)) // /2 width=1/
-]
-qed-.
-
-lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
-#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#D2 #A #d >dsubst_dsubst_ge //
-qed.
-
-theorem lsred_mono: ∀p. singlevalued … (lsred p).
-#p #M #N1 #H elim H -p -M -N1
-[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // #D #C #H #HN2 destruct //
-| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
-  [ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-  | #D1 #D2 #C #_ #H destruct
-  ]
-| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
-  [ #C1 #C2 #_ #H destruct
-  | #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
-  ]
-| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
-]
-qed-.

diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma
index eaa8b7ce14c7be524c1dac5099dc18c1905aca5b..1d97b3b87a4fbe5566e8ebb252619b5817d07f58 100644 (file)
--- a/matita/matita/contribs/lambda/parallel_reduction.ma
+++ b/matita/matita/contribs/lambda/parallel_reduction.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "length.ma".
-include "labelled_sequential_reduction.ma".
+include "labeled_sequential_reduction.ma".
 
 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
 

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 27f30b22c199a2d47544019c18b6e482174e09e0..d71574e744123ba51a836db8443f36dbf7e09627 100644 (file)
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -18,17 +18,12 @@ include "term.ma".
 
 (* Policy: pointer step metavariables: c *)
 (* Note: this is a step of a path in the tree representation of a term:
-         rc (rectus)  : not needed (we use sn instead)
+         rc (rectus)  : proceed on the argument of an abstraction
          sn (sinister): proceed on the left argument of an application
-                        or on the argument of an abstraction (this would be rc)
          dx (dexter)  : proceed on the right argument of an application
 *)
-(* Remark: the following breaks destruct because of δ-expansions
-           definition ptr_step: Type[0] ≝ bool.
-           definition sn: bool ≝ true.
-           definition dx: bool ≝ false.
-*)
 inductive ptr_step: Type[0] ≝
+| rc: ptr_step
 | sn: ptr_step
 | dx: ptr_step
 .
@@ -50,7 +45,7 @@ lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
 qed-.
 
 definition compatible_rc: predicate (ptr→relation term) ≝ λR.
-                          ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2).
+                          ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
 
 definition compatible_sn: predicate (ptr→relation term) ≝ λR.
                           ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).

diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma
index 82f704a78e681ac59dd98157019326709be40e1c..becfc0a5ee436a673c33e009c0d7070eb73ff312 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_list.ma
+++ b/matita/matita/contribs/lambda/pointer_list.ma
@@ -33,7 +33,7 @@ lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
 qed.
 
 definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR.
-                             ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2).
+                             ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
 
 definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR.
                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).

diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma
index 92618412e635092d8043edaef6227a64d2660a10..0b738215a59b3d6764293418065d2595986dd445 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_order.ma
+++ b/matita/matita/contribs/lambda/pointer_order.ma
@@ -20,7 +20,8 @@ include "pointer.ma".
          to serve as base for the order relations: p < q and p ≤ q *)
 inductive pprec: relation ptr ≝
 | pprec_nil : ∀c,q.   pprec (◊) (c::q)
-| ppprc_cons: ∀p,q.   pprec (dx::p) (sn::q)
+| ppprc_rc  : ∀p,q.   pprec (dx::p) (rc::q)
+| ppprc_sn  : ∀p,q.   pprec (rc::p) (sn::q)
 | pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q)
 | pprec_skip:         pprec (dx::◊) ◊
 .
@@ -36,6 +37,7 @@ notation "hvbox(a break ≺ b)"
 lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
 #p #q #H elim H -p -q // /2 width=1/
 [ #p #q * #H destruct
+| #p #q * #H destruct
 | #c #p #q #_ #IHpq * #H destruct /3 width=1/
 ]
 qed-.
@@ -85,7 +87,11 @@ lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2.
 /2 width=3/
 qed-.
 
-lemma ple_cons: ∀p,q. dx::p ≤ sn::q.
+lemma ple_rc: ∀p,q. dx::p ≤ rc::q.
+/2 width=1/
+qed.
+
+lemma ple_sn: ∀p,q. rc::p ≤ sn::q.
 /2 width=1/
 qed.
 
@@ -106,6 +112,15 @@ lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊.
 #p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/
 qed.
 
+theorem ple_trans: transitive … ple.
+/2 width=3/
+qed-.
+
+lemma ple_cons: ∀p,q. dx::p ≤ sn::q.
+#p #q
+@(ple_trans … (rc::q)) /2 width=1/
+qed.
+
 lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1.
 #p1 elim p1 -p1
 [ * /2 width=1/

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index a7ccb05fd58a58de843e2ececc5ad65f53a9ca7e..ebcc572a40b403cd4f8ee3021279d7d87e0db210 100644 (file)
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "labelled_sequential_computation.ma".
+include "labeled_sequential_computation.ma".
 include "pointer_list_standard.ma".
 
 (* KASHIMA'S "ST" COMPUTATION ***********************************************)
@@ -151,7 +151,7 @@ lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N →
 [ #s #M #i #Hs #HM
   lapply (is_whd_is_standard … Hs) -Hs /2 width=3/
 | #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
-  lapply (lsreds_trans … HM (sn:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
+  lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
   @(ex2_intro … HM) -M -A2 /3 width=1/
 | #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
   lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM