matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Basic_2/grammar/aarity.ma".
  16 include "Basic_2/grammar/term_simple.ma".
  17 include "Basic_2/substitution/lift_vector.ma".
  18 include "Basic_2/computation/acp.ma".
  19
  20 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
  21
  22 (* Note: this is Girard's CR1 *)
  23 definition S1 ≝ λRP,C:lenv→predicate term.
  24                 ∀L,T. C L T → RP L T.
  25
  26 (* Note: this is Tait's iii, or Girard's CR4 *)
  27 definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
  28                 ∀L,Vs. all … (RP L) Vs →
  29                 ∀T. 𝕊[T] → NF … (RR L) RS T → C L (ⒶVs.T).
  30
  31 (* Note: this is Tait's ii *)
  32 definition S3 ≝ λRP,C:lenv→predicate term.
  33                 ∀L,Vs,V,T,W. C L (ⒶVs. 𝕔{Abbr}V. T) → RP L W → C L (ⒶVs. 𝕔{Appl}V. 𝕔{Abst}W. T).
  34
  35 definition S5 ≝ λRP,C:lenv→predicate term.
  36                 ∀L,V1s,V2s. ⇑[0, 1] V1s ≡ V2s →
  37                 ∀V,T. C (L. 𝕓{Abbr}V) (ⒶV2s. T) → RP L V → C L (ⒶV1s. 𝕔{Abbr}V. T).
  38
  39 definition S6 ≝ λRP,C:lenv→predicate term.
  40                 ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. 𝕔{Cast}W. T).
  41
  42 definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e.
  43                 C L1 T1 → ⇓[d, e] L2 ≡ L1 → ⇑[d, e] T1 ≡ T2 → C L2 T2.
  44
  45 (* properties of the abstract candidate of reducibility *)
  46 record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝
  47 { s1: S1 RP C;
  48   s2: S2 RR RS RP C;
  49   s3: S3 RP C;
  50   s5: S5 RP C;
  51   s6: S6 RP C;
  52   s7: S7 C
  53 }.
  54
  55 (* the abstract candidate of reducibility associated to an atomic arity *)
  56 let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
  57 λT. match A with
  58 [ AAtom     ⇒ RP L T
  59 | APair B A ⇒ ∀V. aacr RP B L V → aacr RP A L (𝕔{Appl} V. T)
  60 ].
  61
  62 interpretation
  63    "candidate of reducibility of an atomic arity (abstract)"
  64    'InEInt RP L T A = (aacr RP A L T).
  65
  66 (* Basic properties *********************************************************)
  67
  68 axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
  69                 ∀A. acr RR RS RP (aacr RP A).
  70 (*
  71 #RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
  72 #B #A #IHB #IHA @mk_acr normalize
  73 [ #L #T #H
  74   lapply (H (⋆0) ?) -H [ @(s2 … IHB … ◊) // /2 width=2/ ] #H
  75   @(cp3 … H1RP … 0) @(s1 … IHA) //
  76 | #L #Vs #HVs #T #H1T #H2T #V #HB
  77   lapply (s1 … IHB … HB) #HV
  78   @(s2 … IHA … (V :: Vs)) // /2 width=1/
  79 | #L #Vs #V #T #W #HA #HW #V0 #HB
  80   @(s3 … IHA … (V0 :: Vs)) // /2 width=1/
  81 | #L #V1s #V2s #HV12s #V #T #HA #HV #V1 #HB
  82   elim (lift_total V1 0 1) #V2 #HV12
  83   @(s5 … IHA … (V1 :: V1s) (V2 :: V2s)) // /2 width=1/
  84   @HA @(s7 … IHB … HB … HV12) /2 width=1/
  85 | #L #Vs #T #W #HA #HW #V0 #HB
  86   @(s6 … IHA … (V0 :: Vs)) // /2 width=1/
  87 | #L1 #L2 #T1 #T2 #d #e #HA #HL21 #HT12 #V2 #HB
  88   @(s7 … IHA … HL21) [2: @HA [2:
  89 ]
  90 qed.
  91 *)
  92 lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
  93                  ∀L,W,T,A,B. RP L W →
  94                  (∀V. ⦃L, V⦄ [RP] ϵ 〚B〛 → ⦃L. 𝕓{Abbr}V, T⦄ [RP] ϵ 〚A〛) →
  95                               ⦃L, 𝕓{Abst}W. T⦄ [RP] ϵ 〚𝕔B. A〛.
  96 #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #V #HB
  97 lapply (aacr_acr … H1RP H2RP A) #HCA
  98 lapply (aacr_acr … H1RP H2RP B) #HCB
  99 lapply (s1 … HCB) -HCB #HCB
 100 @(s3 … HCA … ◊) // @(s5 … HCA … ◊ ◊) // /2 width=1/
 101 qed.