]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_pat_pat.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/arith/pnat_lt_pred.ma".
16 include "ground/relocation/pr_pat.ma".
17
18 (* POSITIVE APPLICATION FOR PARTIAL RELOCATION MAPS *************************)
19
20 (* Main constructions *******************************************************)
21
22 (*** at_monotonic *)
23 theorem pr_pat_monotonic:
24         ∀j2,i2,f. @❨i2,f❩ ≘ j2 → ∀j1,i1. @❨i1,f❩ ≘ j1 →
25         i1 < i2 → j1 < j2.
26 #j2 elim j2 -j2
27 [ #i2 #f #H2f elim (pr_pat_inv_unit_dx … H2f) -H2f //
28   #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi //
29 | #j2 #IH #i2 #f #H2f * //
30   #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi)
31   #_ #Hi2 elim (pr_pat_inv_succ_bi … H2f (↓i2)) -H2f [1,3: * |*: // ]
32   #g #H2g #H
33   [ elim (pr_pat_inv_push_succ … H1f … H) -f
34     /4 width=8 by plt_inv_succ_bi, plt_succ_bi/
35   | /4 width=8 by pr_pat_inv_next_succ, plt_succ_bi/
36   ]
37 ]
38 qed-.
39
40 (*** at_inv_monotonic *)
41 theorem pr_pat_inv_monotonic:
42         ∀j1,i1,f. @❨i1,f❩ ≘ j1 → ∀j2,i2. @❨i2,f❩ ≘ j2 →
43         j1 < j2 → i1 < i2.
44 #j1 elim j1 -j1
45 [ #i1 #f #H1f elim (pr_pat_inv_unit_dx … H1f) -H1f //
46   #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj
47   #H22 elim (pr_pat_inv_push_succ … H2f … (↓j2) H) -f //
48 | #j1 #IH *
49   [ #f #H1f elim (pr_pat_inv_unit_succ … H1f) -H1f [ |*: // ]
50     #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
51     /3 width=7 by pr_pat_inv_next_succ/
52   | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
53     #Hj #H22 elim (pr_pat_inv_succ_bi … H1f) -H1f [1,4: * |*: // ]
54     #g #Hg #H
55     [ elim (pr_pat_inv_push_succ … H2f … (↓j2) H) -f
56       /3 width=7 by plt_succ_bi/
57     | /3 width=7 by pr_pat_inv_next_succ/
58     ]
59   ]
60 ]
61 qed-.
62
63 (*** at_mono *)
64 theorem pr_pat_mono (f) (i):
65         ∀i1. @❨i,f❩ ≘ i1 → ∀i2. @❨i,f❩ ≘ i2 → i2 = i1.
66 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
67 #Hi elim (plt_ge_false i i)
68 /2 width=6 by pr_pat_inv_monotonic/
69 qed-.
70
71 (*** at_inj *)
72 theorem pr_pat_inj (f) (i):
73         ∀i1. @❨i1,f❩ ≘ i → ∀i2. @❨i2,f❩ ≘ i → i1 = i2.
74 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
75 #Hi elim (plt_ge_false i i)
76 /2 width=6 by pr_pat_monotonic/
77 qed-.
78
79 (*** at_div_comm *)
80 theorem pr_pat_div_comm (f2) (g2) (f1) (g1):
81         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div g2 f2 g1 f1.
82 #f2 #g2 #f1 #g1 #IH #jg #jf #j #Hg #Hf
83 elim (IH … Hf Hg) -IH -j /2 width=3 by ex2_intro/
84 qed-.
85
86 (*** at_div_pp *)
87 theorem pr_pat_div_push_bi (f2) (g2) (f1) (g1):
88         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (⫯f2) (⫯g2) (⫯f1) (⫯g1).
89 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
90 elim (pr_pat_inv_push … Hf) -Hf [1,2: * |*: // ]
91 [ #H1 #H2 destruct -IH
92   lapply (pr_pat_inv_push_unit … Hg ???) -Hg [4: |*: // ] #H destruct
93   /3 width=3 by pr_pat_refl, ex2_intro/
94 | #xf #i #Hf2 #H1 #H2 destruct
95   lapply (pr_pat_inv_push_succ … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
96   elim (IH … Hf2 Hg2) -IH -i /3 width=9 by pr_pat_push, ex2_intro/
97 ]
98 qed-.
99
100 (*** at_div_nn *)
101 theorem pr_pat_div_next_bi (f2) (g2) (f1) (g1):
102         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (↑f2) (↑g2) (f1) (g1).
103 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
104 elim (pr_pat_inv_next … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
105 lapply (pr_pat_inv_next_succ … Hg ????) -Hg [5: |*: // ] #Hg2
106 elim (IH … Hf2 Hg2) -IH -i /2 width=3 by ex2_intro/
107 qed-.
108
109 (*** at_div_np *)
110 theorem pr_pat_div_next_push (f2) (g2) (f1) (g1):
111         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (↑f2) (⫯g2) (f1) (↑g1).
112 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
113 elim (pr_pat_inv_next … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
114 lapply (pr_pat_inv_push_succ … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
115 elim (IH … Hf2 Hg2) -IH -i /3 width=7 by pr_pat_next, ex2_intro/
116 qed-.
117
118 (*** at_div_pn *)
119 theorem pr_pat_div_push_next (f2) (g2) (f1) (g1):
120         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (⫯f2) (↑g2) (↑f1) (g1).
121 /4 width=6 by pr_pat_div_next_push, pr_pat_div_comm/ qed-.