matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.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/relocation/gr_tl.ma".
  16
  17 (* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
  18
  19 (*** sle *)
  20 coinductive gr_sle: relation gr_map ≝
  21 (*** sle_push *)
  22 | gr_sle_push (f1) (f2) (g1) (g2):
  23   gr_sle f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → gr_sle g1 g2
  24 (*** sle_next *)
  25 | gr_sle_next (f1) (f2) (g1) (g2):
  26   gr_sle f1 f2 → ↑f1 = g1 → ↑f2 = g2 → gr_sle g1 g2
  27 (*** sle_weak *)
  28 | gr_sle_weak (f1) (f2) (g1) (g2):
  29   gr_sle f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → gr_sle g1 g2
  30 .
  31
  32 interpretation
  33   "inclusion (generic relocation maps)"
  34   'subseteq f1 f2 = (gr_sle f1 f2).
  35
  36 (* Basic constructions ******************************************************)
  37
  38 (*** sle_refl *)
  39 corec lemma gr_sle_refl:
  40             reflexive … gr_sle.
  41 #f cases (gr_map_split_tl f) #H
  42 [ @(gr_sle_push … H H) | @(gr_sle_next … H H) ] -H //
  43 qed.
  44
  45 (* Basic inversions *********************************************************)
  46
  47 (*** sle_inv_xp *)
  48 lemma gr_sle_inv_push_dx:
  49       ∀g1,g2. g1 ⊆ g2 → ∀f2. ⫯f2 = g2 →
  50       ∃∃f1. f1 ⊆ f2 & ⫯f1 = g1.
  51 #g1 #g2 * -g1 -g2
  52 #f1 #f2 #g1 #g2 #H #H1 #H2 #x2 #Hx2 destruct
  53 [ lapply (eq_inv_gr_push_bi … Hx2) -Hx2 /2 width=3 by ex2_intro/ ]
  54 elim (eq_inv_gr_push_next … Hx2)
  55 qed-.
  56
  57 (*** sle_inv_nx *)
  58 lemma gr_sle_inv_next_sn:
  59       ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 →
  60       ∃∃f2. f1 ⊆ f2 & ↑f2 = g2.
  61 #g1 #g2 * -g1 -g2
  62 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #Hx1 destruct
  63 [2: lapply (eq_inv_gr_next_bi … Hx1) -Hx1 /2 width=3 by ex2_intro/ ]
  64 elim (eq_inv_gr_next_push … Hx1)
  65 qed-.
  66
  67 (*** sle_inv_pn *)
  68 lemma gr_sle_inv_push_next:
  69       ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ⊆ f2.
  70 #g1 #g2 * -g1 -g2
  71 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
  72 [ elim (eq_inv_gr_next_push … Hx2)
  73 | elim (eq_inv_gr_push_next … Hx1)
  74 | lapply (eq_inv_gr_push_bi … Hx1) -Hx1
  75   lapply (eq_inv_gr_next_bi … Hx2) -Hx2 //
  76 ]
  77 qed-.
  78
  79 (* Advanced inversions ******************************************************)
  80
  81 (*** sle_inv_pp *)
  82 lemma gr_sle_inv_push_bi:
  83       ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
  84 #g1 #g2 #H #f1 #f2 #H1 #H2
  85 elim (gr_sle_inv_push_dx … H … H2) -g2 #x1 #H #Hx1 destruct
  86 lapply (eq_inv_gr_push_bi … Hx1) -Hx1 //
  87 qed-.
  88
  89 (*** sle_inv_nn *)
  90 lemma gr_sle_inv_next_bi:
  91       ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ⊆ f2.
  92 #g1 #g2 #H #f1 #f2 #H1 #H2
  93 elim (gr_sle_inv_next_sn … H … H1) -g1 #x2 #H #Hx2 destruct
  94 lapply (eq_inv_gr_next_bi … Hx2) -Hx2 //
  95 qed-.
  96
  97 (*** sle_inv_px *)
  98 lemma gr_sle_inv_push_sn:
  99       ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 →
 100       ∨∨ ∃∃f2. f1 ⊆ f2 & ⫯f2 = g2
 101        | ∃∃f2. f1 ⊆ f2 & ↑f2 = g2.
 102 #g1 #g2
 103 elim (gr_map_split_tl g2) #H2 #H #f1 #H1
 104 [ lapply (gr_sle_inv_push_bi … H … H1 H2)
 105 | lapply (gr_sle_inv_push_next … H … H1 H2)
 106 ] -H -H1
 107 /3 width=3 by ex2_intro, or_introl, or_intror/
 108 qed-.
 109
 110 (*** sle_inv_xn *)
 111 lemma gr_sle_inv_next_dx:
 112       ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 →
 113       ∨∨ ∃∃f1. f1 ⊆ f2 & ⫯f1 = g1
 114        | ∃∃f1. f1 ⊆ f2 & ↑f1 = g1.
 115 #g1 #g2
 116 elim (gr_map_split_tl g1) #H1 #H #f2 #H2
 117 [ lapply (gr_sle_inv_push_next … H … H1 H2)
 118 | lapply (gr_sle_inv_next_bi … H … H1 H2)
 119 ] -H -H2
 120 /3 width=3 by ex2_intro, or_introl, or_intror/
 121 qed-.
 122
 123 (* Constructions with gr_tl *************************************************)
 124
 125 (*** sle_px_tl *)
 126 lemma gr_sle_push_sn_tl:
 127       ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → f1 ⊆ ⫰g2.
 128 #g1 #g2 #H #f1 #H1
 129 elim (gr_sle_inv_push_sn … H … H1) -H -H1 * //
 130 qed.
 131
 132 (*** sle_xn_tl *)
 133 lemma gr_sle_next_dx_tl:
 134       ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → ⫰g1 ⊆ f2.
 135 #g1 #g2 #H #f2 #H2
 136 elim (gr_sle_inv_next_dx … H … H2) -H -H2 * //
 137 qed.
 138
 139 (*** sle_tl *)
 140 lemma gr_sle_tl:
 141       ∀f1,f2. f1 ⊆ f2 → ⫰f1 ⊆ ⫰f2.
 142 #f1 elim (gr_map_split_tl f1) #H1 #f2 #H
 143 [ lapply (gr_sle_push_sn_tl … H … H1) -H //
 144 | elim (gr_sle_inv_next_sn … H … H1) -H //
 145 ]
 146 qed.
 147
 148 (* Inversions with gr_tl ****************************************************)
 149
 150 (*** sle_inv_tl_sn *)
 151 lemma gr_sle_inv_tl_sn:
 152       ∀f1,f2. ⫰f1 ⊆ f2 → f1 ⊆ ↑f2.
 153 #f1 elim (gr_map_split_tl f1) #H #f2 #Hf12
 154 /2 width=5 by gr_sle_next, gr_sle_weak/
 155 qed-.
 156
 157 (*** sle_inv_tl_dx *)
 158 lemma gr_sle_inv_tl_dx:
 159       ∀f1,f2. f1 ⊆ ⫰f2 → ⫯f1 ⊆ f2.
 160 #f1 #f2 elim (gr_map_split_tl f2) #H #Hf12
 161 /2 width=5 by gr_sle_push, gr_sle_weak/
 162 qed-.