(* RELOCATION P-STREAM ******************************************************)
-definition gr_push: gr_map → gr_map ≝ λf. 𝟏⨮f.
-
-interpretation "push (pstream)" 'UpSpoon f = (gr_push f).
-
-definition gr_next: gr_map → gr_map.
-* #p #f @(↑p⨮f)
-defined.
-
-interpretation "next (pstream)" 'UpArrow f = (gr_next f).
-
-(* Basic properties *********************************************************)
-
-lemma gr_push_unfold: ∀f. 𝟏⨮f = ⫯f.
-// qed.
-
-lemma gr_next_unfold: ∀f,p. (↑p)⨮f = ↑(p⨮f).
-// qed.
-
(* Basic inversion lemmas ***************************************************)
lemma eq_inv_gr_push_bi: injective ? ? gr_push.
(* Basic inversions *********************************************************)
+(*** eq_inv_seq_aux *)
lemma stream_eq_inv_cons_bi (A):
∀t1,t2. t1 ≗{A} t2 →
∀u1,u2,b1,b2. b1⨮u1 = t1 → b2⨮u2 = t2 →
--- /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_ist.ma".
+include "ground/relocation/tr_pap_pat.ma".
+
+(* TOTAL RELOCATION MAPS ****************************************************)
+
+(* Constructions with pr_ist ************************************************)
+
+(*** at_istot *)
+lemma tr_ist (f): 𝐓❨𝐭❨f❩❩.
+/2 width=2 by ex_intro/ qed.
lemma tr_pap_succ (f):
∀p,i. f@❨i❩+p = (p⨮f)@❨↑i❩.
// qed.
-(*
-(*** apply_S2 *)
-lemma tr_pap_next (f):
- ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
-* #p #f * //
-qed.
-
-
-
-(*** apply_eq_repl *)
-lemma apply_eq_repl (i):
- ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩.
-
-
-(i): pr_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.
-
-
-(* 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-.
-
-(*
-include "ground/relocation/pstream_eq.ma".
-*)
-
-(*
-include "ground/relocation/rtmap_istot.ma".
-
-lemma at_istot: ∀f. 𝐓❨f❩.
-/2 width=2 by ex_intro/ qed.
-*)
-*)
\ No newline at end of file
--- /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/lib/stream_eq.ma".
+include "ground/relocation/tr_pap.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Main constructions with stream_eq ****************************************)
+
+(* Note: a better statement would be: tr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩) *)
+(*** apply_eq_repl *)
+theorem apply_eq_repl (i):
+ ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩.
+#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
+elim (stream_eq_inv_cons_bi … H) -H [1,8: |*: // ] #Hp #Hf //
+<tr_pap_succ <tr_pap_succ /3 width=1 by eq_f2/
+qed.
+
+(* Main inversions with stream_eq *******************************************)
+
+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 (𝟏)) <tr_pap_unit <tr_pap_unit #H destruct
+ lapply (Hf (↑i)) <tr_pap_succ <tr_pap_succ #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 *)
+(* *)
+(**************************************************************************)
+
+include "ground/relocation/tr_pap_pat.ma".
+
+(* Main inversions **********************************************************)
+
+(*** apply_inj *)
+theorem tr_pap_inj (f):
+ ∀i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+/2 width=4 by pr_pat_inj/ 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/tr_pn.ma".
+include "ground/relocation/tr_pap.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with tr_next ***********************************************)
+
+(*** apply_S2 *)
+lemma tr_pap_next (f):
+ ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
+* #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/relocation/tr_map.ma".
+
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
+
+definition tr_push: tr_map → tr_map ≝
+ λf. 𝟏⨮f.
+
+interpretation
+ "push (total relocation maps)"
+ 'UpSpoon f = (tr_push f).
+
+definition tr_next: tr_map → tr_map.
+* #p #f @(↑p⨮f)
+defined.
+
+interpretation
+ "next (total relocation maps)"
+ 'UpArrow f = (tr_next f).
+
+(* Basic constructions ******************************************************)
+
+lemma tr_push_unfold (f): 𝟏⨮f = ⫯f.
+// qed.
+
+lemma tr_next_unfold (f): ∀p. (↑p)⨮f = ↑(p⨮f).
+// qed.
+
+(* Constructions with tr_inj ************************************************)
+
+lemma tr_inj_push (f): ⫯𝐭❨f❩ = 𝐭❨⫯f❩.
+// qed.
+
+lemma tr_inj_next (f): ↑𝐭❨f❩ = 𝐭❨↑f❩.
+* //
+qed.
}
]
[ { "total relocation" * } {
- [ "tr_pap ( ?@❨?❩ )" * ]
- [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" * ]
+ [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
+ [ "tr_pn ( ⫯? ) ( ↑? )" * ]
+ [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
}
]
[ { "partial relocation" * } {
projects / helm.git / commitdiff