matita/matita/contribs/lambdadelta/static_2/relocation/seq.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 "static_2/notation/relations/ideqsn_3.ma".
  16 include "static_2/syntax/teq_ext.ma".
  17 include "static_2/relocation/sex.ma".
  18
  19 (* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************)
  20
  21 (* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *)
  22 definition seq: relation3 rtmap lenv lenv ≝
  23            sex ceq_ext cfull.
  24
  25 interpretation
  26   "syntactic equivalence on selected entries (local environment)"
  27   'IdEqSn f L1 L2 = (seq f L1 L2).
  28
  29 (* Basic properties *********************************************************)
  30
  31 lemma seq_eq_repl_back:
  32       ∀L1,L2. eq_repl_back … (λf. L1 ≡[f] L2).
  33 /2 width=3 by sex_eq_repl_back/ qed-.
  34
  35 lemma seq_eq_repl_fwd:
  36       ∀L1,L2. eq_repl_fwd … (λf. L1 ≡[f] L2).
  37 /2 width=3 by sex_eq_repl_fwd/ qed-.
  38
  39 lemma sle_seq_trans:
  40       ∀f2,L1,L2. L1 ≡[f2] L2 →
  41       ∀f1. f1 ⊆ f2 → L1 ≡[f1] L2.
  42 /2 width=3 by sle_sex_trans/ qed-.
  43
  44 (* Basic_2A1: includes: lreq_refl *)
  45 lemma seq_refl (f):
  46       reflexive … (seq f).
  47 /2 width=1 by sex_refl/ qed.
  48
  49 (* Basic_2A1: includes: lreq_sym *)
  50 lemma seq_sym (f):
  51       symmetric … (seq f).
  52 /3 width=1 by sex_sym, ceq_ext_sym/ qed-.
  53
  54 (* Basic inversion lemmas ***************************************************)
  55
  56 (* Basic_2A1: includes: lreq_inv_atom1 *)
  57 lemma seq_inv_atom1 (f):
  58       ∀Y. ⋆ ≡[f] Y → Y = ⋆.
  59 /2 width=4 by sex_inv_atom1/ qed-.
  60
  61 (* Basic_2A1: includes: lreq_inv_pair1 *)
  62 lemma seq_inv_next1 (g):
  63       ∀J,K1,Y. K1.ⓘ[J] ≡[↑g] Y →
  64       ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ[J].
  65 #g #J #K1 #Y #H
  66 elim (sex_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct
  67 <(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/
  68 qed-.
  69
  70 (* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *)
  71 lemma seq_inv_push1 (g):
  72       ∀J1,K1,Y. K1.ⓘ[J1] ≡[⫯g] Y →
  73       ∃∃J2,K2. K1 ≡[g] K2 & Y = K2.ⓘ[J2].
  74 #g #J1 #K1 #Y #H elim (sex_inv_push1 … H) -H /2 width=4 by ex2_2_intro/
  75 qed-.
  76
  77 (* Basic_2A1: includes: lreq_inv_atom2 *)
  78 lemma seq_inv_atom2 (f):
  79       ∀X. X ≡[f] ⋆ → X = ⋆.
  80 /2 width=4 by sex_inv_atom2/ qed-.
  81
  82 (* Basic_2A1: includes: lreq_inv_pair2 *)
  83 lemma seq_inv_next2 (g):
  84       ∀J,X,K2. X ≡[↑g] K2.ⓘ[J] →
  85       ∃∃K1. K1 ≡[g] K2 & X = K1.ⓘ[J].
  86 #g #J #X #K2 #H
  87 elim (sex_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct
  88 <(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/
  89 qed-.
  90
  91 (* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *)
  92 lemma seq_inv_push2 (g):
  93       ∀J2,X,K2. X ≡[⫯g] K2.ⓘ[J2] →
  94       ∃∃J1,K1. K1 ≡[g] K2 & X = K1.ⓘ[J1].
  95 #g #J2 #X #K2 #H elim (sex_inv_push2 … H) -H /2 width=4 by ex2_2_intro/
  96 qed-.
  97
  98 (* Basic_2A1: includes: lreq_inv_pair *)
  99 lemma seq_inv_next (f):
 100       ∀I1,I2,L1,L2. L1.ⓘ[I1] ≡[↑f] L2.ⓘ[I2] →
 101       ∧∧ L1 ≡[f] L2 & I1 = I2.
 102 #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next … H) -H
 103 /3 width=3 by ceq_ext_inv_eq, conj/
 104 qed-.
 105
 106 (* Basic_2A1: includes: lreq_inv_succ *)
 107 lemma seq_inv_push (f):
 108       ∀I1,I2,L1,L2. L1.ⓘ[I1] ≡[⫯f] L2.ⓘ[I2] → L1 ≡[f] L2.
 109 #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push … H) -H /2 width=1 by conj/
 110 qed-.
 111
 112 lemma seq_inv_tl (f):
 113       ∀I,L1,L2. L1 ≡[⫰f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
 114 /2 width=1 by sex_inv_tl/ qed-.
 115
 116 (* Basic_2A1: removed theorems 5:
 117               lreq_pair_lt lreq_succ_lt lreq_pair_O_Y lreq_O2 lreq_inv_O_Y
 118 *)