From 9581b03be2b2bc830820b93992920aaa2c021cc9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 16 Nov 2011 23:40:42 +0000 Subject: [PATCH] - lambda_delta: context-free weak head normal forms continued ... - delift started ... - nnAuto: we removed an optimization that breaks lambda_delta --- matita/components/ng_tactics/nnAuto.ml | 5 +- .../lambda_delta/Basic_2/grammar/thom.ma | 27 +++++++++++ .../Basic_2/reducibility/twhnf.ma | 47 ++++++++++++++++++- .../lambda_delta/Basic_2/substitution/tps.ma | 6 +-- .../Basic_2/unfold/{tsubst.ma => delift.ma} | 8 ++-- .../lambda_delta/Ground_2/xoa.conf.xml | 1 + .../contribs/lambda_delta/Ground_2/xoa.ma | 8 ++++ .../lambda_delta/Ground_2/xoa_notation.ma | 10 ++++ 8 files changed, 101 insertions(+), 11 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/unfold/{tsubst.ma => delift.ma} (84%) diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 320f4f630..572cd4e28 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -973,6 +973,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = with Error _ -> smart_apply_auto ("",0,t) eq_cache status in +(* FG: this optimization rules out some applications of + * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma) + * (* we compare the expected branching with the actual one and prune the candidate when the latter is larger. The optimization is meant to rule out stange applications of flexible terms, @@ -993,7 +996,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); debug_print ~depth (lazy "strange application"); None) else - (incr candidate_no; Some ((!candidate_no,t),status)) +*) (incr candidate_no; Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma index d796e10ba..4bb9748d2 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -49,6 +49,33 @@ lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. (* Basic inversion lemmas ***************************************************) +fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 → + ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2. +#T1 #T2 * -T1 T2 +[ #J #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -V1 T1 /2/ +| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct +] +qed. + +lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 → + ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2. +/2 width=5/ qed-. + +fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 → + ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & + I = Appl & T2 = 𝕔{Appl} W2. U2. +#T1 #T2 * -T1 T2 +[ #J #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct -V1 T1 /2 width=5/ +] +qed. + +lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 → + ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & + I = Appl & T2 = 𝕔{Appl} W2. U2. +/2/ qed-. (* Basic_1: removed theorems 7: iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma index c96bf4762..dea7077b4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma @@ -1,12 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/grammar/thom.ma". include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************) definition twhnf: term → Prop ≝ - NF … tpr (thom …). + NF … tpr thom. interpretation "context-free weak head normality (term)" 'WHdNormal T = (twhnf T). +(* Basic inversion lemmas ***************************************************) + +lemma twhnf_inv_thom: ∀T. 𝕎ℍℕ[T] → T ≈ T. +normalize /2 depth=1/ +qed-. + (* Basic properties *********************************************************) + +lemma tpr_thom: ∀T1,T2. T1 ⇒ T2 → T1 ≈ T1 → T1 ≈ T2. +#T1 #T2 #H elim H -T1 T2 // +[ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H + elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct -I T1 V1; + lapply (IHT12 HT1U2) -IHT12 HT1U2 #HUT2 + lapply (simple_thom_repl_dx … HUT2 HT1) /2 width=1/ +| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #H + elim (simple_inv_bind … H) +| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H + elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct -I // +| #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (thom_inv_flat1 … H) -H #U1 #U2 #_ #H + elim (simple_inv_bind … H) +| #V #T #T1 #T2 #_ #_ #_ #H + elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct +| #V #T1 #T2 #_ #_ #H + elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct +] +qed. + +lemma twhnf_thom: ∀T. T ≈ T → 𝕎ℍℕ[T]. +/2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma index 744c00b81..9f10dcc2a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -220,11 +220,7 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2. lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → #[T1] ≤ #[T2]. #L #T1 #T2 #d #e #H elim H normalize -H L T1 T2 d e -[ // -| /2/ -| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *) -| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *) -] +/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *) qed-. (* Basic_1: removed theorems 25: diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma similarity index 84% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma rename to matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma index 7d31f3bd9..5d19b650e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma @@ -14,10 +14,10 @@ include "Basic_2/unfold/tpss.ma". -(* SUBSTITUTION ON TERMS ****************************************************) +(* DELIFT ON TERMS **********************************************************) -definition tsubst: nat → nat → lenv → relation term ≝ +definition delift: nat → nat → lenv → relation term ≝ λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ≫* T & ↑[d, e] T2 ≡ T. -interpretation "substitution (term)" - 'TSubst L T1 d e T2 = (tsubst d e L T1 T2). +interpretation "delift (term)" + 'TSubst L T1 d e T2 = (delift d e L T1 T2). diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml index ac5635c7c..5a4cf8c49 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml @@ -22,6 +22,7 @@ 4 2 4 3 4 4 + 5 2 5 3 5 4 6 4 diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma index 2b75c902d..48593d76e 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma @@ -80,6 +80,14 @@ inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : P interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). +(* multiple existental quantifier (5, 2) *) + +inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ + | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). + (* multiple existental quantifier (5, 3) *) inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma index 80f9762a6..20ab21e69 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma @@ -94,6 +94,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. +(* multiple existental quantifier (5, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) (λ${ident x0}.λ${ident x1}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P4) }. + (* multiple existental quantifier (5, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" -- 2.39.2