some renaming ...

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 30b4fdf6409b7690a05b7b7995e9592d92f90c20..27f30b22c199a2d47544019c18b6e482174e09e0 100644 (file)
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -39,12 +39,12 @@ definition is_dx: predicate ptr_step ≝ λc. dx = c.
 (* Note: this is a path in the tree representation of a term, heading to a redex *)
 definition ptr: Type[0] ≝ list ptr_step.
 
-(* Note: a redex is "in the head" when is not under an abstraction nor in the lefr argument of an application *)
-definition in_head: predicate ptr ≝ All … is_dx.
+(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
+definition in_whd: predicate ptr ≝ All … is_dx.
 
-lemma in_head_ind: ∀R:predicate ptr. R (◊) →
-                   (∀p. in_head p → R p → R (dx::p)) →
-                   ∀p. in_head p → R p.
+lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
+                  (∀p. in_whd p → R p → R (dx::p)) →
+                  ∀p. in_whd p → R p.
 #R #H #IH #p elim p -p // -H *
 #p #IHp * #H1 #H2 destruct /3 width=1/
 qed-.

diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma
index 23a96a56679b8b3e2bb7de936ddb688d63e97301..82f704a78e681ac59dd98157019326709be40e1c 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_list.ma
+++ b/matita/matita/contribs/lambda/pointer_list.ma
@@ -19,15 +19,15 @@ include "pointer.ma".
 (* Policy: pointer list metavariables: r, s *)
 definition ptrl: Type[0] ≝ list ptr.
 
-(* Note: a "head" computation contracts just redexes in the head *)
-definition is_head: predicate ptrl ≝ All … in_head.
+(* Note: a "whd" computation contracts just redexes in the whd *)
+definition is_whd: predicate ptrl ≝ All … in_whd.
 
-lemma is_head_dx: ∀s. is_head s → is_head (dx:::s).
+lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
 #s elim s -s //
 #p #s #IHs * /3 width=1/ 
 qed.
 
-lemma is_head_append: ∀r. is_head r → ∀s. is_head s → is_head (r@s).
+lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
 #r elim r -r //
 #q #r #IHr * /3 width=1/
 qed.

diff --git a/matita/matita/contribs/lambda/pointer_list_standard.ma b/matita/matita/contribs/lambda/pointer_list_standard.ma
index 9d70a3a19f4fc84d3a6dcf2d73e8b38a5acb8b46..8ae8d5aa171b3309b51ecb59474daed6aa35d0b5 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_list_standard.ma
+++ b/matita/matita/contribs/lambda/pointer_list_standard.ma
@@ -35,16 +35,16 @@ lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_sta
 #q #r #IHr * /3 width=1/
 qed.
 
-theorem is_head_is_standard: ∀s. is_head s → is_standard s.
+theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
 #s elim s -s // #p * //
 #q #s #IHs * /3 width=1/
 qed.
 
-lemma is_standard_in_head: ∀p. in_head p → ∀s. is_standard s → is_standard (p::s).
+lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
 #p #Hp * // /3 width=1/
 qed.
 
-theorem is_head_is_standard_trans: ∀r. is_head r → ∀s. is_standard s → is_standard (r@s).
+theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
 #r elim r -r // #p *
 [ #_ * /2 width=1/
 | #q #r #IHr * /3 width=1/

diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma
index 24dcad4fa953a14824c8c4f610287967fa850e69..92618412e635092d8043edaef6227a64d2660a10 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_order.ma
+++ b/matita/matita/contribs/lambda/pointer_order.ma
@@ -33,7 +33,7 @@ notation "hvbox(a break ≺ b)"
    non associative with precedence 45
    for @{ 'prec $a $b }.
 
-lemma pprec_fwd_in_head: ∀p,q. p ≺ q → in_head q → in_head p.
+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
 | #c #p #q #_ #IHpq * #H destruct /3 width=1/
@@ -115,19 +115,19 @@ lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1.
 ]
 qed-.
 
-lemma in_head_ple_nil: ∀p. in_head p → p ≤ ◊.
-#p #H @(in_head_ind … H) -p // /2 width=1/
+lemma in_whd_ple_nil: ∀p. in_whd p → p ≤ ◊.
+#p #H @(in_whd_ind … H) -p // /2 width=1/
 qed.
 
-theorem in_head_ple: ∀p. in_head p → ∀q. p ≤ q.
-#p #H @(in_head_ind … H) -p //
+theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q.
+#p #H @(in_whd_ind … H) -p //
 #p #_ #IHp * /3 width=1/ * #q /2 width=1/
 qed.
 
-lemma ple_nil_inv_in_head: ∀p. p ≤ ◊ → in_head p.
-#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_head/
+lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p.
+#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/
 qed-.
 
-lemma ple_inv_in_head: ∀p. (∀q. p ≤ q) → in_head p.
-/2 width=1 by ple_nil_inv_in_head/
+lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p.
+/2 width=1 by ple_nil_inv_in_whd/
 qed-.

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index 3ba98df9e36f7735933c9811e6358d3f479fb9ed..a7ccb05fd58a58de843e2ececc5ad65f53a9ca7e 100644 (file)
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -21,9 +21,9 @@ include "pointer_list_standard.ma".
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
 inductive st: relation term ≝
-| st_vref: ∀s,M,i. is_head s → M ↦*[s] #i → st M (#i)
-| st_abst: ∀s,M,A1,A2. is_head s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
-| st_appl: ∀s,M,B1,B2,A1,A2. is_head s → M ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
+| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i)
+| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
 .
 
 interpretation "'st' computation"
@@ -34,7 +34,7 @@ notation "hvbox( M ⓢ⤇* break term 46 N )"
    for @{ 'Std $M $N }.
 
 lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N →
-                   ∃∃s. is_head s & M ↦*[s] #j.
+                   ∃∃s. is_whd s & M ↦*[s] #j.
 #M #N * -M -N
 [ /2 width=3/
 | #s #M #A1 #A2 #_ #_ #_ #j #H destruct
@@ -43,7 +43,7 @@ lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N →
 qed-.
 
 lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N →
-                   ∃∃s,C1. is_head s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2.
+                   ∃∃s,C1. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2.
 #M #N * -M -N
 [ #s #M #i #_ #_ #C2 #H destruct
 | #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/
@@ -52,7 +52,7 @@ lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N →
 qed-.
 
 lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N →
-                   ∃∃s,D1,C1. is_head s & M ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2.
+                   ∃∃s,D1,C1. is_whd s & M ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2.
 #M #N * -M -N
 [ #s #M #i #_ #_ #D2 #C2 #H destruct
 | #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct
@@ -64,7 +64,7 @@ lemma st_refl: reflexive … st.
 #M elim M -M /2 width=3/ /2 width=5/ /2 width=7/
 qed.
 
-lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_head s → M ↦*[s] N1 → M ⓢ⤇* N2.
+lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2.
 #N1 #N2 #H elim H -N1 -N2
 [ #r #N #i #Hr #HN #s #M #Hs #HMN
   lapply (lsreds_trans … HMN … HN) -N /3 width=3/
@@ -75,7 +75,7 @@ lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_head s → M ↦*[s] N1
 ]
 qed-.
 
-lemma st_step_rc: ∀s,M1,M2. is_head s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
+lemma st_step_rc: ∀s,M1,M2. is_whd s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
 /3 width=5 by st_step_sn/
 qed.
 
@@ -149,7 +149,7 @@ lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N →
                                  ∃∃r. M ↦*[r] N & is_standard r.
 #M #N #H elim H -M -N
 [ #s #M #i #Hs #HM
-  lapply (is_head_is_standard … Hs) -Hs /2 width=3/
+  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
   @(ex2_intro … HM) -M -A2 /3 width=1/
@@ -172,12 +172,12 @@ theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_sta
 @st_inv_lsreds_is_standard /2 width=2/
 qed-.
 
-(* Note: we use "lapply (rewrite_r ?? is_head … Hq)" (procedural)
-         in place of "cut (is_head (q::r)) [ >Hq ]"  (declarative)
+(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural)
+         in place of "cut (is_whd (q::r)) [ >Hq ]"  (declarative)
 *)
-lemma st_lsred_swap: ∀p. in_head p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 →
-                     ∃∃q,M2. in_head q & M1 ↦[q] M2 & M2 ⓢ⤇* N2.
-#p #H @(in_head_ind … H) -p
+lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 →
+                     ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2.
+#p #H @(in_whd_ind … H) -p
 [ #N1 #N2 #H1 #M1 #H2
   elim (lsred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2
   elim (st_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
@@ -187,7 +187,7 @@ lemma st_lsred_swap: ∀p. in_head p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 
   elim (lsreds_inv_pos … HM1 ?) -HM1
   [2: >length_append normalize in ⊢ (??(??%)); // ]
   #q #r #M #Hq #HM1 #HM
-  lapply (rewrite_r ?? is_head … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
+  lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
   @(ex3_2_intro … HM1) -M1 // -q
   @(st_step_sn … HM) /2 width=1/
 | #p #_ #IHp #N1 #N2 #H1 #M1 #H2
@@ -198,14 +198,14 @@ lemma st_lsred_swap: ∀p. in_head p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 
   elim (lsreds_inv_pos … HM1 ?) -HM1
   [2: >length_append normalize in ⊢ (??(??%)); // ]
   #q #r #M #Hq #HM1 #HM
-  lapply (rewrite_r ?? is_head … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
+  lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
   @(ex3_2_intro … HM1) -M1 // -q /2 width=7/
 ]
 qed-.
 
 theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 →
-                           ∀p,N2. in_head p → N1 ↦[p] N2 →
-                           ∃∃q,r,M2. in_head q & M1 ↦[q] M2 & M2 ↦*[r] N2 &
+                           ∀p,N2. in_whd p → N1 ↦[p] N2 →
+                           ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 &
                                      is_standard (q::r).
 #s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
 lapply (st_lsreds … HMN1) -s #HMN1