From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 18 Nov 2011 12:27:16 +0000 (+0000)
Subject: support for candidates of reducibility started ...
X-Git-Tag: make_still_working~2093
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;p=helm.git

support for candidates of reducibility started ...
---

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
 .