]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc_new/lifts/lifts_neg.etc
small improvements and corrections ...
[helm.git] / 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-.