(* RELOCATION MAP ***********************************************************)
coinductive at: rtmap → relation nat ≝
-| at_refl: â\88\80f,g,j1,j2. â\86\91f = g → 0 = j1 → 0 = j2 → at g j1 j2
-| at_push: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j1,j2. â\86\91f = g â\86\92 ⫯i1 = j1 â\86\92 ⫯i2 = j2 → at g j1 j2
-| at_next: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j2. ⫯f = g â\86\92 ⫯i2 = j2 → at g i1 j2
+| at_refl: â\88\80f,g,j1,j2. ⫯f = g → 0 = j1 → 0 = j2 → at g j1 j2
+| at_push: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j1,j2. ⫯f = g â\86\92 â\86\91i1 = j1 â\86\92 â\86\91i2 = j2 → at g j1 j2
+| at_next: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j2. â\86\91f = g â\86\92 â\86\91i2 = j2 → at g i1 j2
.
interpretation "relational application (rtmap)"
(* Basic inversion lemmas ***************************************************)
-lemma at_inv_ppx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. 0 = i1 â\86\92 â\86\91g = f → 0 = i2.
+lemma at_inv_ppx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. 0 = i1 â\86\92 ⫯g = f → 0 = i2.
#f #i1 #i2 * -f -i1 -i2 //
[ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
| #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
]
qed-.
-lemma at_inv_npx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g,j1. ⫯j1 = i1 â\86\92 â\86\91g = f →
- â\88\83â\88\83j2. @â¦\83j1, gâ¦\84 â\89\98 j2 & ⫯j2 = i2.
+lemma at_inv_npx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g,j1. â\86\91j1 = i1 â\86\92 ⫯g = f →
+ â\88\83â\88\83j2. @â¦\83j1, gâ¦\84 â\89\98 j2 & â\86\91j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
| #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma at_inv_xnx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. ⫯g = f →
- â\88\83â\88\83j2. @â¦\83i1, gâ¦\84 â\89\98 j2 & ⫯j2 = i2.
+lemma at_inv_xnx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. â\86\91g = f →
+ â\88\83â\88\83j2. @â¦\83i1, gâ¦\84 â\89\98 j2 & â\86\91j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
| #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
(* Advanced inversion lemmas ************************************************)
lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80g,j2. 0 = i1 â\86\92 â\86\91g = f â\86\92 ⫯j2 = i2 → ⊥.
+ â\88\80g,j2. 0 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
#H destruct
qed-.
lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80g,j1. ⫯j1 = i1 â\86\92 â\86\91g = f → 0 = i2 → ⊥.
+ â\88\80g,j1. â\86\91j1 = i1 â\86\92 ⫯g = f → 0 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct
qed-.
lemma at_inv_npn: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80g,j1,j2. ⫯j1 = i1 â\86\92 â\86\91g = f â\86\92 ⫯j2 = i2 → @⦃j1, g⦄ ≘ j2.
+ â\88\80g,j1,j2. â\86\91j1 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 → @⦃j1, g⦄ ≘ j2.
#f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct //
qed-.
lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80g. ⫯g = f → 0 = i2 → ⊥.
+ â\88\80g. â\86\91g = f → 0 = i2 → ⊥.
#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct
qed-.
lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80g,j2. ⫯g = f â\86\92 ⫯j2 = i2 → @⦃i1, g⦄ ≘ j2.
+ â\88\80g,j2. â\86\91g = f â\86\92 â\86\91j2 = i2 → @⦃i1, g⦄ ≘ j2.
#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct //
qed-.
-lemma at_inv_pxp: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 0 = i1 â\86\92 0 = i2 â\86\92 â\88\83g. â\86\91g = f.
+lemma at_inv_pxp: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 0 = i1 â\86\92 0 = i2 â\86\92 â\88\83g. ⫯g = f.
#f elim (pn_split … f) * /2 width=2 by ex_intro/
#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
qed-.
-lemma at_inv_pxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j2. 0 = i1 â\86\92 ⫯j2 = i2 →
- â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & ⫯g = f.
+lemma at_inv_pxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j2. 0 = i1 â\86\92 â\86\91j2 = i2 →
+ â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & â\86\91g = f.
#f elim (pn_split … f) *
#g #H #i1 #i2 #Hf #j2 #H1 #H2
[ elim (at_inv_ppn … Hf … H1 H H2)
qed-.
lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 →
- â\88\80j1. ⫯j1 = i1 → 0 = i2 → ⊥.
+ â\88\80j1. â\86\91j1 = i1 → 0 = i2 → ⊥.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #j1 #H1 #H2
[ elim (at_inv_npp … Hf … H1 H H2)
]
qed-.
-lemma at_inv_nxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j1,j2. ⫯j1 = i1 â\86\92 ⫯j2 = i2 →
- (â\88\83â\88\83g. @â¦\83j1, gâ¦\84 â\89\98 j2 & â\86\91g = f) ∨
- â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & ⫯g = f.
+lemma at_inv_nxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j1,j2. â\86\91j1 = i1 â\86\92 â\86\91j2 = i2 →
+ (â\88\83â\88\83g. @â¦\83j1, gâ¦\84 â\89\98 j2 & ⫯g = f) ∨
+ â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & â\86\91g = f.
#f elim (pn_split f) *
/4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
qed-.
(* Note: the following inversion lemmas must be checked *)
-lemma at_inv_xpx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. â\86\91g = f →
+lemma at_inv_xpx: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. ⫯g = f →
(0 = i1 ∧ 0 = i2) ∨
- â\88\83â\88\83j1,j2. @â¦\83j1, gâ¦\84 â\89\98 j2 & ⫯j1 = i1 & ⫯j2 = i2.
+ â\88\83â\88\83j1,j2. @â¦\83j1, gâ¦\84 â\89\98 j2 & â\86\91j1 = i1 & â\86\91j2 = i2.
#f * [2: #i1 ] #i2 #Hf #g #H
[ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
| >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
]
qed-.
-lemma at_inv_xpp: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. â\86\91g = f → 0 = i2 → 0 = i1.
+lemma at_inv_xpp: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g. ⫯g = f → 0 = i2 → 0 = i1.
#f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
#j1 #j2 #_ #_ * -i2 #H destruct
qed-.
-lemma at_inv_xpn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g,j2. â\86\91g = f â\86\92 ⫯j2 = i2 →
- â\88\83â\88\83j1. @â¦\83j1, gâ¦\84 â\89\98 j2 & ⫯j1 = i1.
+lemma at_inv_xpn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80g,j2. ⫯g = f â\86\92 â\86\91j2 = i2 →
+ â\88\83â\88\83j1. @â¦\83j1, gâ¦\84 â\89\98 j2 & â\86\91j1 = i1.
#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f *
[ #_ * -i2 #H destruct
| #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
qed-.
lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → 0 = i2 →
- â\88\83â\88\83g. 0 = i1 & â\86\91g = f.
+ â\88\83â\88\83g. 0 = i1 & ⫯g = f.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #H2
[ /3 width=6 by at_inv_xpp, ex2_intro/
]
qed-.
-lemma at_inv_xxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j2. ⫯j2 = i2 →
- (â\88\83â\88\83g,j1. @â¦\83j1, gâ¦\84 â\89\98 j2 & ⫯j1 = i1 & â\86\91g = f) ∨
- â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & ⫯g = f.
+lemma at_inv_xxn: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\88\80j2. â\86\91j2 = i2 →
+ (â\88\83â\88\83g,j1. @â¦\83j1, gâ¦\84 â\89\98 j2 & â\86\91j1 = i1 & ⫯g = f) ∨
+ â\88\83â\88\83g. @â¦\83i1, gâ¦\84 â\89\98 j2 & â\86\91g = f.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #j2 #H2
[ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
]
qed-.
-lemma at_increasing_strict: â\88\80g,i1,i2. @â¦\83i1, gâ¦\84 â\89\98 i2 â\86\92 â\88\80f. ⫯f = g →
- i1 < i2 â\88§ @â¦\83i1, fâ¦\84 â\89\98 â«°i2.
+lemma at_increasing_strict: â\88\80g,i1,i2. @â¦\83i1, gâ¦\84 â\89\98 i2 â\86\92 â\88\80f. â\86\91f = g →
+ i1 < i2 â\88§ @â¦\83i1, fâ¦\84 â\89\98 â\86\93i2.
#g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
/4 width=2 by conj, at_increasing, le_S_S/
qed-.
-lemma at_fwd_id_ex: â\88\80f,i. @â¦\83i, fâ¦\84 â\89\98 i â\86\92 â\88\83g. â\86\91g = f.
+lemma at_fwd_id_ex: â\88\80f,i. @â¦\83i, fâ¦\84 â\89\98 i â\86\92 â\88\83g. ⫯g = f.
#f elim (pn_split f) * /2 width=2 by ex_intro/
#g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
qed-.
theorem at_div_pp: ∀f2,g2,f1,g1.
- H_at_div f2 g2 f1 g1 â\86\92 H_at_div (â\86\91f2) (â\86\91g2) (â\86\91f1) (â\86\91g1).
+ H_at_div f2 g2 f1 g1 â\86\92 H_at_div (⫯f2) (⫯g2) (⫯f1) (⫯g1).
#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
elim (at_inv_xpx … Hf) -Hf [1,2: * |*: // ]
[ #H1 #H2 destruct -IH
qed-.
theorem at_div_nn: ∀f2,g2,f1,g1.
- H_at_div f2 g2 f1 g1 â\86\92 H_at_div (⫯f2) (⫯g2) (f1) (g1).
+ H_at_div f2 g2 f1 g1 â\86\92 H_at_div (â\86\91f2) (â\86\91g2) (f1) (g1).
#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
lapply (at_inv_xnn … Hg ????) -Hg [5: |*: // ] #Hg2
qed-.
theorem at_div_np: ∀f2,g2,f1,g1.
- H_at_div f2 g2 f1 g1 â\86\92 H_at_div (⫯f2) (â\86\91g2) (f1) (⫯g1).
+ H_at_div f2 g2 f1 g1 â\86\92 H_at_div (â\86\91f2) (⫯g2) (f1) (â\86\91g1).
#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
lapply (at_inv_xpn … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
qed-.
theorem at_div_pn: ∀f2,g2,f1,g1.
- H_at_div f2 g2 f1 g1 â\86\92 H_at_div (â\86\91f2) (⫯g2) (⫯f1) (g1).
+ H_at_div f2 g2 f1 g1 â\86\92 H_at_div (⫯f2) (â\86\91g2) (â\86\91f1) (g1).
/4 width=6 by at_div_np, at_div_comm/ qed-.
(* Properties on tls ********************************************************)
<tls_xn /2 width=1 by/
qed.
-lemma at_tls: â\88\80i2,f. â\86\91⫱*[⫯i2]f â\89\97 ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≘ i2.
+lemma at_tls: â\88\80i2,f. ⫯⫱*[â\86\91i2]f â\89¡ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≘ i2.
#i2 elim i2 -i2
[ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
| #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
(* Inversion lemmas with tls ************************************************)
-lemma at_inv_nxx: â\88\80n,g,i1,j2. @â¦\83⫯i1, g⦄ ≘ j2 → @⦃0, g⦄ ≘ n →
- â\88\83â\88\83i2. @â¦\83i1, ⫱*[⫯n]gâ¦\84 â\89\98 i2 & ⫯(n+i2) = j2.
+lemma at_inv_nxx: â\88\80n,g,i1,j2. @â¦\83â\86\91i1, g⦄ ≘ j2 → @⦃0, g⦄ ≘ n →
+ â\88\83â\88\83i2. @â¦\83i1, ⫱*[â\86\91n]gâ¦\84 â\89\98 i2 & â\86\91(n+i2) = j2.
#n elim n -n
[ #g #i1 #j2 #Hg #H
elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
]
qed-.
-lemma at_inv_tls: â\88\80i2,i1,f. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 â\86\91⫱*[⫯i2]f â\89\97 ⫱*[i2]f.
+lemma at_inv_tls: â\88\80i2,i1,f. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 ⫯⫱*[â\86\91i2]f â\89¡ ⫱*[i2]f.
#i2 elim i2 -i2
[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
/2 width=1 by eq_refl/
(* Advanced properties on id ************************************************)
-lemma id_inv_at: â\88\80f. (â\88\80i. @â¦\83i, fâ¦\84 â\89\98 i) â\86\92 ð\9d\90\88ð\9d\90\9d â\89\97 f.
+lemma id_inv_at: â\88\80f. (â\88\80i. @â¦\83i, fâ¦\84 â\89\98 i) â\86\92 ð\9d\90\88ð\9d\90\9d â\89¡ f.
/3 width=1 by isid_at, eq_id_inv_isid/ qed-.
lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≘ i.