matita/matita/contribs/lambda_delta/Basic_2/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 "Basic_2/conversion/cpc.ma".
  16
  17 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
  18
  19 definition cpcs: lenv → relation term ≝
  20                  λL. TC … (cpc L).
  21
  22 interpretation "context-sensitive parallel equivalence (term)"
  23    'PConvStar L T1 T2 = (cpcs L T1 T2).
  24
  25 (* Basic eliminators ********************************************************)
  26
  27 lemma cpcs_ind: ∀L,T1. ∀R:predicate term. R T1 →
  28                 (∀T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → R T → R T2) →
  29                 ∀T2. L ⊢ T1 ⬌* T2 → R T2.
  30 #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
  31 qed-.
  32
  33 (* Basic properties *********************************************************)
  34
  35 (* Basic_1: was: pc3_refl *)
  36 lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T.
  37 /2 width=1/ qed.
  38
  39 lemma cpcs_strap1: ∀L,T1,T,T2.
  40                    L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
  41 /2 width=3/ qed.
  42
  43 lemma cpcs_strap2: ∀L,T1,T,T2.
  44                    L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
  45 /2 width=3/ qed.
  46
  47 (* Basic_1: removed theorems 1: clear_pc3_trans *)