matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.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 "ground_2/lib/star.ma".
  16 include "basic_2/notation/relations/pconvstar_5.ma".
  17 include "basic_2/rt_conversion/cpc.ma".
  18
  19 (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
  20
  21 definition cpcs (h) (G): relation3 lenv term term ≝
  22                          CTC … (cpc h G).
  23
  24 interpretation "context-sensitive parallel r-equivalence (term)"
  25    'PConvStar h G L T1 T2 = (cpcs h G L T1 T2).
  26
  27 (* Basic eliminators ********************************************************)
  28
  29 (* Basic_2A1: was: cpcs_ind_dx *)
  30 lemma cpcs_ind_sn (h) (G) (L) (T2):
  31                   ∀Q:predicate term. Q T2 →
  32                   (∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T → ❪G,L❫ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
  33                   ∀T1. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T1.
  34 normalize /3 width=6 by TC_star_ind_dx/
  35 qed-.
  36
  37 (* Basic_2A1: was: cpcs_ind *)
  38 lemma cpcs_ind_dx (h) (G) (L) (T1):
  39                   ∀Q:predicate term. Q T1 →
  40                   (∀T,T2. ❪G,L❫ ⊢ T1 ⬌*[h] T → ❪G,L❫ ⊢ T ⬌[h] T2 → Q T → Q T2) →
  41                   ∀T2. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T2.
  42 normalize /3 width=6 by TC_star_ind/
  43 qed-.
  44
  45 (* Basic properties *********************************************************)
  46
  47 (* Basic_1: was: pc3_refl *)
  48 lemma cpcs_refl (h) (G): c_reflexive … (cpcs h G).
  49 /2 width=1 by inj/ qed.
  50
  51 (* Basic_1: was: pc3_s *)
  52 lemma cpcs_sym (h) (G) (L): symmetric … (cpcs h G L).
  53 #h #G #L @TC_symmetric
  54 /2 width=1 by cpc_sym/
  55 qed-.
  56
  57 lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  58 /2 width=1 by inj/ qed.
  59
  60 (* Basic_2A1: was: cpcs_strap2 *)
  61 lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T →
  62                                 ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  63 normalize /2 width=3 by TC_strap/
  64 qed-.
  65
  66 (* Basic_2A1: was: cpcs_strap1 *)
  67 lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
  68                                 ∀T2. ❪G,L❫ ⊢ T ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  69 normalize /2 width=3 by step/
  70 qed-.
  71
  72 (* Basic_1: was: pc3_pr2_r *)
  73 lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  74 /3 width=1 by cpc_cpcs, or_introl/ qed.
  75
  76 (* Basic_1: was: pc3_pr2_x *)
  77 lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T2 ➡[h] T1 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  78 /3 width=1 by cpc_cpcs, or_intror/ qed.
  79
  80 (* Basic_1: was: pc3_pr2_u *)
  81 (* Basic_2A1: was: cpcs_cpr_strap2 *)
  82 lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T → ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  83 /3 width=3 by cpcs_step_sn, or_introl/ qed-.
  84
  85 (* Basic_2A1: was: cpcs_cpr_strap1 *)
  86 lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
  87                                     ∀T2. ❪G,L❫ ⊢ T ➡[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  88 /3 width=3 by cpcs_step_dx, or_introl/ qed-.
  89
  90 lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
  91                                 ∀T2. ❪G,L❫ ⊢ T2 ➡[h] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  92 /3 width=3 by cpcs_step_dx, or_intror/ qed-.
  93
  94 lemma cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T →
  95                            ∀T2. ❪G,L❫ ⊢ T2 ➡[h] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
  96 /3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-.
  97
  98 (* Basic_1: was: pc3_pr2_u2 *)
  99 lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T ➡[h] T1 →
 100                                  ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
 101 /3 width=3 by cpcs_step_sn, or_intror/ qed-.
 102
 103 (* Basic_1: removed theorems 9:
 104             clear_pc3_trans pc3_ind_left
 105             pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
 106             pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
 107             pc3_gen_abst pc3_gen_abst_shift
 108 *)
 109 (* Basic_1: removed local theorems 6:
 110             pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left
 111             pc3_wcpr0_t_aux
 112 *)