rtmaps with finite colength

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_fcla.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
new file mode 100644 (file)
index 0000000..14542cf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rcolength_2.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+inductive fcla: relation2 rtmap nat ≝
+| fcla_isid: ∀f. 𝐈⦃f⦄ → fcla f 0
+| fcla_push: ∀f,n. fcla f n → fcla (↑f) n
+| fcla_next: ∀f,n. fcla f n → fcla (⫯f) (⫯n)
+.
+
+interpretation "finite colength assignment (rtmap)"
+   'RCoLength f n = (fcla f n).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fcla_inv_px: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ↑f = g → 𝐂⦃f⦄ ≡ m.
+#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
+#g #m #_ #f #H elim (discr_push_next … H)
+qed-.
+
+lemma fcla_inv_nx: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ⫯f = g →
+                   ∃∃n. 𝐂⦃f⦄ ≡ n & ⫯n = m.
+#g #m * -g -m /2 width=3 by ex2_intro/
+[ #g #Hg #f #H elim (isid_inv_next …  H) -H //
+| #g #m #_ #f #H elim (discr_next_push … H)
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cla_inv_nn: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f,n. ⫯f = g → ⫯n = m → 𝐂⦃f⦄ ≡ n.
+#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx … H … H1) -g
+#x #Hf #H destruct //
+qed-.
+
+lemma cla_inv_np: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ⫯f = g → 0 = m → ⊥.
+#g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g
+#x #_ #H1 #H2 destruct
+qed-.
+
+lemma fcla_inv_xp: ∀g,m. 𝐂⦃g⦄ ≡ m → 0 = m → 𝐈⦃g⦄.
+#g #m #H elim H -g -m /3 width=3 by isid_push/
+#g #m #_ #_ #H destruct
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fcla_eq_repl_back: ∀n. eq_repl_back … (λf. 𝐂⦃f⦄ ≡ n).
+#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
+#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H
+/3 width=3 by fcla_push, fcla_next/
+qed-.
+
+lemma fcla_eq_repl_fwd: ∀n. eq_repl_fwd … (λf. 𝐂⦃f⦄ ≡ n).
+#n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/
+qed-.