interpretation "nat predecessor" 'Predecessor m = (pred m).
+interpretation "nat min" 'and x y = (min x y).
+
+interpretation "nat max" 'or x y = (max x y).
+
(* Iota equations ***********************************************************)
lemma pred_O: pred 0 = 0.
lemma pred_S: ∀m. pred (S m) = m.
// qed.
+lemma max_O1: ∀n. n = (0 ∨ n).
+// qed.
+
+lemma max_O2: ∀n. n = (n ∨ 0).
+// qed.
+
+lemma max_SS: ∀n1,n2. ⫯(n1∨n2) = (⫯n1 ∨ ⫯n2).
+#n1 #n2 elim (decidable_le n1 n2) #H normalize
+[ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H //
+qed.
+
(* Equations ****************************************************************)
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
lemma lt_S: ∀n,m. n < m → n < ⫯m.
/2 width=1 by le_S/ qed.
+lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (⫯n1 ∨ n2) ≤ ⫯n.
+/4 width=2 by to_max, le_maxr, le_S_S, le_S/ qed-.
+
+lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ⫯n2) ≤ ⫯n.
+/2 width=1 by max_S1_le_S/ qed-.
+
lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐅 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsFinite $f }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐂 ⦃ term 46 f ⦄ ≡ break term 46 n )"
+ non associative with precedence 45
+ for @{ 'RCoLength $f $n }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/isfinite_1.ma".
+include "ground_2/relocation/rtmap_fcla.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+definition isfin: predicate rtmap ≝
+ λf. ∃n. 𝐂⦃f⦄ ≡ n.
+
+interpretation "test for finite colength (rtmap)"
+ 'IsFinite f = (isfin f).
+
+(* Basic properties *********************************************************)
+
+lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
+/3 width=2 by fcla_isid, ex_intro/ qed.
+
+lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
+#f * /3 width=2 by fcla_push, ex_intro/
+qed.
+
+lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
+#f * /3 width=2 by fcla_next, ex_intro/
+qed.
+
+lemma isfin_eq_repl_back: eq_repl_back … isfin.
+#f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
+qed-.
+
+lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
+/3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
+
+(* Basic eliminators ********************************************************)
+
+lemma isfin_ind (R:predicate rtmap): (∀f. 𝐈⦃f⦄ → R f) →
+ (∀f. 𝐅⦃f⦄ → R f → R (↑f)) →
+ (∀f. 𝐅⦃f⦄ → R f → R (⫯f)) →
+ ∀f. 𝐅⦃f⦄ → R f.
+#R #IH1 #IH2 #IH3 #f #H elim H -H
+#n #H elim H -f -n /3 width=2 by ex_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isfin_inv_next: ∀g. 𝐅⦃g⦄ → ∀f. ⫯f = g → 𝐅⦃f⦄.
+#g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g
+/2 width=2 by ex_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma isfin_fwd_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
+#g * /3 width=4 by fcla_inv_px, ex_intro/
+qed-.
(**************************************************************************)
include "ground_2/notation/relations/runion_3.ma".
+include "ground_2/relocation/rtmap_isfin.ma".
include "ground_2/relocation/rtmap_sle.ma".
coinductive sor: relation3 rtmap rtmap rtmap ≝
/2 width=3 by ex2_intro/
qed-.
+(* Main inversion lemmas ****************************************************)
+
+corec theorem sor_mono: ∀f1,f2,x,y. f1 ⋓ f2 ≡ x → f1 ⋓ f2 ≡ y → x ≗ y.
+#f1 #f2 #x #y * -f1 -f2 -x
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
+[ cases (sor_inv_ppx … H … H1 H2)
+| cases (sor_inv_npx … H … H1 H2)
+| cases (sor_inv_pnx … H … H1 H2)
+| cases (sor_inv_nnx … H … H1 H2)
+] -g1 -g2
+/3 width=5 by eq_push, eq_next/
+qed-.
+
(* Basic properties *********************************************************)
corec lemma sor_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋓ f2 ≡ f).
#f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
[ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
qed-.
+
+(* Properies on identity ****************************************************)
+
+corec lemma sor_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⋓ f2 ≡ f2.
+#f1 * -f1
+#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
+/3 width=7 by sor_pp, sor_pn/
+qed.
+
+corec lemma sor_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⋓ f2 ≡ f1.
+#f2 * -f2
+#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
+/3 width=7 by sor_pp, sor_np/
+qed.
+
+(* Properties on finite colength assignment *********************************)
+
+lemma sor_fcla_ex: ∀f1,n1. 𝐂⦃f1⦄ ≡ n1 → ∀f2,n2. 𝐂⦃f2⦄ ≡ n2 →
+ ∃∃f,n. f1 ⋓ f2 ≡ f & 𝐂⦃f⦄ ≡ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
+#f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/
+#f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1
+[ /3 width=7 by fcla_push, sor_pp, ex4_2_intro/
+| /3 width=7 by fcla_next, sor_pn, max_S2_le_S, le_S_S, ex4_2_intro/
+| /3 width=7 by fcla_next, sor_np, max_S1_le_S, le_S_S, ex4_2_intro/
+| /4 width=7 by fcla_next, sor_nn, le_S, le_S_S, ex4_2_intro/
+]
+qed-.
+
+lemma sor_fcla: ∀f1,n1. 𝐂⦃f1⦄ ≡ n1 → ∀f2,n2. 𝐂⦃f2⦄ ≡ n2 → ∀f. f1 ⋓ f2 ≡ f →
+ ∃∃n. 𝐂⦃f⦄ ≡ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
+#f1 #n1 #Hf1 #f2 #n2 #Hf2 #f #Hf elim (sor_fcla_ex … Hf1 … Hf2) -Hf1 -Hf2
+/4 width=6 by sor_mono, fcla_eq_repl_back, ex3_intro/
+qed-.
+
+(* Properties on test for finite colength ***********************************)
+
+lemma sor_isfin_ex: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∃∃f. f1 ⋓ f2 ≡ f & 𝐅⦃f⦄.
+#f1 #f2 * #n1 #H1 * #n2 #H2 elim (sor_fcla_ex … H1 … H2) -H1 -H2
+/3 width=4 by ex2_intro, ex_intro/
+qed-.
+
+lemma sor_isfin: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∀f. f1 ⋓ f2 ≡ f → 𝐅⦃f⦄.
+#f1 #f2 #Hf1 #Hf2 #f #Hf elim (sor_isfin_ex … Hf1 … Hf2) -Hf1 -Hf2
+/3 width=6 by sor_mono, isfin_eq_repl_back/
+qed-.
class "grass"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
- [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+ [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
+ [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
[ { "" * } {
[ "stream ( ? @ ? )" "stream_eq ( ? ≐ ? )" "stream_hdtl ( ↓? )" "stream_tls ( ↓*[?]? )" * ]
[ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
- [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" * ]
+ [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
[ "star" "lstar" * ]
}
]
projects / helm.git / commitdiff