matita/matita/contribs/lambdadelta/basic_2/etc_new/lifts/lifts_neg.etc

   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/substitution/lift.ma".
  16
  17 (* BASIC TERM RELOCATION ****************************************************)
  18
  19 (* Properties on negated basic relocation ***********************************)
  20
  21 lemma nlift_lref_be_SO: ∀X,j. j < ∞ → ⬆[j, 1] X ≡ #j → ⊥.
  22 #X #j #Hj #H elim (lift_inv_lref2 … H) -H *
  23 [ #H elim (ylt_yle_false … H) -H //
  24 | #i #Hij #_ #H1 #H2 destruct
  25   elim (ylt_inv_plus_Y … Hj) -Hj #Hi #_
  26   elim (ylt_yle_false … Hij) -Hij /2 width=1 by monotonic_ylt_plus_sn/
  27 ]
  28 qed-.
  29
  30 lemma nlift_bind_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) →
  31                      ∀a,I,U. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
  32 #W #l #m #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
  33 qed-.
  34
  35 lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[⫯l, m] T ≡ U → ⊥) →
  36                      ∀a,I,W. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
  37 #U #l #m #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
  38 qed-.
  39
  40 lemma nlift_flat_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) →
  41                      ∀I,U. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥).
  42 #W #l #m #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
  43 qed-.
  44
  45 lemma nlift_flat_dx: ∀U,l,m. (∀T. ⬆[l, m] T ≡ U → ⊥) →
  46                      ∀I,W. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥).
  47 #U #l #m #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
  48 qed-.
  49
  50 (* Inversion lemmas on negated basic relocation *****************************)
  51
  52 lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → j = i ∧ j < ∞.
  53 #i #j elim (ylt_split_eq i j) #Hij #H destruct
  54 [ elim (H (#⫰j)) -H /2 width=1 by lift_lref_pred/
  55 | elim (yle_split_eq i (∞)) /2 width=1 by conj/ #H0 destruct
  56   elim (H (#∞)) -H /2 width=1 by lift_lref_plus, ylt_Y/
  57 | elim (H (#j)) -H /2 width=1 by lift_lref_lt/
  58 ]
  59 qed-.
  60
  61 lemma nlift_inv_bind: ∀a,I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥) →
  62                       (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[⫯l, m] T ≡ U → ⊥).
  63 #a #I #W #U #l #m #H elim (is_lift_dec W l m)
  64 [ * /4 width=2 by lift_bind, or_intror/
  65 | /4 width=2 by ex_intro, or_introl/
  66 ]
  67 qed-.
  68
  69 lemma nlift_inv_flat: ∀I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥) →
  70                       (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[l, m] T ≡ U → ⊥).
  71 #I #W #U #l #m #H elim (is_lift_dec W l m)
  72 [ * /4 width=2 by lift_flat, or_intror/
  73 | /4 width=2 by ex_intro, or_introl/
  74 ]
  75 qed-.