From fc7af5f9ea2cd4a876b8babc6b691136799e3c87 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 18 Nov 2011 12:27:16 +0000 Subject: [PATCH] support for candidates of reducibility started ... --- .../lambda_delta/Basic_2/grammar/cl_weight.ma | 2 +- .../Basic_2/grammar/term_simple.ma | 2 +- .../Basic_2/grammar/term_weight.ma | 2 +- .../Basic_2/reducibility/apr_cr.ma | 43 +++++++++++++++++++ .../lambda_delta/Basic_2/reducibility/tnf.ma | 3 +- .../lambda_delta/Basic_2/reducibility/trf.ma | 5 +-- .../Basic_2/reducibility/twhnf.ma | 3 +- .../lambda_delta/Basic_2/unfold/ltpss.ma | 2 +- .../lambda_delta/Basic_2/unfold/tpss.ma | 2 +- .../lambda_delta/Ground_2/notation.ma | 6 +++ .../contribs/lambda_delta/Ground_2/star.ma | 8 ++-- 11 files changed, 63 insertions(+), 15 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma index 355b8a797..0414499a5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma @@ -26,7 +26,7 @@ interpretation "weight (closure)" 'Weight L T = (cw L T). (* Basic_1: was: flt_wf__q_ind *) (* Basic_1: was: flt_wf_ind *) -axiom cw_wf_ind: ∀R:lenv→term→Prop. +axiom cw_wf_ind: ∀R:lenv→predicate term. (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) → ∀L,T. R L T. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma index cd387ee02..be4811eeb 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma @@ -16,7 +16,7 @@ include "Basic_2/grammar/term.ma". (* SIMPLE (NEUTRAL) TERMS ***************************************************) -inductive simple: term → Prop ≝ +inductive simple: predicate term ≝ | simple_atom: ∀I. simple (𝕒{I}) | simple_flat: ∀I,V,T. simple (𝕗{I} V. T) . diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma index 874f030f6..8eaa24aca 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma @@ -32,7 +32,7 @@ qed. (* Basic eliminators ********************************************************) -axiom tw_wf_ind: ∀R:term→Prop. +axiom tw_wf_ind: ∀R:predicate term. (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) → ∀T. R T. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma new file mode 100644 index 000000000..b46de8470 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/term_simple.ma". + +(* CANDIDATES OF REDUCIBILITY ***********************************************) + +(* abstract conditions for candidates *) + +definition CR1: predicate term → predicate term → Prop ≝ + λRD,RC. ∀T. RC T → RD T. + +definition CR2: relation term → predicate term → Prop ≝ + λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2. + +definition CR3: relation term → predicate term → Prop ≝ + λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1. + +(* a candidate *) +record cr (RR:relation term) (RD:predicate term): Type[0] ≝ { + in_cr: predicate term; + cr1: CR1 RD in_cr; + cr2: CR2 RR in_cr; + cr3: CR3 RR in_cr +}. + +interpretation + "context-free parallel reduction (term)" + 'InSubset T R = (in_cr ? ? R T). + +definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝ + λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma index a9a262efe..5772e7626 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -18,8 +18,7 @@ include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE NORMAL TERMS ************************************************) -definition tnf: term → Prop ≝ - NF … tpr (eq …). +definition tnf: predicate term ≝ NF … tpr (eq …). interpretation "context-free normality (term)" diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma index ccdf59224..96d678716 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma @@ -17,7 +17,7 @@ include "Basic_2/grammar/term_simple.ma". (* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************) (* reducible terms *) -inductive trf: term → Prop ≝ +inductive trf: predicate term ≝ | trf_abst_sn: ∀V,T. trf V → trf (𝕔{Abst} V. T) | trf_abst_dx: ∀V,T. trf T → trf (𝕔{Abst} V. T) | trf_appl_sn: ∀V,T. trf V → trf (𝕔{Appl} V. T) @@ -32,8 +32,7 @@ interpretation 'Reducible T = (trf T). (* irreducible terms *) -definition tif: term → Prop ≝ - λT. ℝ[T] → False. +definition tif: predicate term ≝ λT. ℝ[T] → False. interpretation "context-free irreducibility (term)" 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 dea7077b4..ccfaa6aa6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma @@ -17,8 +17,7 @@ include "Basic_2/reducibility/tpr.ma". (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************) -definition twhnf: term → Prop ≝ - NF … tpr thom. +definition twhnf: predicate term ≝ NF … tpr thom. interpretation "context-free weak head normality (term)" diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma index 456a3aae0..eb02c3a06 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -25,7 +25,7 @@ interpretation "partial unfold (local environment)" (* Basic eliminators ********************************************************) -lemma ltpss_ind: ∀d,e,L1. ∀R: lenv → Prop. R L1 → +lemma ltpss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 → (∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) → ∀L2. L1 [d, e] ≫* L2 → R L2. #d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma index 62eb25d49..f21f3603e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma @@ -24,7 +24,7 @@ interpretation "partial unfold (term)" (* Basic eliminators ********************************************************) -lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 → +lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 → (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) → ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2. #d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma index dab6b4982..65cb0a029 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma @@ -14,6 +14,12 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* Subsets ******************************************************************) + +notation "hvbox( T ϵ break R )" + non associative with precedence 45 + for @{ 'InSubset $T $R }. + (* Lists ********************************************************************) notation "hvbox( hd break :: tl )" diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma index e438b44f0..097151367 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma @@ -17,6 +17,8 @@ include "Ground_2/xoa_props.ma". (* PROPERTIES of RELATIONS **************************************************) +definition predicate: Type[0] → Type[0] ≝ λA. A → Prop. + definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False). @@ -105,16 +107,16 @@ qed. lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R). /2/ qed. -lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop. +lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A. P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) → ∀a2. TC … R a1 a2 → P a2. #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/ qed. -definition NF: ∀A. relation A → relation A → A → Prop ≝ +definition NF: ∀A. relation A → relation A → predicate A ≝ λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. -inductive SN (A) (R,S:relation A): A → Prop ≝ +inductive SN (A) (R,S:relation A): predicate A ≝ | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1 . -- 2.39.2