matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.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/isfinite_1.ma".
  16 include "ground_2/relocation/rtmap_fcla.ma".
  17
  18 (* RELOCATION MAP ***********************************************************)
  19
  20 definition isfin: predicate rtmap ≝
  21                   λf. ∃n. 𝐂⦃f⦄ ≘ n.
  22
  23 interpretation "test for finite colength (rtmap)"
  24    'IsFinite f = (isfin f).
  25
  26 (* Basic eliminators ********************************************************)
  27
  28 lemma isfin_ind (R:predicate rtmap): (∀f.  𝐈⦃f⦄ → R f) →
  29                                      (∀f. 𝐅⦃f⦄ → R f → R (⫯f)) →
  30                                      (∀f. 𝐅⦃f⦄ → R f → R (↑f)) →
  31                                      ∀f. 𝐅⦃f⦄ → R f.
  32 #R #IH1 #IH2 #IH3 #f #H elim H -H
  33 #n #H elim H -f -n /3 width=2 by ex_intro/
  34 qed-.
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  38 lemma isfin_inv_push: ∀g. 𝐅⦃g⦄ → ∀f. ⫯f = g → 𝐅⦃f⦄.
  39 #g * /3 width=4 by fcla_inv_px, ex_intro/
  40 qed-.
  41
  42 lemma isfin_inv_next: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
  43 #g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g
  44 /2 width=2 by ex_intro/
  45 qed-.
  46
  47 (* Basic properties *********************************************************)
  48
  49 lemma isfin_eq_repl_back: eq_repl_back … isfin.
  50 #f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
  51 qed-.
  52
  53 lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
  54 /3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
  55
  56 lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
  57 /3 width=2 by fcla_isid, ex_intro/ qed.
  58
  59 lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
  60 #f * /3 width=2 by fcla_push, ex_intro/
  61 qed.
  62
  63 lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
  64 #f * /3 width=2 by fcla_next, ex_intro/
  65 qed.
  66
  67 (* Properties with iterated push ********************************************)
  68
  69 lemma isfin_pushs: ∀n,f. 𝐅⦃f⦄ → 𝐅⦃⫯*[n]f⦄.
  70 #n elim n -n /3 width=3 by isfin_push/
  71 qed.
  72
  73 (* Inversion lemmas with iterated push **************************************)
  74
  75 lemma isfin_inv_pushs: ∀n,g. 𝐅⦃⫯*[n]g⦄ → 𝐅⦃g⦄.
  76 #n elim n -n /3 width=3 by isfin_inv_push/
  77 qed.
  78
  79 (* Properties with tail *****************************************************)
  80
  81 lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
  82 #f elim (pn_split f) * #g #H #Hf destruct
  83 /3 width=3 by isfin_inv_push, isfin_inv_next/
  84 qed.
  85
  86 (* Inversion lemmas with tail ***********************************************)
  87
  88 lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
  89 #f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
  90 qed-.
  91
  92 (* Inversion lemmas with iterated tail **************************************)
  93
  94 lemma isfin_inv_tls: ∀n,f. 𝐅⦃⫱*[n]f⦄ → 𝐅⦃f⦄.
  95 #n elim n -n /3 width=1 by isfin_inv_tl/
  96 qed-.