rec definition flifts f U on U ≝ match U with
[ TAtom I ⇒ match I with
[ Sort _ ⇒ U
- | LRef i ⇒ #(f@❨i❩)
+ | LRef i ⇒ #(f＠⧣❨i❩)
| GRef _ ⇒ U
]
| TPair I V T ⇒ match I with
(* Basic properties *********************************************************)
-lemma flifts_lref (f) (i): ↑*[f](#i) = #(f@❨i❩).
+lemma flifts_lref (f) (i): ↑*[f](#i) = #(f＠⧣❨i❩).
// qed.
lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ[p,I]V.T) = ⓑ[p,I]↑*[f]V.↑*[⫯f]T.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( @ break term 71 u . break term 70 t )"
+notation "hvbox( ＠ break term 71 u . break term 70 t )"
non associative with precedence 70
for @{ 'At $u $t }.
definition dfr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃∃b,n.
let r ≝ p●𝗔◗b●𝗟◗q in
- ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+ ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)＠⧣❨n❩ & r◖𝗱n ϵ t1 &
t1[⋔r←𝛗(n+♭b).(t1⋔(p◖𝗦))] ⇔ t2
.
(* COMMENT
axiom pippo (b) (q) (n):
- ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
- ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
+ ↑❘q❘ = (↑[q]𝐢)＠⧣❨n❩ →
+ ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)＠⧣❨n+❘b❘❩.
lemma unwind_rmap_tls_eq_id (p) (n):
- ❘p❘ = ↑[p]𝐢@❨n❩ →
+ ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
(𝐢) ≗ ⇂*[n]↑[p]𝐢.
#p @(list_ind_rcons … p) -p
[ #n <depth_empty #H destruct
]
-(* (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
+(* (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩ *)
+(* [↑[p]𝐢＠⧣❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
lemma unwind_rmap_tls_eq (f) (p) (n):
- ❘p❘ = ↑[p]𝐢@❨n❩ →
+ ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
f ≗ ⇂*[n]↑[p]f.
#f #p #n #Hp
@(stream_eq_canc_dx … (stream_tls_eq_repl …))
]
(*
-Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢@❨n❩
+Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n❩
---------------------------
-↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢@❨n+❘b❘❩❩] t
+↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩❩] t
*)
(*
(↑[𝐮❨↑❘q❘❩]▼[⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢](t1⋔(p◖𝗦))⇔▼[𝐮❨↑❘q❘❩∘▼[p●𝗔◗b●𝗟◗q]𝐢](t1⋔(p◖𝗦))
definition ifr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃∃b,n.
let r ≝ p●𝗔◗b●𝗟◗q in
- ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+ ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)＠⧣❨n❩ & r◖𝗱n ϵ t1 &
t1[⋔r←↑[𝐮❨♭(b●𝗟◗q)❩](t1⋔(p◖𝗦))] ⇔ t2
.
[ list_empty ⇒ k f (𝐞)
| list_lcons l q ⇒
match l with
- [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q
+ [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f＠⧣❨n❩)◗p)) (⇂*[n]f) q
| label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
| label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
| label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
// qed.
lemma lift_d_sn (A) (k) (p) (n) (f):
- ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
+ ↑❨(λg,p. k g (𝗱(f＠⧣❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
// qed.
lemma lift_m_sn (A) (k) (p) (f):
// qed.
lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
- ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩+↑[p]f@❨n❩.
+ ↑[p]f＠⧣❨m+n❩ = ↑[p◖𝗱n]f＠⧣❨m❩+↑[p]f＠⧣❨n❩.
// qed.
qed.
lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
- (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
+ (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
@(ex2_intro … (𝗱n◗𝗺◗r))
/2 width=1 by in_comp_iref/
qed-.
lemma lift_iref_dx (f) (t) (n:pnat):
- ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t.
+ ↑[f](𝛗n.t) ⊆ 𝛗f＠⧣❨n❩.↑[⇂*[n]f]t.
#f #t #n #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
/3 width=1 by in_comp_iref, in_comp_lift_bi/
qed-.
lemma lift_iref (f) (t) (n:pnat):
- (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
+ (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
/3 width=1 by conj, lift_iref_sn, lift_iref_dx/
qed.
qed.
lemma lift_path_d_sn (f) (p) (n):
- (𝗱(f@❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
+ (𝗱(f＠⧣❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
// qed.
lemma lift_path_m_sn (f) (p):
qed.
definition tr_nap (f) (l:nat): nat ≝
- ↓(f@❨↑l❩).
+ ↓(f＠⧣❨↑l❩).
interpretation
"functional non-negative application (total relocation maps)"
'ApplySucc f l = (tr_nap f l).
lemma tr_nap_unfold (f) (l):
- ↓(f@❨↑l❩) = f@↑❨l❩.
+ ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
// qed.
lemma tr_compose_nap (f2) (f1) (l):
match l with
[ label_d n ⇒
match q with
- [ list_empty ⇒ 𝗱((f n)@❨n❩)◗(unwind_gen f q)
+ [ list_empty ⇒ 𝗱((f n)＠⧣❨n❩)◗(unwind_gen f q)
| list_lcons _ _ ⇒ unwind_gen f q
]
| label_m ⇒ unwind_gen f q
// qed.
lemma unwind_gen_d_empty (f) (n):
- 𝗱((f n)@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
+ 𝗱((f n)＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
// qed.
lemma unwind_gen_d_lcons (f) (p) (l) (n):
(* Properties with tr_compose ***********************************************)
lemma unwind_gen_after (f2) (f1) (p):
- ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p.
+ ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)＠⧣❨n❩))∘(f1 n)]p.
#f2 #f1 #p @(path_ind_unwind … p) -p //
#n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
qed.
(* Advanced constructions with list_rcons ***********************************)
lemma unwind_gen_d_empty_dx (n) (p) (f):
- (⊗p)◖𝗱((f n)@❨n❩) = ◆[f](p◖𝗱n).
+ (⊗p)◖𝗱((f n)＠⧣❨n❩) = ◆[f](p◖𝗱n).
#n #p #f <unwind_gen_append_proper_dx //
qed.
lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
(𝗱k◗q) = ◆[f]p →
- ∃∃r,h. 𝐞 = ⊗r & (f h)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+ ∃∃r,h. 𝐞 = ⊗r & (f h)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
#k #q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_gen_empty #H destruct
match l with
[ label_d n ⇒
match q with
- [ list_empty ⇒ unwind_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐮❨f@❨n❩❩) q
- | list_lcons _ _ ⇒ unwind_gen (A) k (𝐮❨f@❨n❩❩) q
+ [ list_empty ⇒ unwind_gen (A) (λg,p. k g (𝗱(f＠⧣❨n❩)◗p)) (𝐮❨f＠⧣❨n❩❩) q
+ | list_lcons _ _ ⇒ unwind_gen (A) k (𝐮❨f＠⧣❨n❩❩) q
]
| label_m ⇒ unwind_gen (A) k f q
| label_L ⇒ unwind_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
// qed.
lemma unwind_d_empty (A) (k) (n) (f):
- ▼❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐮❨f@❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
+ ▼❨(λg,p. k g (𝗱(f＠⧣❨n❩)◗p)), 𝐮❨f＠⧣❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
// qed.
lemma unwind_d_lcons (A) (k) (p) (l) (n) (f):
- ▼❨k, 𝐮❨f@❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
+ ▼❨k, 𝐮❨f＠⧣❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
// qed.
lemma unwind_m_sn (A) (k) (p) (f):
// qed.
lemma unwind_path_d_empty (f) (n):
- 𝗱(f@❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
+ 𝗱(f＠⧣❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
// qed.
lemma unwind_path_d_lcons (f) (p) (l) (n):
- ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
+ ▼[𝐮❨f＠⧣❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
// qed.
lemma unwind_path_m_sn (f) (p):
// qed.
lemma unwind_rmap_d_sn (f) (p) (n):
- ▼[p](𝐮❨f@❨n❩❩) = ▼[𝗱n◗p]f.
+ ▼[p](𝐮❨f＠⧣❨n❩❩) = ▼[𝗱n◗p]f.
#f * // qed.
lemma unwind_rmap_m_sn (f) (p):
(* Advanced constructions with proj_rmap and path_rcons *********************)
lemma unwind_rmap_d_dx (f) (p) (n):
- (𝐮❨(▼[p]f)@❨n❩❩) = ▼[p◖𝗱n]f.
+ (𝐮❨(▼[p]f)＠⧣❨n❩❩) = ▼[p◖𝗱n]f.
// qed.
lemma unwind_rmap_m_dx (f) (p):
// qed.
lemma unwind_rmap_pap_d_dx (f) (p) (n) (m):
- ▼[p]f@❨n❩+m = ▼[p◖𝗱n]f@❨m❩.
+ ▼[p]f＠⧣❨n❩+m = ▼[p◖𝗱n]f＠⧣❨m❩.
#f #p #n #m
<unwind_rmap_d_dx <tr_uni_pap <pplus_comm //
qed.
(* UNWIND FOR PROTOTERM *****************************************************)
lemma unwind_iref_sn (f) (t:prototerm) (n:pnat):
- ▼[𝐮❨f@❨n❩❩]t ⊆ ▼[f](𝛗n.t).
+ ▼[𝐮❨f＠⧣❨n❩❩]t ⊆ ▼[f](𝛗n.t).
#f #t #n #p * #q #Hq #H0 destruct
@(ex2_intro … (𝗱n◗𝗺◗q))
/2 width=1 by in_comp_iref/
qed-.
lemma unwind_iref_dx (f) (t) (n:pnat):
- ▼[f](𝛗n.t) ⊆ ▼[𝐮❨f@❨n❩❩]t.
+ ▼[f](𝛗n.t) ⊆ ▼[𝐮❨f＠⧣❨n❩❩]t.
#f #t #n #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
/2 width=1 by in_comp_unwind_bi/
qed-.
lemma unwind_iref (f) (t) (n:pnat):
- ▼[𝐮❨f@❨n❩❩]t ⇔ ▼[f](𝛗n.t).
+ ▼[𝐮❨f＠⧣❨n❩❩]t ⇔ ▼[f](𝛗n.t).
/3 width=1 by conj, unwind_iref_sn, unwind_iref_dx/
qed.
qed.
lemma unwind_rmap_pap_le (f) (p) (n):
- n < ▼❘p❘ → (▼[p]𝐢)@❨n❩ = (▼[p]f)@❨n❩.
+ n < ▼❘p❘ → (▼[p]𝐢)＠⧣❨n❩ = (▼[p]f)＠⧣❨n❩.
#f #p #n #Hn
>(tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …))
<tr_compose_pap <tr_pap_pushs_le //
(* Advanced constructions with proj_path ************************************)
lemma unwind_path_d_empty_dx (n) (p) (f):
- (⊗p)◖𝗱((▼[p]f)@❨n❩) = ▼[f](p◖𝗱n).
+ (⊗p)◖𝗱((▼[p]f)＠⧣❨n❩) = ▼[f](p◖𝗱n).
#n #p #f <unwind_append_proper_dx //
qed.
lemma unwind_path_inv_d_sn (k) (q) (p) (f):
(𝗱k◗q) = ▼[f]p →
- ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+ ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
#k #q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
lemma unwind_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
ninj (m+⧣p+l) = ❘p❘ →
- (▼[p]f1)@❨m❩ = (▼[p]f2)@❨m❩.
+ (▼[p]f1)＠⧣❨m❩ = (▼[p]f2)＠⧣❨m❩.
#f1 #f2 #p @(list_ind_rcons … p) -p
[ #m #l <depth_empty #H0 destruct
| #p * [ #n ] #IH #m #l
qed.
lemma unwind_rmap_pap_gt (f) (p) (m):
- f@❨m+⧣p❩+❘p❘ = (▼[p]f)@❨m+❘p❘❩.
+ f＠⧣❨m+⧣p❩+❘p❘ = (▼[p]f)＠⧣❨m+❘p❘❩.
#f #p @(list_ind_rcons … p) -p [ // ]
#p * [ #n ] #IH #m
[ <update_d_dx <depth_d_dx
(* GROUND NOTATION **********************************************************)
-notation "hvbox( f @❨ break term 46 a ❩ )"
+notation "hvbox( f ＠❨ break term 46 a ❩ )"
non associative with precedence 60
for @{ 'Apply $f $a }.
--- /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( f ＠⧣❨ break term 46 a ❩ )"
+ non associative with precedence 60
+ for @{ 'AtSharp $f $a }.
+++ /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( @❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RAt $T1 $f $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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( ＠⧣❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RAtSharp $T1 $f $T2 }.
(* *)
(**************************************************************************)
-include "ground/notation/relations/rat_3.ma".
+include "ground/notation/relations/ratsucc_3.ma".
include "ground/arith/nat_plus.ma".
include "ground/arith/nat_lt.ma".
include "ground/relocation/fr2_map.ma".
interpretation
"non-negative relational application (finite relocation maps with pairs)"
- 'RAt l1 f l2 = (fr2_nat f l1 l2).
+ 'RAtSucc l1 f l2 = (fr2_nat f l1 l2).
(* Basic inversions *********************************************************)
(*** at_inv_nil *)
lemma fr2_nat_inv_empty (l1) (l2):
- @❨l1, 𝐞❩ ≘ l2 → l1 = l2.
+ @â\86\91â\9d¨l1, ð\9d\90\9eâ\9d© â\89\98 l2 â\86\92 l1 = l2.
#l1 #l2 @(insert_eq_1 … (𝐞))
#f * -f -l1 -l2
[ //
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2):
- @❨l1, ❨d,h❩◗f❩ ≘ l2 →
- ∨∨ ∧∧ l1 < d & @❨l1, f❩ ≘ l2
- | ∧∧ d ≤ l1 & @❨l1+h, f❩ ≘ l2.
+ @â\86\91â\9d¨l1, â\9d¨d,hâ\9d©â\97\97fâ\9d© â\89\98 l2 â\86\92
+ â\88¨â\88¨ â\88§â\88§ l1 < d & @â\86\91â\9d¨l1, fâ\9d© â\89\98 l2
+ | â\88§â\88§ d â\89¤ l1 & @â\86\91â\9d¨l1+h, fâ\9d© â\89\98 l2.
#g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g))
#f * -f -l1 -l2
[ #l #H destruct
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2):
- @â\9d¨l1, â\9d¨d,hâ\9d©â\97\97fâ\9d© â\89\98 l2 â\86\92 l1 < d â\86\92 @❨l1, f❩ ≘ l2.
+ @â\86\91â\9d¨l1, â\9d¨d,hâ\9d©â\97\97fâ\9d© â\89\98 l2 â\86\92 l1 < d â\86\92 @â\86\91❨l1, f❩ ≘ l2.
#f #d #h #l1 #h2 #H
elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d
elim (nlt_ge_false … Hl1d Hdl1)
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2):
- @â\9d¨l1, â\9d¨d,hâ\9d©â\97\97fâ\9d© â\89\98 l2 â\86\92 d â\89¤ l1 â\86\92 @❨l1+h, f❩ ≘ l2.
+ @â\86\91â\9d¨l1, â\9d¨d,hâ\9d©â\97\97fâ\9d© â\89\98 l2 â\86\92 d â\89¤ l1 â\86\92 @â\86\91❨l1+h, f❩ ≘ l2.
#f #d #h #l1 #h2 #H
elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1
elim (nlt_ge_false … Hl1d Hdl1)
(*** at_mono *)
theorem fr2_nat_mono (f) (l):
- â\88\80l1. @â\9d¨l, fâ\9d© â\89\98 l1 â\86\92 â\88\80l2. @❨l, f❩ ≘ l2 → l1 = l2.
+ â\88\80l1. @â\86\91â\9d¨l, fâ\9d© â\89\98 l1 â\86\92 â\88\80l2. @â\86\91❨l, f❩ ≘ l2 → l1 = l2.
#f #l #l1 #H elim H -f -l -l1
[ #l #x #H <(fr2_nat_inv_empty … H) -x //
| #f #d #h #l #l1 #Hld #_ #IH #x #H
(*** after_inj_O_aux *)
corec fact pr_after_inj_unit_aux:
- ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1.
+ ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1.
#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [|*: // ] #g1 #H1
lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
(*** after_inj_aux *)
fact pr_after_inj_aux:
- (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1) →
- ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_after_inj f1.
+ (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1) →
+ ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_after_inj f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [|*: // ] #g1 #H1g1 #H1
(*** after_at1_fwd *)
lemma pr_after_des_ist_pat:
- ∀f1,i1,i2. @❨i1, f1❩ ≘ i2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
- ∃∃i. @❨i2, f2❩ ≘ i & @❨i1, f❩ ≘ i.
+ ∀f1,i1,i2. ＠⧣❨i1, f1❩ ≘ i2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
+ ∃∃i. ＠⧣❨i2, f2❩ ≘ i & ＠⧣❨i1, f❩ ≘ i.
#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
/3 width=8 by pr_after_des_pat, ex2_intro/
qed-.
(*** after_at_fwd *)
lemma pr_after_pat_des (i) (i1):
- ∀f. @❨i1, f❩ ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
- ∃∃i2. @❨i1, f1❩ ≘ i2 & @❨i2, f2❩ ≘ i.
+ ∀f. ＠⧣❨i1, f❩ ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
+ ∃∃i2. ＠⧣❨i1, f1❩ ≘ i2 & ＠⧣❨i2, f2❩ ≘ i.
#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
[ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3:* |*: // ]
[1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
(*** after_fwd_at *)
lemma pr_after_des_pat (i) (i2) (i1):
- ∀f1,f2. @❨i1, f1❩ ≘ i2 → @❨i2, f2❩ ≘ i →
- ∀f. f2 ⊚ f1 ≘ f → @❨i1, f❩ ≘ i.
+ ∀f1,f2. ＠⧣❨i1, f1❩ ≘ i2 → ＠⧣❨i2, f2❩ ≘ i →
+ ∀f. f2 ⊚ f1 ≘ f → ＠⧣❨i1, f❩ ≘ i.
#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
[ elim (pr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
#g2 [ #j2 ] #Hg2 [ #H22 ] #H20
(*** after_fwd_at2 *)
lemma pr_after_des_pat_sn (i1) (i):
- ∀f. @❨i1, f❩ ≘ i → ∀f1,i2. @❨i1, f1❩ ≘ i2 →
- ∀f2. f2 ⊚ f1 ≘ f → @❨i2, f2❩ ≘ i.
+ ∀f. ＠⧣❨i1, f❩ ≘ i → ∀f1,i2. ＠⧣❨i1, f1❩ ≘ i2 →
+ ∀f2. f2 ⊚ f1 ≘ f → ＠⧣❨i2, f2❩ ≘ i.
#i1 #i #f #Hf #f1 #i2 #Hf1 #f2 #H elim (pr_after_pat_des … Hf … H) -f
#j1 #H #Hf2 <(pr_pat_mono … Hf1 … H) -i1 -i2 //
qed-.
(*** after_fwd_at1 *)
lemma pr_after_des_pat_dx (i) (i2) (i1):
- ∀f,f2. @❨i1, f❩ ≘ i → @❨i2, f2❩ ≘ i →
- ∀f1. f2 ⊚ f1 ≘ f → @❨i1, f1❩ ≘ i2.
+ ∀f,f2. ＠⧣❨i1, f❩ ≘ i → ＠⧣❨i2, f2❩ ≘ i →
+ ∀f1. f2 ⊚ f1 ≘ f → ＠⧣❨i1, f1❩ ≘ i2.
#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
[ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
#g [ #j1 ] #Hg [ #H01 ] #H00
(* Note: this requires ↑ on first n *)
(*** after_tls *)
lemma pr_after_tls_sn_tls (n):
- ∀f1,f2,f. @❨𝟏, f1❩ ≘ ↑n →
+ ∀f1,f2,f. ＠⧣❨𝟏, f1❩ ≘ ↑n →
f1 ⊚ f2 ≘ f → ⫰*[n]f1 ⊚ f2 ≘ ⫰*[n]f.
#n @(nat_ind_succ … n) -n //
#n #IH #f1 #f2 #f #Hf1 #Hf
(*** after_uni_succ_dx *)
lemma pr_after_pat_uni (i2) (i1):
- ∀f2. @❨i1, f2❩ ≘ i2 →
+ ∀f2. ＠⧣❨i1, f2❩ ≘ i2 →
∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
(*** after_uni_succ_sn *)
lemma pr_pat_after_uni_tls (i2) (i1):
- ∀f2. @❨i1, f2❩ ≘ i2 →
+ ∀f2. ＠⧣❨i1, f2❩ ≘ i2 →
∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
(*** coafter_inj_O_aux *)
corec fact pr_coafter_inj_unit_aux:
- ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1.
+ ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1.
#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
(*** coafter_inj_aux *)
fact pr_coafter_inj_aux:
- (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1) →
- ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_inj f1.
+ (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1) →
+ ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_inj f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1
(*** coafter_isfin2_fwd_O_aux *)
fact pr_coafter_des_ist_isf_unit_aux:
- ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
+ ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
#f1 #Hf1 #f2 #H
generalize in match Hf1; generalize in match f1; -f1
@(pr_isf_ind … H) -f2
(*** coafter_isfin2_fwd_aux *)
fact pr_coafter_des_ist_isf_aux:
- (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
- ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_isf f1.
+ (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
+ ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_isf f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
(*** coafter_fwd_isid2_O_aux *)
corec fact pr_coafter_des_ist_sn_isi_unit_aux:
- ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
+ ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
#f1 #H1f1 #f2 #f #H #H2f1 #Hf
cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
(*** coafter_fwd_isid2_aux *)
fact pr_coafter_des_ist_sn_isi_aux:
- (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
- ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
+ (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
+ ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
(*** coafter_tls_succ *)
lemma pr_coafter_tls_tl_tls:
∀g2,g1,g. g2 ~⊚ g1 ≘ g →
- ∀j. @❨𝟏, g2❩ ≘ j → ⫰*[j]g2 ~⊚ ⫰g1 ≘ ⫰*[j]g.
+ ∀j. ＠⧣❨𝟏, g2❩ ≘ j → ⫰*[j]g2 ~⊚ ⫰g1 ≘ ⫰*[j]g.
#g2 #g1 #g #Hg #j #Hg2
lapply (pr_nat_pred_bi … Hg2) -Hg2 #Hg2
lapply (pr_coafter_tls_bi_tls … Hg2 … Hg) -Hg #Hg
(* Note: parked for now
lemma coafter_fwd_xpx_pushs:
- ∀g2,f1,g,i,j. @❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
+ ∀g2,f1,g,i,j. ＠⧣❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
∃∃f. ⫰*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
#g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg(coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
qed-.
lemma coafter_fwd_xnx_pushs:
- ∀g2,f1,g,i,j. @❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ g →
+ ∀g2,f1,g,i,j. ＠⧣❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ g →
∃∃f. ⫰*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j] ↑f = g.
#g2 #g1 #g #i #j #Hg2 #Hg
elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
(* Advanced constructions with pr_isi and pr_pat ****************************)
(*** isid_at *)
-lemma pr_isi_pat (f): (∀i. @❨i,f❩ ≘ i) → 𝐈❨f❩.
+lemma pr_isi_pat (f): (∀i. ＠⧣❨i,f❩ ≘ i) → 𝐈❨f❩.
/3 width=1 by pr_eq_id_isi, pr_pat_inv_id/
qed.
(* Inversions with pr_pat ***************************************************)
(*** isid_inv_at *)
-lemma pr_isi_inv_pat (f) (i): 𝐈❨f❩ → @❨i,f❩ ≘ i.
+lemma pr_isi_inv_pat (f) (i): 𝐈❨f❩ → ＠⧣❨i,f❩ ≘ i.
/3 width=3 by pr_isi_inv_eq_id, pr_pat_id, pr_pat_eq_repl_back/
qed-.
(* Destructions with pr_pat *************************************************)
(*** isid_inv_at_mono *)
-lemma pr_isi_pat_des (f) (i1) (i2): 𝐈❨f❩ → @❨i1,f❩ ≘ i2 → i1 = i2.
+lemma pr_isi_pat_des (f) (i1) (i2): 𝐈❨f❩ → ＠⧣❨i1,f❩ ≘ i2 → i1 = i2.
/4 width=3 by pr_isi_inv_eq_id, pr_pat_id_des, pr_pat_eq_repl_fwd/
qed-.
(*** istot *)
definition pr_ist: predicate pr_map ≝
- λf. ∀i. ∃j. @❨i,f❩ ≘ j.
+ λf. ∀i. ∃j. ＠⧣❨i,f❩ ≘ j.
interpretation
"totality condition (partial relocation maps)"
(* Advanced constructions with pr_isi ***************************************)
(*** isid_at_total *)
-lemma pr_isi_pat_total: ∀f. 𝐓❨f❩ → (∀i1,i2. @❨i1,f❩ ≘ i2 → i1 = i2) → 𝐈❨f❩.
+lemma pr_isi_pat_total: ∀f. 𝐓❨f❩ → (∀i1,i2. ＠⧣❨i1,f❩ ≘ i2 → i1 = i2) → 𝐈❨f❩.
#f #H1f #H2f @pr_isi_pat
#i lapply (H1f i) -H1f *
#j #Hf >(H2f … Hf) in ⊢ (???%); -H2f //
(* Advanced constructions with pr_pat ***************************************)
(*** at_dec *)
-lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
+lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (＠⧣❨i1,f❩ ≘ i2).
#f #i1 #i2 #Hf lapply (Hf i1) -Hf *
#j2 #Hf elim (eq_pnat_dec i2 j2)
[ #H destruct /2 width=1 by or_introl/
qed-.
(*** is_at_dec *)
-lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. @❨i1,f❩ ≘ i2).
+lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. ＠⧣❨i1,f❩ ≘ i2).
#f #i2 #Hf
-lapply (dec_plt (λi1.@❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
+lapply (dec_plt (λi1.＠⧣❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
[ /2 width=1 by pr_pat_dec/
| * /3 width=2 by ex_intro, or_introl/
| #H @or_intror * #i1 #Hi12
(*** at_ext *)
corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
- (∀i,i1,i2. @❨i,f1❩ ≘ i1 → @❨i,f2❩ ≘ i2 → i1 = i2) →
+ (∀i,i1,i2. ＠⧣❨i,f1❩ ≘ i1 → ＠⧣❨i,f2❩ ≘ i2 → i1 = i2) →
f1 ≐ f2.
cases (pr_map_split_tl f1) #H1
cases (pr_map_split_tl f2) #H2
(* NON-NEGATIVE APPLICATION FOR PARTIAL RELOCATION MAPS *********************)
definition pr_nat: relation3 pr_map nat nat ≝
- λf,l1,l2. @❨↑l1,f❩ ≘ ↑l2.
+ λf,l1,l2. ＠⧣❨↑l1,f❩ ≘ ↑l2.
interpretation
"relational non-negative application (partial relocation maps)"
qed.
lemma pr_nat_pred_bi (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
+ ＠⧣❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
#f #i1 #i2
>(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
//
(* *)
(**************************************************************************)
-include "ground/notation/relations/rat_3.ma".
+include "ground/notation/relations/ratsharp_3.ma".
include "ground/xoa/ex_3_2.ma".
include "ground/arith/pnat.ma".
include "ground/relocation/pr_tl.ma".
interpretation
"relational positive application (partial relocation maps)"
- 'RAt i1 f i2 = (pr_pat f i1 i2).
+ 'RAtSharp i1 f i2 = (pr_pat f i1 i2).
(*** H_at_div *)
definition H_pr_pat_div: relation4 pr_map pr_map pr_map pr_map ≝
λf2,g2,f1,g1.
- ∀jf,jg,j. @❨jf,f2❩ ≘ j → @❨jg,g2❩ ≘ j →
- ∃∃j0. @❨j0,f1❩ ≘ jf & @❨j0,g1❩ ≘ jg.
+ ∀jf,jg,j. ＠⧣❨jf,f2❩ ≘ j → ＠⧣❨jg,g2❩ ≘ j →
+ ∃∃j0. ＠⧣❨j0,f1❩ ≘ jf & ＠⧣❨j0,g1❩ ≘ jg.
(* Basic inversions *********************************************************)
(*** at_inv_ppx *)
lemma pr_pat_inv_unit_push (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
#f #i1 #i2 * -f -i1 -i2 //
[ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
| #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (eq_inv_pr_push_next … H)
(*** at_inv_npx *)
lemma pr_pat_inv_succ_push (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
- ∃∃j2. @❨j1,g❩ ≘ j2 & ↑j2 = i2.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+ ∃∃j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
| #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(eq_inv_pr_push_bi … Hf) -g destruct /2 width=3 by ex2_intro/
(*** at_inv_xnx *)
lemma pr_pat_inv_next (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
- ∃∃j2. @❨i1,g❩ ≘ j2 & ↑j2 = i2.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
+ ∃∃j2. ＠⧣❨i1,g❩ ≘ j2 & ↑j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
| #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
(*** at_inv_ppn *)
lemma pr_pat_inv_unit_push_succ (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j2 #H1 #H <(pr_pat_inv_unit_push … Hf … H1 H) -f -g -i1 -i2
#H destruct
qed-.
(*** at_inv_npp *)
lemma pr_pat_inv_succ_push_unit (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j1 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct
qed-.
(*** at_inv_npn *)
lemma pr_pat_inv_succ_push_succ (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❨j1,g❩ ≘ j2.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → ＠⧣❨j1,g❩ ≘ j2.
#f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct //
qed-.
(*** at_inv_xnp *)
lemma pr_pat_inv_next_unit (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
#f #i1 #i2 #Hf #g #H elim (pr_pat_inv_next … Hf … H) -f
#x2 #Hg * -i2 #H destruct
qed-.
(*** at_inv_xnn *)
lemma pr_pat_inv_next_succ (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → @❨i1,g❩ ≘ j2.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → ＠⧣❨i1,g❩ ≘ j2.
#f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_next … Hf … H) -f
#x2 #Hg * -i2 #H destruct //
qed-.
(*** at_inv_pxp *)
lemma pr_pat_inv_unit_bi (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
+ ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
#f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
#H #i1 #i2 #Hf #H1 #H2 cases (pr_pat_inv_next_unit … Hf … H H2)
qed-.
(*** at_inv_pxn *)
lemma pr_pat_inv_unit_succ (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
- ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
+ ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
#f elim (pr_map_split_tl … f)
#H #i1 #i2 #Hf #j2 #H1 #H2
[ elim (pr_pat_inv_unit_push_succ … Hf … H1 H H2)
(*** at_inv_nxp *)
lemma pr_pat_inv_succ_unit (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
#f elim (pr_map_split_tl f)
#H #i1 #i2 #Hf #j1 #H1 #H2
[ elim (pr_pat_inv_succ_push_unit … Hf … H1 H H2)
(*** at_inv_nxn *)
lemma pr_pat_inv_succ_bi (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
- ∨∨ ∃∃g. @❨j1,g❩ ≘ j2 & ⫯g = f
- | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+ ∨∨ ∃∃g. ＠⧣❨j1,g❩ ≘ j2 & ⫯g = f
+ | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
#f elim (pr_map_split_tl f) *
/4 width=7 by pr_pat_inv_next_succ, pr_pat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
qed-.
(* Note: the following inversion lemmas must be checked *)
(*** at_inv_xpx *)
lemma pr_pat_inv_push (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
- | ∃∃j1,j2. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+ | ∃∃j1,j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
#f * [2: #i1 ] #i2 #Hf #g #H
[ elim (pr_pat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
| >(pr_pat_inv_unit_push … Hf … H) -f /3 width=1 by conj, or_introl/
(*** at_inv_xpp *)
lemma pr_pat_inv_push_unit (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
#f #i1 #i2 #Hf #g #H elim (pr_pat_inv_push … Hf … H) -f * //
#j1 #j2 #_ #_ * -i2 #H destruct
qed-.
(*** at_inv_xpn *)
lemma pr_pat_inv_push_succ (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
- ∃∃j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+ ∃∃j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1.
#f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_push … Hf … H) -f *
[ #_ * -i2 #H destruct
| #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
(*** at_inv_xxp *)
lemma pr_pat_inv_unit_dx (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → 𝟏 = i2 →
+ ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i2 →
∃∃g. 𝟏 = i1 & ⫯g = f.
#f elim (pr_map_split_tl f)
#H #i1 #i2 #Hf #H2
(*** at_inv_xxn *)
lemma pr_pat_inv_succ_dx (f) (i1) (i2):
- @❨i1,f❩ ≘ i2 → ∀j2. ↑j2 = i2 →
- ∨∨ ∃∃g,j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
- | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+ ＠⧣❨i1,f❩ ≘ i2 → ∀j2. ↑j2 = i2 →
+ ∨∨ ∃∃g,j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
+ | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
#f elim (pr_map_split_tl f)
#H #i1 #i2 #Hf #j2 #H2
[ elim (pr_pat_inv_push_succ … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
(*** at_basic_lt *)
lemma pr_pat_basic_lt (m) (n) (i):
- ninj i ≤ m → @❨i, 𝐛❨m,n❩❩ ≘ i.
+ ninj i ≤ m → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ i.
#m #n #i >(npsucc_pred i) #Hmi
/2 width=1 by pr_nat_basic_lt/
qed.
(*** at_basic_ge *)
lemma pr_pat_basic_ge (m) (n) (i):
- m < ninj i → @❨i, 𝐛❨m,n❩❩ ≘ i+n.
+ m < ninj i → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ i+n.
#m #n #i >(npsucc_pred i) #Hmi <nrplus_npsucc_sn
/3 width=1 by pr_nat_basic_ge, nlt_inv_succ_dx/
qed.
(*** at_basic_inv_lt *)
lemma pr_pat_basic_inv_lt (m) (n) (i) (j):
- ninj i ≤ m → @❨i, 𝐛❨m,n❩❩ ≘ j → i = j.
+ ninj i ≤ m → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ j → i = j.
/3 width=4 by pr_pat_basic_lt, pr_pat_mono/ qed-.
(*** at_basic_inv_ge *)
lemma pr_pat_basic_inv_ge (m) (n) (i) (j):
- m < ninj i → @❨i, 𝐛❨m,n❩❩ ≘ j → i+n = j.
+ m < ninj i → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ j → i+n = j.
/3 width=4 by pr_pat_basic_ge, pr_pat_mono/ qed-.
(*** at_eq_repl_back *)
corec lemma pr_pat_eq_repl_back (i1) (i2):
- pr_eq_repl_back (λf. @❨i1,f❩ ≘ i2).
+ pr_eq_repl_back (λf. ＠⧣❨i1,f❩ ≘ i2).
#f1 * -f1 -i1 -i2
[ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12
cases (pr_eq_inv_push_sn … H12 … H) -g1 /2 width=2 by pr_pat_refl/
(*** at_eq_repl_fwd *)
lemma pr_pat_eq_repl_fwd (i1) (i2):
- pr_eq_repl_fwd (λf. @❨i1,f❩ ≘ i2).
+ pr_eq_repl_fwd (λf. ＠⧣❨i1,f❩ ≘ i2).
#i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
qed-.
-lemma pr_pat_eq (f): ⫯f ≐ f → ∀i. @❨i,f❩ ≘ i.
+lemma pr_pat_eq (f): ⫯f ≐ f → ∀i. ＠⧣❨i,f❩ ≘ i.
#f #Hf #i elim i -i
[ /3 width=3 by pr_pat_eq_repl_back, pr_pat_refl/
| /3 width=7 by pr_pat_eq_repl_back, pr_pat_push/
(* Inversions with pr_eq ****************************************************)
corec lemma pr_pat_inv_eq (f):
- (∀i. @❨i,f❩ ≘ i) → ⫯f ≐ f.
+ (∀i. ＠⧣❨i,f❩ ≘ i) → ⫯f ≐ f.
#Hf
lapply (Hf (𝟏)) #H
lapply (pr_pat_des_id … H) -H #H
(* Constructions with pr_id *************************************************)
(*** id_at *)
-lemma pr_pat_id (i): @❨i,𝐢❩ ≘ i.
+lemma pr_pat_id (i): ＠⧣❨i,𝐢❩ ≘ i.
/2 width=1 by pr_pat_eq, pr_eq_refl/ qed.
(* Inversions with pr_id ****************************************************)
(*** id_inv_at *)
lemma pr_pat_inv_id (f):
- (∀i. @❨i,f❩ ≘ i) → 𝐢 ≐ f.
+ (∀i. ＠⧣❨i,f❩ ≘ i) → 𝐢 ≐ f.
/3 width=1 by pr_pat_inv_eq, pr_id_eq/
qed-.
(*** at_increasing *)
lemma pr_pat_increasing (i2) (i1) (f):
- @❨i1,f❩ ≘ i2 → i1 ≤ i2.
+ ＠⧣❨i1,f❩ ≘ i2 → i1 ≤ i2.
#i2 elim i2 -i2
[ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf //
| #i2 #IH * //
(*** at_increasing_strict *)
lemma pr_pat_increasing_strict (g) (i1) (i2):
- @❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
- ∧∧ i1 < i2 & @❨i1,f❩ ≘ ↓i2.
+ ＠⧣❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
+ ∧∧ i1 < i2 & ＠⧣❨i1,f❩ ≘ ↓i2.
#g #i1 #i2 #Hg #f #H elim (pr_pat_inv_next … Hg … H) -Hg -H
/4 width=2 by conj, pr_pat_increasing, ple_succ_bi/
qed-.
(*** at_fwd_id_ex *)
-lemma pr_pat_des_id (f) (i): @❨i,f❩ ≘ i → ⫯⫰f = f.
+lemma pr_pat_des_id (f) (i): ＠⧣❨i,f❩ ≘ i → ⫯⫰f = f.
#f elim (pr_map_split_tl f) //
#H #i #Hf elim (pr_pat_inv_next … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (pr_pat_increasing … Hg) -Hg
(*** at_le_ex *)
lemma pr_pat_le_ex (j2) (i2) (f):
- @❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
- ∃∃j1. @❨i1,f❩ ≘ j1 & j1 ≤ j2.
+ ＠⧣❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
+ ∃∃j1. ＠⧣❨i1,f❩ ≘ j1 & j1 ≤ j2.
#j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
[ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
#g [ #x2 ] #Hg [ #H2 ] #H0
(*** at_id_le *)
lemma pr_pat_id_le (i1) (i2):
- i1 ≤ i2 → ∀f. @❨i2,f❩ ≘ i2 → @❨i1,f❩ ≘ i1.
+ i1 ≤ i2 → ∀f. ＠⧣❨i2,f❩ ≘ i2 → ＠⧣❨i1,f❩ ≘ i1.
#i1 #i2 #H
@(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ] #f #Hf
lapply (pr_pat_des_id … Hf) #H <H in Hf; -H
(*** at_monotonic *)
theorem pr_pat_monotonic:
- ∀j2,i2,f. @❨i2,f❩ ≘ j2 → ∀j1,i1. @❨i1,f❩ ≘ j1 →
+ ∀j2,i2,f. ＠⧣❨i2,f❩ ≘ j2 → ∀j1,i1. ＠⧣❨i1,f❩ ≘ j1 →
i1 < i2 → j1 < j2.
#j2 elim j2 -j2
[ #i2 #f #H2f elim (pr_pat_inv_unit_dx … H2f) -H2f //
(*** at_inv_monotonic *)
theorem pr_pat_inv_monotonic:
- ∀j1,i1,f. @❨i1,f❩ ≘ j1 → ∀j2,i2. @❨i2,f❩ ≘ j2 →
+ ∀j1,i1,f. ＠⧣❨i1,f❩ ≘ j1 → ∀j2,i2. ＠⧣❨i2,f❩ ≘ j2 →
j1 < j2 → i1 < i2.
#j1 elim j1 -j1
[ #i1 #f #H1f elim (pr_pat_inv_unit_dx … H1f) -H1f //
(*** at_mono *)
theorem pr_pat_mono (f) (i):
- ∀i1. @❨i,f❩ ≘ i1 → ∀i2. @❨i,f❩ ≘ i2 → i2 = i1.
+ ∀i1. ＠⧣❨i,f❩ ≘ i1 → ∀i2. ＠⧣❨i,f❩ ≘ i2 → i2 = i1.
#f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
#Hi elim (plt_ge_false i i)
/2 width=6 by pr_pat_inv_monotonic/
(*** at_inj *)
theorem pr_pat_inj (f) (i):
- ∀i1. @❨i1,f❩ ≘ i → ∀i2. @❨i2,f❩ ≘ i → i1 = i2.
+ ∀i1. ＠⧣❨i1,f❩ ≘ i → ∀i2. ＠⧣❨i2,f❩ ≘ i → i1 = i2.
#f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
#Hi elim (plt_ge_false i i)
/2 width=6 by pr_pat_monotonic/
(*** at_id_fwd *)
lemma pr_pat_id_des (i1) (i2):
- @❨i1,𝐢❩ ≘ i2 → i1 = i2.
+ ＠⧣❨i1,𝐢❩ ≘ i2 → i1 = i2.
/2 width=4 by pr_pat_mono/ qed-.
(* Main constructions with pr_id ********************************************)
(* Note: this requires ↑ on first n *)
(*** at_pxx_tls *)
lemma pr_pat_unit_succ_tls (n) (f):
- @❨𝟏,f❩ ≘ ↑n → @❨𝟏,⫰*[n]f❩ ≘ 𝟏.
+ ＠⧣❨𝟏,f❩ ≘ ↑n → ＠⧣❨𝟏,⫰*[n]f❩ ≘ 𝟏.
#n @(nat_ind_succ … n) -n //
#n #IH #f #Hf
elim (pr_pat_inv_unit_succ … Hf) -Hf [|*: // ] #g #Hg #H0 destruct
(* Note: this requires ↑ on third n2 *)
(*** at_tls *)
-lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≐ ⫰*[n2]f → ∃i1. @❨i1,f❩ ≘ ↑n2.
+lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≐ ⫰*[n2]f → ∃i1. ＠⧣❨i1,f❩ ≘ ↑n2.
#n2 @(nat_ind_succ … n2) -n2
[ /4 width=4 by pr_pat_eq_repl_back, pr_pat_refl, ex_intro/
| #n2 #IH #f <pr_tls_swap <pr_tls_swap in ⊢ (??%→?); #H
(* Note: this does not require ↑ on second and third p *)
(*** at_inv_nxx *)
lemma pr_pat_inv_succ_sn (p) (g) (i1) (j2):
- @❨↑i1,g❩ ≘ j2 → @❨𝟏,g❩ ≘ p →
- ∃∃i2. @❨i1,⫰*[p]g❩ ≘ i2 & p+i2 = j2.
+ ＠⧣❨↑i1,g❩ ≘ j2 → ＠⧣❨𝟏,g❩ ≘ p →
+ ∃∃i2. ＠⧣❨i1,⫰*[p]g❩ ≘ i2 & p+i2 = j2.
#p elim p -p
[ #g #i1 #j2 #Hg #H
elim (pr_pat_inv_unit_bi … H) -H [|*: // ] #f #H0
(* Note: this requires ↑ on first n2 *)
(*** at_inv_tls *)
lemma pr_pat_inv_succ_dx_tls (n2) (i1) (f):
- @❨i1,f❩ ≘ ↑n2 → ⫯⫰*[↑n2]f ≐ ⫰*[n2]f.
+ ＠⧣❨i1,f❩ ≘ ↑n2 → ⫯⫰*[↑n2]f ≐ ⫰*[n2]f.
#n2 @(nat_ind_succ … n2) -n2
[ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf // #g #H1 #H destruct
/2 width=1 by pr_eq_refl/
(*** at_uni *)
lemma pr_pat_uni (n) (i):
- @❨i,𝐮❨n❩❩ ≘ i+n.
+ ＠⧣❨i,𝐮❨n❩❩ ≘ i+n.
#n @(nat_ind_succ … n) -n
/2 width=5 by pr_pat_next/
qed.
(*** at_inv_uni *)
lemma pr_pat_inv_uni (n) (i) (j):
- @❨i,𝐮❨n❩❩ ≘ j → j = i+n.
+ ＠⧣❨i,𝐮❨n❩❩ ≘ j → j = i+n.
/2 width=4 by pr_pat_mono/ qed-.
corec definition tr_compose: tr_map → tr_map → tr_map.
#f2 * #p1 #f1
-@(stream_cons … (f2@❨p1❩))
+@(stream_cons … (f2＠⧣❨p1❩))
@(tr_compose ? f1) -tr_compose -f1
@(⇂*[p1]f2)
defined.
(*** compose_rew *)
lemma tr_compose_unfold (f2) (f1):
- ∀p1. f2@❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
+ ∀p1. f2＠⧣❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
#f2 #f1 #p1 <(stream_unfold … (f2∘(p1⨮f1))) //
qed.
(*** compose_inv_rew *)
lemma tr_compose_inv_unfold (f2) (f1):
∀f,p1,p. f2∘(p1⨮f1) = p⨮f →
- ∧∧ f2@❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
+ ∧∧ f2＠⧣❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
#f2 #f1 #f #p1 #p
<tr_compose_unfold #H destruct
/2 width=1 by conj/
(*** compose_inv_S2 *)
lemma tr_compose_inv_succ_dx (f2) (f1):
∀f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
- ∧∧ f2@❨p1❩+p2 = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+ ∧∧ f2＠⧣❨p1❩+p2 = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
#f2 #f1 #f #p2 #p1 #p
<tr_compose_unfold #H destruct
>nsucc_inj <stream_tls_swap
(*** after_apply *)
lemma tr_after_pap:
∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
- (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@❨p1❩⨮f❩.
+ (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2＠⧣❨p1❩⨮f❩.
#p1 elim p1 -p1
[ * /2 width=1 by tr_after_push_dx/
| #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
(* Forward lemmas on after (specific) *****************************************)
-lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
+lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2＠⧣❨p1❩ = p.
#f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
/3 width=2 by at_inv_O1, sym_eq/
qed-.
qed-.
lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
- (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+ (p2⨮f2)＠⧣❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
(*** compose_apply *)
lemma tr_compose_pap (i) (f1) (f2):
- f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
+ f2＠⧣❨f1＠⧣❨i❩❩ = (f2∘f1)＠⧣❨i❩.
#i elim i -i
[ * #p1 #f1 #f2
<tr_compose_unfold <tr_pap_unit <tr_pap_unit //
(*** compose_inv_S1 *)
lemma tr_compose_inv_next_sn (f2) (f1):
∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
- ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+ ∧∧ ↑(f2＠⧣❨p1❩) = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
#f2 #f1 #f #p1 #p
<tr_compose_unfold #H destruct
/2 width=1 by conj/
(* Advanced constructions with stream_tls ***********************************)
lemma tr_compose_tls (p) (f1) (f2):
- (⇂*[f1@❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+ (⇂*[f1＠⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
<tr_compose_unfold <tr_pap_succ
>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
(* Coonstructions with tr_pap ***********************************************)
lemma tr_id_pap (p):
- p = 𝐢@❨p❩.
+ p = 𝐢＠⧣❨p❩.
#p >(tr_pushs_id p)
/2 width=1 by tr_pap_pushs_le/
qed.
(* *)
(**************************************************************************)
-include "ground/notation/functions/apply_2.ma".
+include "ground/notation/functions/atsharp_2.ma".
include "ground/arith/pnat_plus.ma".
include "ground/relocation/tr_map.ma".
interpretation
"functional positive application (total relocation maps)"
- 'Apply f i = (tr_pap i f).
+ 'AtSharp f i = (tr_pap i f).
(* Basic constructions ******************************************************)
(*** apply_O1 *)
lemma tr_pap_unit (f):
- ∀p. p = (p⨮f)@❨𝟏❩.
+ ∀p. p = (p⨮f)＠⧣❨𝟏❩.
// qed.
(*** apply_S1 *)
lemma tr_pap_succ (f):
- ∀p,i. f@❨i❩+p = (p⨮f)@❨↑i❩.
+ ∀p,i. f＠⧣❨i❩+p = (p⨮f)＠⧣❨↑i❩.
// qed.
(*** apply_eq_repl *)
theorem tr_pap_eq_repl (i):
- stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+ stream_eq_repl … (λ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/
(* Main inversions with stream_eq *******************************************)
corec theorem nstream_eq_inv_ext:
- ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+ ∀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
(*** apply_inj *)
theorem tr_pap_inj (f):
- ∀i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+ ∀i1,i2,j. f＠⧣❨i1❩ = j → f＠⧣❨i2❩ = j → i1 = i2.
/2 width=4 by pr_pat_inj/ qed-.
(* Constructions with pr_pat ***********************************************)
(*** at_total *)
-lemma tr_pat_total: ∀i1,f. @❨i1,𝐭❨f❩❩ ≘ f@❨i1❩.
+lemma tr_pat_total: ∀i1,f. ＠⧣❨i1,𝐭❨f❩❩ ≘ f＠⧣❨i1❩.
#i1 elim i1 -i1
[ * // | #i #IH * /3 width=1 by tr_pat_succ_sn/ ]
qed.
(*** at_inv_total *)
lemma tr_pat_inv_total (f):
- ∀i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → f@❨i1❩ = i2.
+ ∀i1,i2. ＠⧣❨i1, 𝐭❨f❩❩ ≘ i2 → f＠⧣❨i1❩ = i2.
/2 width=6 by pr_pat_mono/ qed-.
(* Constructions with tr_push ***********************************************)
lemma tr_pap_push (f):
- ∀i. ↑(f@❨i❩) = (⫯f)@❨↑i❩.
+ ∀i. ↑(f＠⧣❨i❩) = (⫯f)＠⧣❨↑i❩.
// qed.
(* Constructions with tr_next ***********************************************)
(*** apply_S2 *)
lemma tr_pap_next (f):
- ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
+ ∀i. ↑(f＠⧣❨i❩) = (↑f)＠⧣❨i❩.
* #p #f * //
qed.
(* Constructions with tr_pushs **********************************************)
lemma tr_pap_pushs_le (n) (p) (f):
- p < ↑n → p = (⫯*[n]f)@❨p❩.
+ p < ↑n → p = (⫯*[n]f)＠⧣❨p❩.
#n @(nat_ind_succ … n) -n
[ #p #f #H0
elim (plt_inv_unit_dx … H0)
(* Constructions with stream_tls ********************************************)
lemma tr_pap_plus (p1) (p2) (f):
- (⇂*[ninj p2]f)@❨p1❩+f@❨p2❩ = f@❨p1+p2❩.
+ (⇂*[ninj p2]f)＠⧣❨p1❩+f＠⧣❨p2❩ = f＠⧣❨p1+p2❩.
#p1 #p2 elim p2 -p2
[ * #p #f //
| #i #IH * #p #f
(* Constructions with pr_pat ***********************************************)
(*** at_O1 *)
-lemma tr_pat_unit_sn: ∀i2,f. @❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
+lemma tr_pat_unit_sn: ∀i2,f. ＠⧣❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
#i2 elim i2 -i2 /2 width=5 by pr_pat_refl, pr_pat_next/
qed.
(*** at_S1 *)
-lemma tr_pat_succ_sn: ∀p,f,i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → @❨↑i1, 𝐭❨p⨮f❩❩ ≘ i2+p.
+lemma tr_pat_succ_sn: ∀p,f,i1,i2. ＠⧣❨i1, 𝐭❨f❩❩ ≘ i2 → ＠⧣❨↑i1, 𝐭❨p⨮f❩❩ ≘ i2+p.
#p elim p -p /3 width=7 by pr_pat_push, pr_pat_next/
qed.
(*** at_plus2 *)
lemma tr_pat_plus_dx (f):
- ∀i1,i,p,q. @❨i1, 𝐭❨p⨮f❩❩ ≘ i → @❨i1, 𝐭❨(p+q)⨮f❩❩ ≘ i+q.
+ ∀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 pr_pat_next/
qed.
(*** at_inv_O1 *)
lemma tr_pat_inv_unit_sn (f):
- ∀p,i2. @❨𝟏, 𝐭❨p⨮f❩❩ ≘ i2 → p = i2.
+ ∀p,i2. ＠⧣❨𝟏, 𝐭❨p⨮f❩❩ ≘ i2 → p = i2.
#f #p elim p -p /2 width=6 by pr_pat_inv_unit_push/
#p #IH #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
#j2 #Hj * -i2 /3 width=1 by eq_f/
(*** at_inv_S1 *)
lemma tr_pat_inv_succ_sn (f):
- ∀p,j1,i2. @❨↑j1, 𝐭❨p⨮f❩❩ ≘ i2 →
- ∃∃j2. @❨j1, 𝐭❨f❩❩ ≘ j2 & j2+p = i2.
+ ∀p,j1,i2. ＠⧣❨↑j1, 𝐭❨p⨮f❩❩ ≘ i2 →
+ ∃∃j2. ＠⧣❨j1, 𝐭❨f❩❩ ≘ j2 & j2+p = i2.
#f #p elim p -p /2 width=5 by pr_pat_inv_succ_push/
#p #IH #j1 #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
(* Note: a better conclusion would be: "i1 + ↓p ≤ i2" *)
(*** at_increasing_plus *)
lemma tr_pat_increasing_plus (f):
- ∀p,i1,i2. @❨i1, 𝐭❨p⨮f❩❩ ≘ i2 → i1 + p ≤ ↑i2.
+ ∀p,i1,i2. ＠⧣❨i1, 𝐭❨p⨮f❩❩ ≘ i2 → i1 + p ≤ ↑i2.
#f #p *
[ #i2 #H <(tr_pat_inv_unit_sn … H) -i2 //
| #i1 #i2 #H elim (tr_pat_inv_succ_sn … H) -H
(*** at_fwd_id *)
lemma tr_pat_des_id (f):
- ∀p,i. @❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
+ ∀p,i. ＠⧣❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
#f #p #i #H lapply (pr_pat_des_id … H) -H #H
elim (eq_inv_pr_push_cons … H) -H //
qed-.
(* Main constructions with tr_compose and tr_tls ****************************)
theorem tr_compose_uni_dx (f) (p):
- (𝐮❨f@❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
+ (𝐮❨f＠⧣❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
#f #p
@nstream_eq_inv_ext #q
<tr_compose_pap <tr_compose_pap
(* Coonstructions with tr_pap ***********************************************)
lemma tr_uni_pap_unit (n):
- ↑n = 𝐮❨n❩@❨𝟏❩.
+ ↑n = 𝐮❨n❩＠⧣❨𝟏❩.
// qed.
lemma tr_uni_pap (n) (p):
- p + n = 𝐮❨n❩@❨p❩.
+ p + n = 𝐮❨n❩＠⧣❨p❩.
#n @(nat_ind_succ … n) -n //
#n #IH * [| #p ] //
qed.
class "green"
[ { "relocation maps" * } {
[ { "finite relocation with pairs" * } {
- [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
+ [ "fr2_nat ( ＠⧣❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
[ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
[ "fr2_append ( ?●? )" * ]
[ "fr2_plus ( ?+? )" * ]
[ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_hdtl" "tr_uni_tls" "tr_uni_pap" "tr_uni_compose" * ]
[ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
[ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "tr_compose_pap" "tr_compose_compose" * ]
- [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
+ [ "tr_pap ( ?＠⧣❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
[ "tr_pushs ( ⫯*[?]? )" * ]
[ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
[ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
[ "pr_isu ( 𝐔❨?❩ )" "pr_isu_tl" "pr_isu_uni" * ]
[ "pr_isi ( 𝐈❨?❩ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ]
[ "pr_nat ( @↑❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
- [ "pr_pat ( @❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
+ [ "pr_pat ( ＠⧣❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
[ "pr_basic ( 𝐛❨?,?❩ )" * ]
[ "pr_uni ( 𝐮❨?❩ )" "pr_uni_eq" * ]
[ "pr_id ( 𝐢 ) " "pr_id_eq" * ]
"" "" "nstream_isid" "nstream_id ( 𝐢 )" ""
"" "" "" ""
"" "" "" "nstream_sor"
- "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+ "" "nstream_istot ( ?＠⧣❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
"nstream_basic" ""
* ]
- [ "trace ( ∥?∥ )" "trace_at ( @❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
+ [ "trace ( ∥?∥ )" "trace_at ( ＠⧣❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )"
* ]
}
(* Properties with application **********************************************)
-lemma drops_tls_at: ∀f,i1,i2. @❨i1,f❩ ≘ i2 →
+lemma drops_tls_at: ∀f,i1,i2. ＠⧣❨i1,f❩ ≘ i2 →
∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
/3 width=3 by drops_eq_repl_fwd, pr_pat_inv_succ_dx_tls/ qed-.
-lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❨O,f❩ ≘ i →
+lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. ＠⧣❨O,f❩ ≘ i →
∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J.
#b #f #I #L #K0 #H #i #Hf
elim (drops_split_trans … H) -H [ |5: @(pr_after_nat_uni … Hf) |2,3: skip ] /2 width=1 by pr_after_isi_dx/ #Y #HLY #H
;;
let predefined_classes = [
+ ["@"; "＠"; ];
["*"; "∗"; ];
["/"; "⧸"; ];
["&"; "⅋"; ];
projects / helm.git / commitdiff