(* RELOCATION P-STREAM ******************************************************)
-definition gr_map: Type[0] ≝ stream pnat.
-
definition gr_push: gr_map → gr_map ≝ λf. 𝟏⨮f.
interpretation "push (pstream)" 'UpSpoon f = (gr_push 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 *)
-(* *)
-(**************************************************************************)
-
-include "ground/notation/functions/apply_2.ma".
-include "ground/arith/pnat_le_plus.ma".
-include "ground/relocation/pstream_eq.ma".
-include "ground/relocation/rtmap_istot.ma".
-
-(* RELOCATION P-STREAM ******************************************************)
-
-rec definition apply (i: pnat) on i: gr_map → pnat.
-* #p #f cases i -i
-[ @p
-| #i lapply (apply i f) -apply -i -f
- #i @(i+p)
-]
-defined.
-
-interpretation "functional application (nstream)"
- 'Apply f i = (apply i f).
-
-(* Properties on at (specific) ************************************************)
-
-lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2.
-#i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/
-qed.
-
-lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p.
-#p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/
-qed.
-
-lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
-#i1 elim i1 -i1
-[ * // | #i #IH * /3 width=1 by at_S1/ ]
-qed.
-
-lemma at_istot: ∀f. 𝐓❪f❫.
-/2 width=2 by ex_intro/ qed.
-
-lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q.
-#f #i1 #i #p #q #H elim q -q
-/2 width=5 by gr_pat_next/
-qed.
-
-(* Inversion lemmas on at (specific) ******************************************)
-
-lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2.
-#f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/
-#p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
-#j2 #Hj * -i2 /3 width=1 by eq_f/
-qed-.
-
-lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 →
- ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2.
-#f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/
-#p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
-#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
-#i2 #Hi * -j2 /2 width=3 by ex2_intro/
-qed-.
-
-lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
-/2 width=6 by fr2_nat_mono/ qed-.
-
-(* Forward lemmas on at (specific) *******************************************)
-
-lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2.
-#f #p *
-[ #i2 #H <(at_inv_O1 … H) -i2 //
-| #i1 #i2 #H elim (at_inv_S1 … H) -H
- #j1 #Ht * -i2 <pplus_succ_sn
- /4 width=2 by gr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
-]
-qed-.
-
-lemma at_fwd_id: ∀f,p,i. @❪i, p⨮f❫ ≘ i → 𝟏 = p.
-#f #p #i #H elim (gr_pat_des_id … H) -H
-#g #H elim (push_inv_seq_dx … H) -H //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma apply_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
-// qed.
-
-lemma apply_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
-// qed.
-
-lemma apply_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
-#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
-elim (eq_inv_seq_aux … H) -H #Hp #Hf //
->apply_S1 >apply_S1 /3 width=1 by eq_f2/
-qed.
-
-lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
-* #p #f * //
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
-/2 width=4 by gr_pat_inj/ qed-.
-
-corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
-* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
-[ @(Hf (𝟏))
-| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
- lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct
- lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
- /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
-]
-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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( 𝐭❨ break term 46 a ❩ )"
+ non associative with precedence 75
+ for @{ 'ElementT $a }.
"functional composition (partial relocation maps)"
'compose f2 f1 = (pr_compose f2 f1).
-(* Basic constructions (specific) *******************************************)
+(* Basic constructions ******************************************************)
lemma pr_compose_unfold_refl (f2) (f1): ⫯(f2∘f1) = (⫯f2)∘(⫯f1).
#f2 #f1
(* *)
(**************************************************************************)
-include "ground/relocation/pr_eq.ma".
+include "ground/relocation/pr_tl_eq.ma".
include "ground/relocation/pr_nexts.ma".
(* ITERATED NEXT FOR PARTIAL RELOCATION MAPS ********************************)
#n @(nat_ind_succ … n) -n
/3 width=5 by pr_eq_next/
qed.
+
+(* Inversions with pr_eq ****************************************************)
+
+lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
+ ↑*[n1] ⫯f1 ≡ ↑*[n2] ⫯f2 →
+ ∧∧ n1 = n2 & f1 ≡ f2.
+#f1 #f2
+#n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+[ <pr_nexts_zero <pr_nexts_succ #H
+ elim (pr_eq_inv_push_next … H) -H //
+| <pr_nexts_succ <pr_nexts_succ #H
+ lapply (pr_eq_inv_next_bi … H ????) -H [5:|*: // ] #H
+ elim (IH … H) -IH -H /2 width=1 by conj/
+| <pr_nexts_zero <pr_nexts_zero #H
+ lapply (pr_eq_inv_push_bi … H ????) -H [5:|*: // ] #H
+ /2 width=1 by conj/
+| <pr_nexts_succ <pr_nexts_zero #H
+ elim (pr_eq_inv_next_push … H) -H //
+]
+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/relocation/pr_nexts_eq.ma".
+include "ground/relocation/tr_nexts.ma".
+
+(* TOTAL RELOCATION MAPS ****************************************************)
+
+(* Constructions with pr_eq and stream_eq ***********************************)
+
+corec lemma eq_tr_inj_bi (f1) (f2): f1 ≗ f2 → 𝐭❨f1❩ ≡ 𝐭❨f2❩.
+* -f1 -f2 #p1 #p2 #f1 #f2 * -p2 #H
+cases p1 -p1
+[ @pr_eq_push /2 width=5 by/
+| #p @pr_eq_next [3:|*: //]
+ cases tr_inj_fold cases tr_inj_fold
+ /3 width=5 by stream_eq_cons/
+]
+qed.
+
+(* Inversions with pr_eq and stream_eq **************************************)
+
+corec lemma eq_inv_tr_inj_bi (f1) (f2): 𝐭❨f1❩ ≡ 𝐭❨f2❩ → f1 ≗ f2.
+cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
+cases tr_inj_unfold cases tr_inj_unfold #H
+cases (pr_eq_inv_nexts_push_bi … H) -H #H1 #H2
+@stream_eq_cons /2 width=1 by/
+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/notation/functions/element_t_1.ma".
+include "ground/relocation/pr_map.ma".
+include "ground/arith/pnat.ma".
+
+(* TOTAL RELOCATION MAPS ****************************************************)
+
+definition tr_map: Type[0] ≝ stream pnat.
+
+corec definition tr_inj: tr_map → pr_map.
+* *
+[ #f @(⫯(tr_inj f))
+| #p #f @(↑(tr_inj (p⨮f)))
+]
+defined.
+
+interpretation
+ "injection (total relocation maps)"
+ 'ElementT f = (tr_inj f).
+
+(* Basic constructions ******************************************************)
+
+lemma tr_inj_unfold_unit (f): ⫯𝐭❨f❩ = 𝐭❨𝟏⨮f❩.
+#f <(stream_unfold … (𝐭❨𝟏⨮f❩)) in ⊢ (???%); //
+qed.
+
+lemma tr_inj_unfold_succ (f): ∀p. ↑𝐭❨p⨮f❩ = 𝐭❨↑p⨮f❩.
+#f #p <(stream_unfold … (𝐭❨↑p⨮f❩)) in ⊢ (???%); //
+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/arith/nat_pred_succ.ma".
+include "ground/relocation/pr_nexts.ma".
+include "ground/relocation/tr_map.ma".
+
+(* TOTAL RELOCATION MAPS ****************************************************)
+
+(* Advanced constructions with pr_nexts *************************************)
+
+lemma tr_inj_unfold (f):
+ ∀p. ↑*[↓p]⫯𝐭❨f❩ = 𝐭❨p⨮f❩.
+#f #p elim p -p //
+qed.
+
+lemma tr_inj_fold (f):
+ ∀p. 𝐭❨p⨮f❩ = ↑*[↓p]⫯𝐭❨f❩.
+// 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/notation/functions/apply_2.ma".
+include "ground/relocation/tr_map.ma".
+(*
+include "ground/arith/pnat_le_plus.ma".
+include "ground/relocation/pstream_eq.ma".
+include "ground/relocation/rtmap_istot.ma".
+*)
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+rec definition tr_pat (i: pnat) on i: tr_map → pnat.
+* #p #f cases i -i
+[ @p
+| #i lapply (tr_pat i f) -tr_pat -i -f
+ #i @(i+p)
+]
+defined.
+
+interpretation
+ "functional positive application (total relocation maps)"
+ 'apply f i = (tr_pat i f).
+
+(* Properties on at (specific) ************************************************)
+
+lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2.
+#i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/
+qed.
+
+lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p.
+#p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/
+qed.
+
+lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
+#i1 elim i1 -i1
+[ * // | #i #IH * /3 width=1 by at_S1/ ]
+qed.
+
+lemma at_istot: ∀f. 𝐓❪f❫.
+/2 width=2 by ex_intro/ qed.
+
+lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q.
+#f #i1 #i #p #q #H elim q -q
+/2 width=5 by gr_pat_next/
+qed.
+
+(* Inversion lemmas on at (specific) ******************************************)
+
+lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2.
+#f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/
+#p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
+#j2 #Hj * -i2 /3 width=1 by eq_f/
+qed-.
+
+lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 →
+ ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2.
+#f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/
+#p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
+#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
+#i2 #Hi * -j2 /2 width=3 by ex2_intro/
+qed-.
+
+lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
+/2 width=6 by fr2_nat_mono/ qed-.
+
+(* Forward lemmas on at (specific) *******************************************)
+
+lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2.
+#f #p *
+[ #i2 #H <(at_inv_O1 … H) -i2 //
+| #i1 #i2 #H elim (at_inv_S1 … H) -H
+ #j1 #Ht * -i2 <pplus_succ_sn
+ /4 width=2 by gr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
+]
+qed-.
+
+lemma at_fwd_id: ∀f,p,i. @❪i, p⨮f❫ ≘ i → 𝟏 = p.
+#f #p #i #H elim (gr_pat_des_id … H) -H
+#g #H elim (push_inv_seq_dx … H) -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tr_pat_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
+// qed.
+
+lemma tr_pat_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
+// qed.
+
+lemma tr_pat_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
+elim (eq_inv_seq_aux … H) -H #Hp #Hf //
+>tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/
+qed.
+
+lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
+* #p #f * //
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+/2 width=4 by gr_pat_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
+[ @(Hf (𝟏))
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+ ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct
+ ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H
+ /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
+]
+qed-.
[ "fr2_map ( ◊ ) ( ❨?,?❩;? )" * ]
}
]
+ [ { "total relocation" * } {
+ [ "tr_map ( 𝐭❨?❩ )" "tr_nexts" "tr_eq" * ]
+ }
+ ]
[ { "partial relocation" * } {
[ "pr_sor ( ? ⋓ ? ≘ ? )" "pr_sor_eq" "pr_sor_tls" "pr_sor_isi" "pr_sor_fcla" "pr_sor_isf" "pr_sor_coafter_ist_isf" "pr_sor_sle" "pr_sor_sor" "pr_sor_sor_sle" * ]
[ "pr_sand ( ? ⋒ ? ≘ ? )" "pr_sand_eq" * ]
projects / helm.git / commitdiff