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/upspoon_1.ma".
16 include "ground/notation/functions/uparrow_1.ma".
17 include "ground/lib/stream.ma".
18 include "ground/lib/bool.ma".
20 (* GENERIC RELOCATION MAPS **************************************************)
23 definition gr_map: Type[0] ≝ stream bool.
26 definition gr_push (f): gr_map ≝ Ⓕ⨮f.
29 "push (generic relocation maps)"
30 'UpSpoon f = (gr_push f).
33 definition gr_next (f): gr_map ≝ Ⓣ⨮f.
36 "next (generic relocation maps)"
37 'UpArrow f = (gr_next f).
39 (* Basic constructions (specific) *******************************************)
42 lemma gr_push_unfold (f): Ⓕ⨮f = ⫯f.
46 lemma gr_next_unfold (f): Ⓣ⨮f = ↑f.
49 (* Basic inversions *********************************************************)
51 (*** injective_push *)
52 lemma eq_inv_gr_push_bi: injective ? ? gr_push.
53 #f1 #f2 <gr_push_unfold <gr_push_unfold #H destruct //
56 (*** discr_push_next *)
57 lemma eq_inv_gr_push_next (f1) (f2): ⫯f1 = ↑f2 → ⊥.
58 #f1 #f2 <gr_push_unfold <gr_next_unfold #H destruct
61 (*** discr_next_push *)
62 lemma eq_inv_gr_next_push (f1) (f2): ↑f1 = ⫯f2 → ⊥.
63 #f1 #f2 <gr_next_unfold <gr_push_unfold #H destruct
66 (*** injective_next *)
67 lemma eq_inv_gr_next_bi: injective ? ? gr_next.
68 #f1 #f2 <gr_next_unfold <gr_next_unfold #H destruct //