matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj.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/notation/relations/parallel_2.ma".
  16 include "ground/relocation/gr_tl.ma".
  17
  18 (* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
  19
  20 (*** sdj *)
  21 coinductive gr_sdj: relation gr_map ≝
  22 (*** sdj_pp *)
  23 | gr_sdj_push_bi (f1) (f2) (g1) (g2):
  24   gr_sdj f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → gr_sdj g1 g2
  25 (*** sdj_np *)
  26 | gr_sdj_next_push (f1) (f2) (g1) (g2):
  27   gr_sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → gr_sdj g1 g2
  28 (*** sdj_pn *)
  29 | gr_sdj_push_next (f1) (f2) (g1) (g2):
  30   gr_sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → gr_sdj g1 g2
  31 .
  32
  33 interpretation
  34   "disjointness (generic relocation maps)"
  35   'Parallel f1 f2 = (gr_sdj f1 f2).
  36
  37 (* Basic constructions ******************************************************)
  38
  39 (*** sdj_sym *)
  40 corec lemma gr_sdj_sym:
  41             symmetric … gr_sdj.
  42 #f1 #f2 * -f1 -f2
  43 #f1 #f2 #g1 #g2 #Hf #H1 #H2
  44 [ @(gr_sdj_push_bi … H2 H1)
  45 | @(gr_sdj_push_next … H2 H1)
  46 | @(gr_sdj_next_push … H2 H1)
  47 ] -g2 -g1
  48 /2 width=1 by/
  49 qed-.
  50
  51 (* Basic inversions *********************************************************)
  52
  53 (*** sdj_inv_pp *)
  54 lemma gr_sdj_inv_push_bi:
  55       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
  56 #g1 #g2 * -g1 -g2
  57 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
  58 [ lapply (eq_inv_gr_push_bi … Hx1) -Hx1
  59   lapply (eq_inv_gr_push_bi … Hx2) -Hx2 //
  60 | elim (eq_inv_gr_push_next … Hx1)
  61 | elim (eq_inv_gr_push_next … Hx2)
  62 ]
  63 qed-.
  64
  65 (*** sdj_inv_np *)
  66 lemma gr_sdj_inv_next_push:
  67       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
  68 #g1 #g2 * -g1 -g2
  69 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
  70 [ elim (eq_inv_gr_next_push … Hx1)
  71 | lapply (eq_inv_gr_next_bi … Hx1) -Hx1
  72   lapply (eq_inv_gr_push_bi … Hx2) -Hx2 //
  73 | elim (eq_inv_gr_push_next … Hx2)
  74 ]
  75 qed-.
  76
  77 (*** sdj_inv_pn *)
  78 lemma gr_sdj_inv_push_next:
  79       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
  80 #g1 #g2 * -g1 -g2
  81 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
  82 [ elim (eq_inv_gr_next_push … Hx2)
  83 | elim (eq_inv_gr_push_next … Hx1)
  84 | lapply (eq_inv_gr_push_bi … Hx1) -Hx1
  85   lapply (eq_inv_gr_next_bi … Hx2) -Hx2 //
  86 ]
  87 qed-.
  88
  89 (*** sdj_inv_nn *)
  90 lemma gr_sdj_inv_next_bi:
  91       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → ⊥.
  92 #g1 #g2 * -g1 -g2
  93 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
  94 [ elim (eq_inv_gr_next_push … Hx1)
  95 | elim (eq_inv_gr_next_push … Hx2)
  96 | elim (eq_inv_gr_next_push … Hx1)
  97 ]
  98 qed-.
  99
 100 (* Advanced inversions ******************************************************)
 101
 102 (*** sdj_inv_nx *)
 103 lemma gr_sdj_inv_next_sn:
 104       ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
 105       ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
 106 #g1 #g2 elim (gr_map_split_tl g2) #H2 #H #f1 #H1
 107 [ lapply (gr_sdj_inv_next_push … H … H1 H2) -H /2 width=3 by ex2_intro/
 108 | elim (gr_sdj_inv_next_bi … H … H1 H2)
 109 ]
 110 qed-.
 111
 112 (*** sdj_inv_xn *)
 113 lemma gr_sdj_inv_next_dx:
 114       ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
 115       ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
 116 #g1 #g2 elim (gr_map_split_tl g1) #H1 #H #f2 #H2
 117 [ lapply (gr_sdj_inv_push_next … H … H1 H2) -H /2 width=3 by ex2_intro/
 118 | elim (gr_sdj_inv_next_bi … H … H1 H2)
 119 ]
 120 qed-.
 121
 122 (*** sdj_inv_xp *)
 123 lemma gr_sdj_inv_push_dx:
 124       ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
 125       ∨∨ ∃∃f1. f1 ∥ f2 & ⫯f1 = g1
 126        | ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
 127 #g1 #g2 elim (gr_map_split_tl g1) #H1 #H #f2 #H2
 128 [ lapply (gr_sdj_inv_push_bi … H … H1 H2)
 129 | lapply (gr_sdj_inv_next_push … H … H1 H2)
 130 ] -H -H2
 131 /3 width=3 by ex2_intro, or_introl, or_intror/
 132 qed-.
 133
 134 (*** sdj_inv_px *)
 135 lemma gr_sdj_inv_push_sn:
 136       ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
 137       ∨∨ ∃∃f2. f1 ∥ f2 & ⫯f2 = g2
 138        | ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
 139 #g1 #g2 elim (gr_map_split_tl g2) #H2 #H #f1 #H1
 140 [ lapply (gr_sdj_inv_push_bi … H … H1 H2)
 141 | lapply (gr_sdj_inv_push_next … H … H1 H2)
 142 ] -H -H1
 143 /3 width=3 by ex2_intro, or_introl, or_intror/
 144 qed-.