1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
16 include "ground/relocation/pstream_tls.ma".
17 include "ground/relocation/pstream_istot.ma".
19 include "ground/arith/pnat_plus.ma".
20 include "ground/relocation/pr_after.ma".
21 include "ground/relocation/tr_map.ma".
23 (* Properties on after (specific) *********************************************)
26 lemma tr_after_push_dx:
27 ∀f2,f1,f. 𝐭❨f2❩ ⊚ f1 ≘ 𝐭❨f❩ →
28 ∀p. 𝐭❨p⨮f2❩ ⊚ ⫯f1 ≘ 𝐭❨p⨮f❩.
29 #f2 #f1 #f #Hf #p elim p -p
30 /2 width=7 by pr_after_refl, pr_after_next/
34 lemma tr_after_next_dx:
35 ∀f2,f1,f,p1,p. 𝐭❨f2❩ ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨p⨮f❩ →
36 ∀p2. 𝐭❨p2⨮f2❩ ⊚ 𝐭❨↑p1⨮f1❩ ≘ 𝐭❨(p+p2)⨮f❩.
37 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
38 /2 width=7 by pr_after_next, pr_after_push/
41 include "ground/lib/stream_tls.ma".
42 include "ground/relocation/tr_pap.ma".
46 ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
47 (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@⧣❨p1❩⨮f❩.
49 [ * /2 width=1 by tr_after_push_dx/
50 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
51 /3 width=1 by tr_after_next_dx/
55 include "ground/relocation/tr_compose_pn.ma".
57 (*** after_total_aux *)
58 corec fact tr_after_total_aux:
59 ∀f2,f1,f. f2 ∘ f1 = f → 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩.
60 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
62 [ #H cases (tr_compose_inv_push_dx … H) -H /3 width=7 by pr_after_refl, eq_f2/
63 | #p1 #H cases (tr_compose_inv_succ_dx … H) -H * -p /3 width=7 by pr_after_push/
65 | #p2 >tr_next_unfold #H cases (tr_compose_inv_next_sn … H) -H * -p
66 /3 width=5 by pr_after_next/
71 theorem tr_after_total:
72 ∀f1,f2. 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f2 ∘ f1❩.
73 /2 width=1 by tr_after_total_aux/ qed.
75 (* Inversion lemmas on after (specific) ***************************************)
77 lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
79 #f2 #g2 #f #p2 elim p2 -p2
80 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
81 #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
82 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
83 #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
84 #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
85 #H destruct /2 width=1 by conj/
89 lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
90 ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
91 #f2 #g2 #f #p2 elim p2 -p2
92 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
93 #g #Hf #H elim (next_inv_seq_dx … H) -H
94 #x #Hx #Hg destruct /2 width=3 by ex2_intro/
95 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
96 #g #Hg #H elim (next_inv_seq_dx … H) -H
97 #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
98 #m #Hf #Hm destruct /2 width=3 by ex2_intro/
102 lemma after_inv_const: ∀f2,f1,f,p1,p.
103 p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
104 #f2 #f1 #f #p1 #p elim p -p
105 [ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
106 #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
107 | #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
111 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
112 /2 width=4 by gr_after_mono/ qed-.
114 (* Forward lemmas on after (specific) *****************************************)
116 lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@⧣❨p1❩ = p.
117 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
118 /3 width=2 by at_inv_O1, sym_eq/
121 lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
122 (⫰*[↓p1]f2) ⊚ f1 ≘ f.
123 #f #f1 #p1 elim p1 -p1
124 [ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
125 | #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
126 #x #Hx #H destruct /2 width=3 by/
130 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
131 (p2⨮f2)@⧣❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
132 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.