1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/notation/functions/element_t_1.ma".
16 include "ground/relocation/pr_map.ma".
17 include "ground/arith/pnat.ma".
19 (* TOTAL RELOCATION MAPS ****************************************************)
21 definition tr_map: Type[0] ≝ stream pnat.
23 corec definition tr_inj: tr_map → pr_map.
26 | #p #f @(↑(tr_inj (p⨮f)))
31 "injection (total relocation maps)"
32 'ElementT f = (tr_inj f).
34 (* Basic constructions ******************************************************)
36 lemma tr_inj_unfold_unit (f): ⫯𝐭❨f❩ = 𝐭❨𝟏⨮f❩.
37 #f <(stream_unfold … (𝐭❨𝟏⨮f❩)) in ⊢ (???%); //
40 lemma tr_inj_unfold_succ (f): ∀p. ↑𝐭❨p⨮f❩ = 𝐭❨↑p⨮f❩.
41 #f #p <(stream_unfold … (𝐭❨↑p⨮f❩)) in ⊢ (???%); //
44 (* Basic inversions *********************************************************)
46 (*** push_inv_seq_sn *)
47 lemma eq_inv_cons_pr_push (f) (g):
48 ∀p. 𝐭❨p⨮g❩ = ⫯f → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
51 /3 width=1 by eq_inv_pr_push_bi, conj/
52 | #p <tr_inj_unfold_succ #H
53 elim (eq_inv_pr_next_push … H)
57 (*** push_inv_seq_dx *)
58 lemma eq_inv_pr_push_cons (f) (g):
59 ∀p. ⫯f = 𝐭❨p⨮g❩ → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
62 /3 width=1 by eq_inv_pr_push_bi, conj/
63 | #p <tr_inj_unfold_succ #H
64 elim (eq_inv_pr_push_next … H)
68 (*** next_inv_seq_sn *)
69 lemma eq_inv_cons_pr_next (f) (g):
70 ∀p. 𝐭❨p⨮g❩ = ↑f → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
72 [ <tr_inj_unfold_unit #H
73 elim (eq_inv_pr_push_next … H)
74 | #p <tr_inj_unfold_succ #H
75 /3 width=3 by eq_inv_pr_next_bi, ex2_intro/
79 (*** next_inv_seq_dx *)
80 lemma eq_inv_pr_next_cons (f) (g):
81 ∀p. ↑f = 𝐭❨p⨮g❩ → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
83 [ <tr_inj_unfold_unit #H
84 elim (eq_inv_pr_next_push … H)
85 | #p <tr_inj_unfold_succ #H
86 /3 width=3 by eq_inv_pr_next_bi, ex2_intro/