]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_tl_eq.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/pr_eq.ma".
16 include "ground/relocation/pr_tl.ma".
17
18 (* TAIL FOR PARTIAL RELOCATION MAPS *****************************************)
19
20 (* Constructions with pr_eq *************************************************)
21
22 (*** eq_refl *)
23 corec lemma pr_eq_refl: reflexive … pr_eq.
24 #f cases (pr_map_split_tl f) #Hf
25 [ @(pr_eq_push … Hf Hf) | @(pr_eq_next … Hf Hf) ] -Hf //
26 qed.
27
28 (*** tl_eq_repl *)
29 lemma pr_tl_eq_repl:
30       pr_eq_repl … (λf1,f2. ⫰f1 ≡ ⫰f2).
31 #f1 #f2 * -f1 -f2 //
32 qed.
33
34 (* Inversions with pr_eq ****************************************************)
35
36 (*** eq_inv_gen *)
37 lemma pr_eq_inv_gen (g1) (g2):
38       g1 ≡ g2 →
39       ∨∨ ∧∧ ⫰g1 ≡ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
40        | ∧∧ ⫰g1 ≡ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
41 #g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
42 /3 width=1 by and3_intro, or_introl, or_intror/
43 qed-.
44
45 (* Advanced inversions with pr_eq *******************************************)
46
47 (*** pr_eq_inv_px *)
48 lemma pr_eq_inv_push_sn (g1) (g2):
49       g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
50       ∧∧ f1 ≡ ⫰g2 & ⫯⫰g2 = g2.
51 #g1 #g2 #H #f1 #Hf1
52 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
53 [ /2 width=1 by conj/
54 | elim (eq_inv_pr_next_push … Hg1)
55 ]
56 qed-.
57
58 (*** pr_eq_inv_nx *)
59 lemma pr_eq_inv_next_sn (g1) (g2):
60       g1 ≡ g2 → ∀f1. ↑f1 = g1 →
61       ∧∧ f1 ≡ ⫰g2 & ↑⫰g2 = g2.
62 #g1 #g2 #H #f1 #Hf1
63 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
64 [ elim (eq_inv_pr_push_next … Hg1)
65 | /2 width=1 by conj/
66 ]
67 qed-.
68
69 (*** pr_eq_inv_xp *)
70 lemma pr_eq_inv_push_dx (g1) (g2):
71       g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
72       ∧∧ ⫰g1 ≡ f2 & ⫯⫰g1 = g1.
73 #g1 #g2 #H #f2 #Hf2
74 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
75 [ /2 width=1 by conj/
76 | elim (eq_inv_pr_next_push … Hg2)
77 ]
78 qed-.
79
80 (*** pr_eq_inv_xn *)
81 lemma pr_eq_inv_next_dx (g1) (g2):
82       g1 ≡ g2 → ∀f2. ↑f2 = g2 →
83       ∧∧ ⫰g1 ≡ f2 & ↑⫰g1 = g1.
84 #g1 #g2 #H #f2 #Hf2
85 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
86 [ elim (eq_inv_pr_push_next … Hg2)
87 | /2 width=1 by conj/
88 ]
89 qed-.
90
91 (*** pr_eq_inv_pp *)
92 lemma pr_eq_inv_push_bi (g1) (g2):
93       g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≡ f2.
94 #g1 #g2 #H #f1 #f2 #H1
95 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
96 lapply (eq_inv_pr_push_bi … H) -H //
97 qed-.
98
99 (*** pr_eq_inv_nn *)
100 lemma pr_eq_inv_next_bi (g1) (g2):
101       g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≡ f2.
102 #g1 #g2 #H #f1 #f2 #H1
103 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
104 lapply (eq_inv_pr_next_bi … H) -H //
105 qed-.
106
107 (*** pr_eq_inv_pn *)
108 lemma pr_eq_inv_push_next (g1) (g2):
109       g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
110 #g1 #g2 #H #f1 #f2 #H1
111 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
112 elim (eq_inv_pr_next_push … H)
113 qed-.
114
115 (*** pr_eq_inv_np *)
116 lemma pr_eq_inv_next_push (g1) (g2):
117       g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
118 #g1 #g2 #H #f1 #f2 #H1
119 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
120 elim (eq_inv_pr_push_next … H)
121 qed-.