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 (**************************************************************************)
15 include "ground_2/notation/functions/identity_0.ma".
16 include "ground_2/notation/relations/isidentity_1.ma".
17 include "ground_2/relocation/nstream_lift.ma".
18 include "ground_2/relocation/nstream_after.ma".
20 (* RELOCATION N-STREAM ******************************************************)
22 let corec id: rtmap ≝ ↑id.
24 interpretation "identity (nstream)"
27 definition isid: predicate rtmap ≝ λf. f ≐ 𝐈𝐝.
29 interpretation "test for identity (trace)"
30 'IsIdentity f = (isid f).
32 (* Basic properties on id ***************************************************)
34 lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝.
35 >(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize //
38 (* Basic properties on isid *************************************************)
43 lemma isid_push: ∀f. 𝐈⦃f⦄ → 𝐈⦃↑f⦄.
44 #f #H normalize >id_unfold /2 width=1 by eq_seq/
47 (* Basic inversion lemmas on isid *******************************************)
49 lemma isid_inv_seq: ∀f,a. 𝐈⦃a@f⦄ → 𝐈⦃f⦄ ∧ a = 0.
50 #f #a normalize >id_unfold in ⊢ (???%→?);
51 #H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
54 lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄.
55 * #a #f #H elim (isid_inv_seq … H) -H //
58 lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥.
59 * #a #f #H elim (isid_inv_seq … H) -H
63 (* inversion lemmas on at ***************************************************)
65 let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
66 * #a #f #Ht lapply (Ht 0)
67 #H lapply (at_inv_O1 … H) -H
68 #H0 >id_unfold @eq_seq
70 | @id_inv_at -id_inv_at
71 #i lapply (Ht (⫯i)) -Ht cases H0 -a
72 #H elim (at_inv_SOx … H) -H //
76 lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
78 [ * #a #f #H elim (isid_inv_seq … H) -H //
79 | #i #IH * #a #f #H elim (isid_inv_seq … H) -H
84 lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
85 /3 width=6 by isid_inv_at, at_mono/ qed-.
87 (* Properties on at *********************************************************)
89 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
90 /2 width=1 by isid_inv_at/ qed.
92 lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
93 /2 width=1 by id_inv_at/ qed.
95 lemma isid_at_total: ∀f. (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄.
97 #i lapply (at_total i f)
98 #H >(Ht … H) in ⊢ (???%); -Ht //
101 (* Properties on after ******************************************************)
103 lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
104 #f2 #f1 #f #Ht #H2 @isid_at_total
105 #i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
106 /3 width=6 by at_inj, eq_stream_sym/
109 lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
110 #f2 #f1 #f #Ht #H1 @isid_at_total
111 #i2 #i #Hi2 lapply (at_total i2 f1)
112 #H0 lapply (at_increasing … H0)
113 #Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
114 /3 width=7 by at_repl_back, at_mono, at_id_le/
117 (* Inversion lemmas on after ************************************************)
119 let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
120 * #a1 #f1 * * [ | #a2 ] #f2 #H cases (isid_inv_seq … H) -H
122 [ @(after_zero … H1) -H1 /2 width=1 by/
123 | @(after_skip … H1) -H1 /2 width=5 by/
127 let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
129 [ #f1 #H cases (isid_inv_seq … H) -H
130 #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/
131 | #a1 #f1 #H @(after_drop … a1 a1) /2 width=5 by/
135 lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
136 /3 width=4 by isid_after_sn, after_mono/
139 lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
140 /3 width=4 by isid_after_dx, after_mono/
143 lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.