From 07f64a04ac6061c853d2e60237a7173968c6d759 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 20 Dec 2012 14:52:58 +0000 Subject: [PATCH] - nat.ma: cut removed from f_ind :) - lanbda: some refactoring --- .../lambda/labelled_sequential_computation.ma | 4 +- .../{pointer_sequence.ma => pointer_list.ma} | 50 +++---------------- matita/matita/contribs/lambda/pointer_tree.ma | 14 +++--- .../matita/contribs/lambda/st_computation.ma | 19 +++---- matita/matita/lib/arithmetics/nat.ma | 11 ++-- 5 files changed, 35 insertions(+), 63 deletions(-) rename matita/matita/contribs/lambda/{pointer_sequence.ma => pointer_list.ma} (60%) diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma index 837c9668d..f62864831 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -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). diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_list.ma similarity index 60% rename from matita/matita/contribs/lambda/pointer_sequence.ma rename to matita/matita/contribs/lambda/pointer_list.ma index fa153ccd4..23a96a566 100644 --- a/matita/matita/contribs/lambda/pointer_sequence.ma +++ b/matita/matita/contribs/lambda/pointer_list.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -include "pointer_order.ma". +include "pointer.ma". -(* POINTER SEQUENCE *********************************************************) +(* POINTER LIST *************************************************************) -(* Policy: pointer sequence metavariables: r, s *) -definition pseq: Type[0] ≝ list ptr. +(* 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 pseq ≝ All … in_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 // @@ -32,47 +32,13 @@ lemma is_head_append: ∀r. is_head r → ∀s. is_head s → is_head (r@s). #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. +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 (pseq→relation term) ≝ λR. +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 (pseq→relation term) ≝ λR. +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). diff --git a/matita/matita/contribs/lambda/pointer_tree.ma b/matita/matita/contribs/lambda/pointer_tree.ma index 89d2122c2..4381cd62c 100644 --- a/matita/matita/contribs/lambda/pointer_tree.ma +++ b/matita/matita/contribs/lambda/pointer_tree.ma @@ -12,20 +12,20 @@ (* *) (**************************************************************************) -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). diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index db418c763..3ba98df9e 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "labelled_sequential_computation.ma". +include "pointer_list_standard.ma". (* KASHIMA'S "ST" COMPUTATION ***********************************************) @@ -144,11 +145,11 @@ lemma st_lsreds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ⤇* M2. #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/ @@ -161,14 +162,14 @@ qed-. 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) @@ -205,9 +206,9 @@ 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 & - 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-. diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 67b7de50b..5b430d7c6 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -495,12 +495,17 @@ cut (∀q:nat. q ≤ n → P q) /2/ ] 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 **************************************************) -- 2.39.2