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_2/notation/relations/rcolength_2.ma".
16 include "ground_2/relocation/rtmap_isid.ma".
18 (* RELOCATION MAP ***********************************************************)
20 inductive fcla: relation2 rtmap nat ā
21 | fcla_isid: āf. šā¦fā¦ ā fcla f 0
22 | fcla_push: āf,n. fcla f n ā fcla (ā«Æf) n
23 | fcla_next: āf,n. fcla f n ā fcla (āf) (ān)
26 interpretation "finite colength assignment (rtmap)"
27 'RCoLength f n = (fcla f n).
29 (* Basic inversion lemmas ***************************************************)
31 lemma fcla_inv_px: āg,m. šā¦gā¦ ā m ā āf. ā«Æf = g ā šā¦fā¦ ā m.
32 #g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
33 #g #m #_ #f #H elim (discr_push_next ā¦ H)
36 lemma fcla_inv_nx: āg,m. šā¦gā¦ ā m ā āf. āf = g ā
37 āān. šā¦fā¦ ā n & ān = m.
38 #g #m * -g -m /2 width=3 by ex2_intro/
39 [ #g #Hg #f #H elim (isid_inv_next ā¦ H) -H //
40 | #g #m #_ #f #H elim (discr_next_push ā¦ H)
44 (* Advanced inversion lemmas ************************************************)
46 lemma cla_inv_nn: āg,m. šā¦gā¦ ā m ā āf,n. āf = g ā ān = m ā šā¦fā¦ ā n.
47 #g #m #H #f #n #H1 #H2 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
51 lemma cla_inv_np: āg,m. šā¦gā¦ ā m ā āf. āf = g ā 0 = m ā ā„.
52 #g #m #H #f #H1 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
53 #x #_ #H1 #H2 destruct
56 lemma fcla_inv_xp: āg,m. šā¦gā¦ ā m ā 0 = m ā šā¦gā¦.
57 #g #m #H elim H -g -m /3 width=3 by isid_push/
58 #g #m #_ #_ #H destruct
61 lemma fcla_inv_isid: āf,n. šā¦fā¦ ā n ā šā¦fā¦ ā 0 = n.
62 #f #n #H elim H -f -n /3 width=3 by isid_inv_push/
63 #f #n #_ #_ #H elim (isid_inv_next ā¦ H) -H //
66 (* Main forward lemmas ******************************************************)
68 theorem fcla_mono: āf,n1. šā¦fā¦ ā n1 ā ān2. šā¦fā¦ ā n2 ā n1 = n2.
70 [ /2 width=3 by fcla_inv_isid/
71 | /3 width=3 by fcla_inv_px/
72 | #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx ā¦ H) -H [2,3 : // ]
73 #g #Hf #H destruct /3 width=1 by eq_f/
77 (* Basic properties *********************************************************)
79 lemma fcla_eq_repl_back: ān. eq_repl_back ā¦ (Ī»f. šā¦fā¦ ā n).
80 #n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
81 #f1 #n #_ #IH #g2 #H [ elim (eq_inv_px ā¦ H) | elim (eq_inv_nx ā¦ H) ] -H
82 /3 width=3 by fcla_push, fcla_next/
85 lemma fcla_eq_repl_fwd: ān. eq_repl_fwd ā¦ (Ī»f. šā¦fā¦ ā n).
86 #n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/