matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.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_2/notation/relations/rcolength_2.ma".
  16 include "ground_2/relocation/rtmap_isid.ma".
  17
  18 (* RELOCATION MAP ***********************************************************)
  19
  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)
  24 .
  25
  26 interpretation "finite colength assignment (rtmap)"
  27    'RCoLength f n = (fcla f n).
  28
  29 (* Basic inversion lemmas ***************************************************)
  30
  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)
  34 qed-.
  35
  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)
  41 ]
  42 qed-.
  43
  44 (* Advanced inversion lemmas ************************************************)
  45
  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
  48 #x #Hf #H destruct //
  49 qed-.
  50
  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
  54 qed-.
  55
  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
  59 qed-.
  60
  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 //
  64 qed-.
  65
  66 (* Main forward lemmas ******************************************************)
  67
  68 theorem fcla_mono: ∀f,n1. 𝐂❪f❫ ≘ n1 → ∀n2. 𝐂❪f❫ ≘ n2 → n1 = n2.
  69 #f #n #H elim H -f -n
  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/
  74 ]
  75 qed-.
  76
  77 (* Basic properties *********************************************************)
  78
  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/
  83 qed-.
  84
  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/
  87 qed-.