(* *)
(**************************************************************************)
-include "pointer_sequence.ma".
+include "pointer_list.ma".
include "parallel_computation.ma".
(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
-definition lsreds: pseq → relation term ≝ lstar … lsred.
+definition lsreds: ptrl → relation term ≝ lstar … lsred.
interpretation "labelled sequential computation"
'SeqRedStar M s N = (lsreds s M N).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
+(* POINTER LIST *************************************************************)
+
+(* 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.
+
+lemma is_head_dx: ∀s. is_head s → is_head (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).
+#r elim r -r //
+#q #r #IHr * /3 width=1/
+qed.
+
+definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR.
+ ∀s,A1,A2. R s A1 A2 → R (sn:::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).
+
+definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR.
+ ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
+
+lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
+#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_order.ma".
-
-(* POINTER SEQUENCE *********************************************************)
-
-(* Policy: pointer sequence metavariables: r, s *)
-definition pseq: Type[0] ≝ list ptr.
-
-(* Note: a "head" computation contracts just redexes in the head *)
-definition is_head: predicate pseq ≝ All … in_head.
-
-lemma is_head_dx: ∀s. is_head s → is_head (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).
-#r elim r -r //
-#q #r #IHr * /3 width=1/
-qed.
-
-(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
-definition is_le: predicate pseq ≝ Allr … ple.
-
-lemma is_le_compatible: ∀c,s. is_le s → is_le (c:::s).
-#c #s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_le_cons: ∀p,s. is_le s → is_le ((dx::p)::sn:::s).
-#p #s elim s -s // #q1 * /2 width=1/
-#q2 #s #IHs * /4 width=1/
-qed.
-
-lemma is_le_append: ∀r. is_le r → ∀s. is_le s → is_le ((dx:::r)@sn:::s).
-#r elim r -r /3 width=1/ #p * /2 width=1/
-#q #r #IHr * /3 width=1/
-qed.
-
-theorem is_head_is_le: ∀s. is_head s → is_le s.
-#s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_le_in_head: ∀p. in_head p → ∀s. is_le s → is_le (p::s).
-#p #Hp * // /3 width=1/
-qed.
-
-theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s).
-#r elim r -r // #p *
-[ #_ * /2 width=1/
-| #q #r #IHr * /3 width=1/
-]
-qed.
-
-definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR.
- ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2).
-
-definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR.
- ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
-
-definition ho_compatible_dx: predicate (pseq→relation term) ≝ λR.
- ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
-
-lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
-#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
-#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
-#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
(* *)
(**************************************************************************)
-include "pointer_sequence.ma".
+include "pointer_list.ma".
(* POINTER TREE *************************************************************)
(* Policy: pointer tree metavariables: P, Q *)
(* Note: this is a binary tree on pointer sequences *)
-inductive ptree: Type[0] ≝
-| tnil : ptree
-| tcons: pseq → ptree → ptree → ptree
+inductive ptrt: Type[0] ≝
+| tnil : ptrt
+| tcons: ptrl → ptrt → ptrt → ptrt
.
-let rec size (P:ptree) on P ≝ match P with
+let rec length (P:ptrt) on P ≝ match P with
[ tnil ⇒ 0
-| tcons s Q1 Q2 ⇒ size Q2 + size Q1 + |s|
+| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s|
].
-interpretation "pointer tree size" 'card P = (size P).
+interpretation "pointer tree length" 'card P = (length P).
(**************************************************************************)
include "labelled_sequential_computation.ma".
+include "pointer_list_standard.ma".
(* KASHIMA'S "ST" COMPUTATION ***********************************************)
#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/
qed.
-lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⤇* N →
- ∃∃r. M ↦*[r] N & is_le r.
+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_le … Hs) -Hs /2 width=3/
+ lapply (is_head_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/
theorem st_trans: transitive … st.
#M1 #M #M2 #HM1 #HM2
-elim (st_inv_lsreds_is_le … HM1) -HM1 #s1 #HM1 #_
-elim (st_inv_lsreds_is_le … HM2) -HM2 #s2 #HM2 #_
+elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_
+elim (st_inv_lsreds_is_standard … HM2) -HM2 #s2 #HM2 #_
lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
qed-.
-theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_le r.
+theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_standard r.
#s #M #N #H
-@st_inv_lsreds_is_le /2 width=2/
+@st_inv_lsreds_is_standard /2 width=2/
qed-.
(* Note: we use "lapply (rewrite_r ?? is_head … Hq)" (procedural)
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 &
- is_le (q::r).
+ is_standard (q::r).
#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
lapply (st_lsreds … HMN1) -s #HMN1
elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2
-elim (st_inv_lsreds_is_le … HMN2) -HMN2 /3 width=8/
+elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/
qed-.
]
qed.
+fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+ (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
+ ∀n,a. f a = n → P a.
+#A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
(∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
#A #f #P #H #a
-cut (∀n,a. f a = n → P a) /2 width=3/ -a
-#n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *)
-qed-.
+@(f_ind_aux … H) -H [2: // | skip ]
+qed-.
(* More negated equalities **************************************************)
projects / helm.git / commitdiff