From: Ferruccio Guidi Date: Thu, 20 Dec 2012 14:52:58 +0000 (+0000) Subject: - nat.ma: cut removed from f_ind :) X-Git-Tag: make_still_working~1379 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=07f64a04ac6061c853d2e60237a7173968c6d759;p=helm.git - nat.ma: cut removed from f_ind :) - lanbda: some refactoring --- 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_list.ma b/matita/matita/contribs/lambda/pointer_list.ma new file mode 100644 index 000000000..23a96a566 --- /dev/null +++ b/matita/matita/contribs/lambda/pointer_list.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma deleted file mode 100644 index fa153ccd4..000000000 --- a/matita/matita/contribs/lambda/pointer_sequence.ma +++ /dev/null @@ -1,88 +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_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. 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 **************************************************)