matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.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/rt_transition/cpr.ma".
  16 include "basic_2/rt_computation/cpms.ma".
  17
  18 (* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************)
  19
  20 (* Basic eliminators ********************************************************)
  21
  22 (* Basic_2A1: was: cprs_ind_dx *)
  23 lemma cprs_ind_sn (h) (G) (L) (T2) (Q:predicate …):
  24                   Q T2 →
  25                   (∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T → ❪G,L❫ ⊢ T ➡*[h] T2 → Q T → Q T1) →
  26                   ∀T1. ❪G,L❫ ⊢ T1 ➡*[h] T2 → Q T1.
  27 #h #G #L #T2 #Q #IH1 #IH2 #T1
  28 @(insert_eq_0 … 0) #n #H
  29 @(cpms_ind_sn … H) -n -T1 //
  30 #n1 #n2 #T1 #T #HT1 #HT2 #IH #H
  31 elim (plus_inv_O3 n1 n2) // -H #H1 #H2 destruct
  32 /3 width=4 by/
  33 qed-.
  34
  35 (* Basic_2A1: was: cprs_ind *)
  36 lemma cprs_ind_dx (h) (G) (L) (T1) (Q:predicate …):
  37                   Q T1 →
  38                   (∀T,T2. ❪G,L❫ ⊢ T1 ➡*[h] T → ❪G,L❫ ⊢ T ➡[h] T2 → Q T → Q T2) →
  39                   ∀T2. ❪G,L❫ ⊢ T1 ➡*[h] T2 → Q T2.
  40 #h #G #L #T1 #Q #IH1 #IH2 #T2
  41 @(insert_eq_0 … 0) #n #H
  42 @(cpms_ind_dx … H) -n -T2 //
  43 #n1 #n2 #T #T2 #HT1 #IH #HT2 #H
  44 elim (plus_inv_O3 n1 n2) // -H #H1 #H2 destruct
  45 /3 width=4 by/
  46 qed-.
  47
  48 (* Basic properties *********************************************************)
  49
  50 (* Basic_1: was: pr3_step *)
  51 (* Basic_2A1: was: cprs_strap2 *)
  52 lemma cprs_step_sn (h) (G) (L):
  53                    ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T →
  54                    ∀T2. ❪G,L❫ ⊢ T ➡*[h] T2 → ❪G,L❫ ⊢ T1 ➡*[h] T2.
  55 /2 width=3 by cpms_step_sn/ qed-.
  56
  57 (* Basic_2A1: was: cprs_strap1 *)
  58 lemma cprs_step_dx (h) (G) (L):
  59                    ∀T1,T. ❪G,L❫ ⊢ T1 ➡*[h] T →
  60                    ∀T2. ❪G,L❫ ⊢ T ➡[h] T2 → ❪G,L❫ ⊢ T1 ➡*[h] T2.
  61 /2 width=3 by cpms_step_dx/ qed-.
  62
  63 (* Basic_1: was only: pr3_thin_dx *)
  64 lemma cprs_flat_dx (h) (I) (G) (L):
  65                    ∀V1,V2. ❪G,L❫ ⊢ V1 ➡[h] V2 →
  66                    ∀T1,T2. ❪G,L❫ ⊢ T1 ➡*[h] T2 →
  67                    ❪G,L❫ ⊢ ⓕ[I]V1.T1 ➡*[h] ⓕ[I]V2.T2.
  68 #h #I #G #L #V1 #V2 #HV12 #T1 #T2 #H @(cprs_ind_sn … H) -T1
  69 /3 width=3 by cprs_step_sn, cpm_cpms, cpr_flat/
  70 qed.
  71
  72 lemma cprs_flat_sn (h) (I) (G) (L):
  73                    ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h] T2 → ∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h] V2 →
  74                    ❪G,L❫ ⊢ ⓕ[I] V1. T1 ➡*[h] ⓕ[I] V2. T2.
  75 #h #I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind_sn … H) -V1
  76 /3 width=3 by cprs_step_sn, cpm_cpms, cpr_flat/
  77 qed.
  78
  79 (* Basic inversion lemmas ***************************************************)
  80
  81 (* Basic_1: was: pr3_gen_sort *)
  82 lemma cprs_inv_sort1 (h) (G) (L): ∀X2,s. ❪G,L❫ ⊢ ⋆s ➡*[h] X2 → X2 = ⋆s.
  83 /2 width=4 by cpms_inv_sort1/ qed-.
  84
  85 (* Basic_1: was: pr3_gen_cast *)
  86 lemma cprs_inv_cast1 (h) (G) (L): ∀W1,T1,X2. ❪G,L❫ ⊢ ⓝW1.T1 ➡*[h] X2 →
  87                                   ∨∨ ∃∃W2,T2. ❪G,L❫ ⊢ W1 ➡*[h] W2 & ❪G,L❫ ⊢ T1 ➡*[h] T2 & X2 = ⓝW2.T2
  88                                    | ❪G,L❫ ⊢ T1 ➡*[h] X2.
  89 #h #G #L #W1 #T1 #X2 #H
  90 elim (cpms_inv_cast1 … H) -H
  91 [ /2 width=1 by or_introl/
  92 | /2 width=1 by or_intror/
  93 | * #m #_ #H destruct
  94 ]
  95 qed-.
  96
  97 (* Basic_1: removed theorems 13:
  98    pr1_head_1 pr1_head_2 pr1_comp
  99    clear_pr3_trans pr3_cflat pr3_gen_bind
 100    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
 101    pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 102 *)