lemma lt_S_S: ∀x,y. x < y → ⫯x < ⫯y.
/2 width=1 by le_S_S/ qed.
+lemma lt_S: ∀n,m. n < m → n < ⫯m.
+/2 width=1 by le_S/ qed.
+
lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
+lemma lt_inv_O1: ∀n. 0 < n → ∃m. ⫯m = n.
+* /2 width=2 by ex_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_S1: ∀m,n. ⫯m < n → ∃∃p. m < p & ⫯p = n.
+#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ⫯z = y.
+* /3 width=3 by le_S_S_to_le, ex2_intro/
+#x #H elim (lt_le_false … H) -H //
+qed-.
+
lemma pred_inv_refl: ∀m. pred m = m → m = 0.
* // normalize #m #H elim (lt_refl_false m) //
qed-.
(* Basic inversion lemmas ***************************************************)
-fact eq_stream_inv_seq_aux: ∀A,t1,t2. t1 ≐⦋A⦌ t2 →
- ∀u1,u2,a1,a2. t1 = a1@u1 → t2 = a2@u2 →
- a1 = a2 ∧ u1 ≐ u2.
+lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≐⦋A⦌ t2 →
+ ∀u1,u2,a1,a2. a1@u1 = t1 → a2@u2 = t2 →
+ u1 ≐ u2 ∧ a1 = a2.
#A #t1 #t2 * -t1 -t2
#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
qed-.
-lemma eq_stream_inv_seq: ∀A,t1,t2,b1,b2. b1@t1 ≐⦋A⦌ b2@t2 → b1 = b2 ∧ t1 ≐ t2.
-/2 width=5 by eq_stream_inv_seq_aux/ qed-.
-
(* Basic properties *********************************************************)
-lemma stream_expand (A) (t:stream A): t = match t with [ seq a u ⇒ a @ u ].
+lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a @ u ] = t.
#A * //
qed.
let corec eq_stream_trans: ∀A. Transitive … (eq_stream A) ≝ ?.
#A #t1 #t * -t1 -t
-#t1 #t #b1 #b #Hb1 #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H
-#Hb2 #Ht2 @eq_seq /2 width=3 by/
+#t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b
+/3 width=7 by eq_seq/
qed-.
theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≐ t1 → t ≐ t2 → t1 ≐⦋A⦌ t2.
lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
#A #i elim i -i //
-#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
-/2 width=1 by/
+#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( f1 ≗ break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'FunExtEq $f1 $f2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐓 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsTotal $f }.
theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
/2 width=8 by after_mono/ qed-.
+
+(* Properties on after ******************************************************)
+
+lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
+#f2 #f1 #f #Ht #H2 @isid_at_total
+#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
+/3 width=6 by at_inj, eq_stream_sym/
+qed.
+
+lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
+#f2 #f1 #f #Ht #H1 @isid_at_total
+#i2 #i #Hi2 lapply (at_total i2 f1)
+#H0 lapply (at_increasing … H0)
+#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
+/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
+qed.
+
+(* Inversion lemmas on after ************************************************)
+
+let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
+* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
+/3 width=7 by after_push, after_refl/
+qed-.
+
+let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
+* #n2 #f2 * *
+[ #f1 #H cases (isid_inv_seq … H) -H
+ /3 width=7 by after_refl/
+| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
+]
+qed-.
+
+lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
+/3 width=8 by isid_after_sn, after_mono/
+qed-.
+
+lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
+/3 width=8 by isid_after_dx, after_mono/
+qed-.
+
+axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.tcs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/apply_2.ma".
-include "ground_2/notation/relations/rat_3.ma".
-include "ground_2/relocation/nstream_lift.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-let rec apply (i: nat) on i: rtmap → nat ≝ ?.
-* #n #f cases i -i
-[ @n
-| #i lapply (apply i f) -apply -i -f
- #i @(⫯(n+i))
-]
-defined.
-
-interpretation "functional application (nstream)"
- 'Apply f i = (apply i f).
-
-inductive at: rtmap → relation nat ≝
-| at_refl: ∀f. at (↑f) 0 0
-| at_push: ∀f,i1,i2. at f i1 i2 → at (↑f) (⫯i1) (⫯i2)
-| at_next: ∀f,i1,i2. at f i1 i2 → at (⫯f) i1 (⫯i2)
-.
-
-interpretation "relational application (nstream)"
- 'RAt i1 f i2 = (at f i1 i2).
-
-(* Basic properties on apply ************************************************)
-
-lemma apply_eq_repl (i): eq_stream_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
-#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
-elim (eq_stream_inv_seq ????? H) -H normalize //
-#Hn #Hf /4 width=1 by eq_f2, eq_f/
-qed.
-
-lemma apply_S1: ∀f,n,i. (⫯n@f)@❴i❵ = ⫯((n@f)@❴i❵).
-#n #f * //
-qed.
-
-(* Basic inversion lemmas on at *********************************************)
-
-fact at_inv_OOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. i1 = 0 → f = ↑g → i2 = 0.
-#f #i1 #i2 * -f -i1 -i2 //
-[ #f #i1 #i2 #_ #g #H destruct
-| #f #i1 #i2 #_ #g #_ #H elim (discr_next_push … H)
-]
-qed-.
-
-lemma at_inv_OOx: ∀f,i2. @⦃0, ↑f⦄ ≡ i2 → i2 = 0.
-/2 width=6 by at_inv_OOx_aux/ qed-.
-
-fact at_inv_SOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j1. i1 = ⫯j1 → f = ↑g →
- ∃∃j2. @⦃j1, g⦄ ≡ j2 & i2 = ⫯j2.
-#f #i1 #i2 * -f -i1 -i2
-[ #f #g #j1 #H destruct
-| #f #i1 #i2 #Hi #g #j1 #H #Hf <(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
-| #f #i1 #i2 #_ #g #j1 #_ #H elim (discr_next_push … H)
-]
-qed-.
-
-lemma at_inv_SOx: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ i2 →
- ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2.
-/2 width=5 by at_inv_SOx_aux/ qed-.
-
-fact at_inv_xSx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. f = ⫯g →
- ∃∃j2. @⦃i1, g⦄ ≡ j2 & i2 = ⫯j2.
-#f #i1 #i2 * -f -i1 -i2
-[ #f #g #H elim (discr_push_next … H)
-| #f #i1 #i2 #_ #g #H elim (discr_push_next … H)
-| #f #i1 #i2 #Hi #g #H <(injective_next … H) -g /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma at_inv_xSx: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 →
- ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2.
-/2 width=3 by at_inv_xSx_aux/ qed-.
-
-(* Advanced inversion lemmas on at ******************************************)
-
-lemma at_inv_OOS: ∀f,i2. @⦃0, ↑f⦄ ≡ ⫯i2 → ⊥.
-#f #i2 #H lapply (at_inv_OOx … H) -H
-#H destruct
-qed-.
-
-lemma at_inv_SOS: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2.
-#f #i1 #i2 #H elim (at_inv_SOx … H) -H
-#j2 #H2 #H destruct //
-qed-.
-
-lemma at_inv_SOO: ∀f,i1. @⦃⫯i1, ↑f⦄ ≡ 0 → ⊥.
-#f #i1 #H elim (at_inv_SOx … H) -H
-#j2 #_ #H destruct
-qed-.
-
-lemma at_inv_xSS: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2.
-#f #i1 #i2 #H elim (at_inv_xSx … H) -H
-#j2 #H #H2 destruct //
-qed-.
-
-lemma at_inv_xSO: ∀f,i1. @⦃i1, ⫯f⦄ ≡ 0 → ⊥.
-#f #i1 #H elim (at_inv_xSx … H) -H
-#j2 #_ #H destruct
-qed-.
-
-lemma at_inv_xOx: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ i2 →
- (i1 = 0 ∧ i2 = 0) ∨
- ∃∃j1,j2. @⦃j1, f⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2.
-#f * [2: #i1 ] #i2 #H
-[ elim (at_inv_SOx … H) -H
- #j2 #H2 #H destruct /3 width=5 by or_intror, ex3_2_intro/
-| >(at_inv_OOx … H) -i2 /3 width=1 by conj, or_introl/
-]
-qed-.
-
-lemma at_inv_xOO: ∀f,i. @⦃i, ↑f⦄ ≡ 0 → i = 0.
-#f #i #H elim (at_inv_xOx … H) -H * //
-#j1 #j2 #_ #_ #H destruct
-qed-.
-
-lemma at_inv_xOS: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ ⫯i2 →
- ∃∃j1. @⦃j1, f⦄ ≡ i2 & i1 = ⫯j1.
-#f #i1 #i2 #H elim (at_inv_xOx … H) -H *
-[ #_ #H destruct
-| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-(* alternative definition ***************************************************)
-
-lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≡ i2.
-#i2 elim i2 -i2 /2 width=1 by at_refl, at_next/
-qed.
-
-lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, n@f⦄ ≡ ⫯(n+i2).
-#n elim n -n /3 width=1 by at_push, at_next/
-qed.
-
-lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≡ i2 → i2 = n.
-#f #n elim n -n /2 width=2 by at_inv_OOx/
-#n #IH #i2 <next_rew #H elim (at_inv_xSx … H) -H
-#j2 #Hj #H destruct /3 width=1 by eq_f/
-qed-.
-
-lemma at_inv_S1: ∀f,n,j1,i2. @⦃⫯j1, n@f⦄ ≡ i2 → ∃∃j2. @⦃j1, f⦄ ≡ j2 & i2 =⫯(n+j2).
-#f #n elim n -n /2 width=1 by at_inv_SOx/
-#n #IH #j1 #i2 <next_rew #H elim (at_inv_xSx … H) -H
-#j2 #Hj #H destruct elim (IH … Hj) -IH -Hj
-#i2 #Hi #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma at_total: ∀i1,f. @⦃i1, f⦄ ≡ f@❴i1❵.
-#i1 elim i1 -i1
-[ * // | #i #IH * /3 width=1 by at_S1/ ]
-qed.
-
-(* Advanced forward lemmas on at ********************************************)
-
-lemma at_increasing: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2.
-#f #i1 #i2 #H elim H -f -i1 -i2 /2 width=1 by le_S_S, le_S/
-qed-.
-
-lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≡ i2 → i1 + n ≤ i2.
-#f #n *
-[ #i2 #H >(at_inv_O1 … H) -i2 //
-| #i1 #i2 #H elim (at_inv_S1 … H) -H
- #j1 #Ht #H destruct
- /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/
-]
-qed-.
-
-lemma at_increasing_strict: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 →
- i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2.
-#f #i1 #i2 #H elim (at_inv_xSx … H) -H
-#j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/
-qed-.
-
-lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≡ i → n = 0.
-#f #n *
-[ #H <(at_inv_O1 … H) -f -n //
-| #i #H elim (at_inv_S1 … H) -H
- #j #H #H0 destruct lapply (at_increasing … H) -H
- #H lapply (eq_minus_O … H) -H //
-]
-qed-.
-
-(* Basic properties on at ***************************************************)
-
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i.
-#f #i1 #i #n #m #H elim m -m /2 width=1 by at_next/
-qed.
-
-(* Advanced properties on at ************************************************)
-
-lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1.
-#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
-* #n #f #H lapply (at_fwd_id … H)
-#H0 destruct /4 width=1 by at_S1, at_inv_SOS/
-qed-.
-
-(* Main properties on at ****************************************************)
-
-let corec at_ext: ∀f1,f2. (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≐ f2 ≝ ?.
-* #n1 #f1 * #n2 #f2 #Hi lapply (Hi 0 n1 n2 ? ?) //
-#H lapply (at_ext f1 f2 ?) /2 width=1 by eq_seq/ -at_ext
-#j #j1 #j2 #H1 #H2 @(injective_plus_r … n2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *)
-qed-.
-
-theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀f1,f2. f1 ≐ f2 → ∀j1,j2. @⦃i1, f1⦄ ≡ j1 → @⦃i2, f2⦄ ≡ j2 → j1 < j2.
-#i1 #i2 #H @(lt_elim … H) -i1 -i2
-[ #i2 * #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
- #H #Ht #j1 #j2 #H1 #H2 destruct
- >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 //
-| #i1 #i2 #IH * #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
- #H #Ht #j1 #j2 #H1 #H2 destruct
- elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2
- #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=5 by lt_S_S, monotonic_lt_plus_r/
-]
-qed-.
-
-theorem at_inv_monotonic: ∀f1,i1,j1. @⦃i1, f1⦄ ≡ j1 → ∀f2,i2,j2. @⦃i2, f2⦄ ≡ j2 → f1 ≐ f2 → j2 < j1 → i2 < i1.
-#f1 #i1 #j1 #H elim H -f1 -i1 -j1
-[ #f1 #f2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) //
-| #f1 #i1 #j1 #_ #IH * #n2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
- #H0 #Ht destruct elim (at_inv_xOx … H) -H *
- [ #H1 #H2 destruct //
- | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=5 by lt_S_S_to_lt, lt_S_S/
- ]
-| * #n1 #f1 #i1 #j1 #_ #IH * #n2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
- #H0 #Ht destruct <next_rew in H; #H elim (at_inv_xSx … H) -H
- #y2 #Hy #H destruct /3 width=5 by eq_seq, lt_S_S_to_lt/
-]
-qed-.
-
-theorem at_mono: ∀f1,f2. f1 ≐ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1.
-#f1 #f2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_stream_sym/
-qed-.
-
-theorem at_inj: ∀f1,f2. f1 ≐ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2.
-#f1 #f2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_stream_sym/
-qed-.
-
-lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i2 = f@❴i1❵.
-/2 width=6 by at_mono/ qed-.
-
-lemma at_eq_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2).
-#i1 #i2 #f1 #H1 #f2 #Hf lapply (at_total i1 f2)
-#H2 <(at_mono … Hf … H1 … H2) -f1 -i2 //
-qed-.
-
-lemma at_eq_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2).
-#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_eq_repl_back/
-qed-.
-
-(* Advanced properties on at ************************************************)
-
-(* Note: see also: trace_at/at_dec *)
-lemma at_dec: ∀f,i1,i2. Decidable (@⦃i1, f⦄ ≡ i2).
-#f #i1 #i2 lapply (at_total i1 f)
-#Ht elim (eq_nat_dec i2 (f@❴i1❵))
-[ #H destruct /2 width=1 by or_introl/
-| /4 width=6 by at_mono, or_intror/
-]
-qed-.
-
-lemma is_at_dec_le: ∀f,i2,i. (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
-#f #i2 #i elim i -i
-[ #Ht @or_intror * /3 width=3 by at_increasing/
-| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/
- #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/
- #H destruct -Ht /2 width=1 by/
-]
-qed-.
-
-(* Note: see also: trace_at/is_at_dec *)
-lemma is_at_dec: ∀f,i2. Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
-#f #i2 @(is_at_dec_le ?? (⫯i2)) /2 width=4 by lt_le_false/
-qed-.
-
-(* Advanced properties on apply *********************************************)
-
-fact apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. j1 = f1@❴i1❵ → j2 = f2@❴i2❵ →
- j1 = j2 → f1 ≐ f2 → i1 = i2.
-/2 width=6 by at_inj/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_eq.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific properties on eq ************************************************)
+
+fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≗ n2@f2 → n1 = n2 ∧ f1 ≗ f2.
+#f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
+[ #n2 #H elim (eq_inv_px … H) -H [2,3: // ]
+ #g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+| #n1 #H elim (eq_inv_np … H) -H //
+| #n1 #n2 #IH #H lapply (eq_inv_nn … H ????) -H [1,2,3,4: // ]
+ #H elim (IH H) -IH -H /2 width=1 by conj/
+]
+qed-.
+
+lemma eq_inv_seq: ∀g1,g2. g1 ≗ g2 → ∀f1,f2,n1,n2. n1@f1 = g1 → n2@f2 = g2 →
+ n1 = n2 ∧ f1 ≗ f2.
+/2 width=1 by eq_inv_seq_aux/ qed-.
+
+let corec nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2 ≝ ?.
+* #n1 #f1 * #n2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf *
+#g1 #g2 #Hg #H1 #H2
+[ cases (push_inv_seq_dx … H1) -H1 * -n1 #H1
+ cases (push_inv_seq_dx … H2) -H2 * -n2 #H2
+ @eq_seq /2 width=1 by/
+| cases (next_inv_seq_dx … H1) -H1 #m1 #H1 * -n1
+ cases (next_inv_seq_dx … H2) -H2 #m2 #H2 * -n2
+ cases (eq_inv_seq … Hg … H1 H2) -g1 -g2 #Hm #Hf
+ @eq_seq /2 width=1 by/
+]
+qed-.
+
+let corec nstream_inv_eq: ∀f1,f2. f1 ≐ f2 → f1 ≗ f2 ≝ ?.
+* #n1 #f1 * #n2 #f2 #H cases (eq_stream_inv_seq ??? H) -H [2,3,4,5,6,7: // ]
+#Hf * -n2 cases n1 -n1 /3 width=5 by eq_push/
+#n @eq_next /3 width=5 by eq_seq/
+qed.
+
+lemma eq_seq_id: ∀f1,f2. f1 ≗ f2 → ∀n. n@f1 ≗ n@f2.
+/4 width=1 by nstream_inv_eq, nstream_eq, eq_seq/ qed.
(**************************************************************************)
include "ground_2/notation/functions/identity_0.ma".
-include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/nstream_after.ma".
+include "ground_2/relocation/rtmap_eq.ma".
(* RELOCATION N-STREAM ******************************************************)
interpretation "identity (nstream)"
'Identity = (id).
-definition isid: predicate rtmap ≝ λf. f ≐ 𝐈𝐝.
+(* Basic properties *********************************************************)
-interpretation "test for identity (trace)"
- 'IsIdentity f = (isid f).
-
-(* Basic properties on id ***************************************************)
-
-lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝.
->(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize //
-qed.
-
-(* Basic properties on isid *************************************************)
-
-lemma isid_eq_repl_back: eq_stream_repl_back … isid.
-/2 width=3 by eq_stream_canc_sn/ qed-.
-
-lemma isid_eq_repl_fwd: eq_stream_repl_fwd … isid.
-/3 width=3 by isid_eq_repl_back, eq_stream_repl_sym/ qed-.
-
-lemma isid_id: 𝐈⦃𝐈𝐝⦄.
-// qed.
-
-lemma isid_push: ∀f. 𝐈⦃f⦄ → 𝐈⦃↑f⦄.
-#f #H normalize >id_unfold /2 width=1 by eq_seq/
-qed.
-
-(* Basic inversion lemmas on isid *******************************************)
-
-lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ n = 0.
-#f #n normalize >id_unfold in ⊢ (???%→?);
-#H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
-qed-.
-
-lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄.
-* #n #f #H elim (isid_inv_seq … H) -H //
-qed-.
-
-lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥.
-* #n #f #H elim (isid_inv_seq … H) -H
-#_ #H destruct
-qed-.
-
-lemma isid_inv_gen: ∀f. 𝐈⦃f⦄ → ∃∃g. 𝐈⦃g⦄ & f = ↑g.
-* #n #f #H elim (isid_inv_seq … H) -H
-#Hf #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≐ f2.
-/2 width=3 by eq_stream_canc_dx/ qed-.
-
-(* inversion lemmas on at ***************************************************)
-
-let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
-* #n #f #Ht lapply (Ht 0)
-#H lapply (at_inv_O1 … H) -H
-#H0 >id_unfold @eq_seq
-[ cases H0 -n //
-| @id_inv_at -id_inv_at
- #i lapply (Ht (⫯i)) -Ht cases H0 -n
- #H elim (at_inv_SOx … H) -H //
-]
-qed-.
-
-lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
-#i elim i -i
-[ * #n #f #H elim (isid_inv_seq … H) -H //
-| #i #IH * #n #f #H elim (isid_inv_seq … H) -H
- /3 width=1 by at_S1/
-]
-qed-.
-
-lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
-/3 width=6 by isid_inv_at, at_mono/ qed-.
-
-(* Properties on at *********************************************************)
-
-lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
-/2 width=1 by isid_inv_at/ qed.
-
-lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
-/2 width=1 by id_inv_at/ qed.
-
-lemma isid_at_total: ∀f. (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄.
-#f #Ht @isid_at
-#i lapply (at_total i f)
-#H >(Ht … H) in ⊢ (???%); -Ht //
-qed.
-
-(* Properties on after ******************************************************)
-
-lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
-#f2 #f1 #f #Ht #H2 @isid_at_total
-#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
-/3 width=6 by at_inj, eq_stream_sym/
+lemma id_rew: ↑𝐈𝐝 = 𝐈𝐝.
+<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize //
qed.
-lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
-#f2 #f1 #f #Ht #H1 @isid_at_total
-#i2 #i #Hi2 lapply (at_total i2 f1)
-#H0 lapply (at_increasing … H0)
-#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
-/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
+lemma id_eq_rew: ↑𝐈𝐝 ≗ 𝐈𝐝.
+cases id_rew in ⊢ (??%); //
qed.
-
-(* Inversion lemmas on after ************************************************)
-
-let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
-* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
-/3 width=7 by after_push, after_refl/
-qed-.
-
-let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
-* #n2 #f2 * *
-[ #f1 #H cases (isid_inv_seq … H) -H
- /3 width=7 by after_refl/
-| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
-]
-qed-.
-
-lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
-/3 width=8 by isid_after_sn, after_mono/
-qed-.
-
-lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
-/3 width=8 by isid_after_dx, after_mono/
-qed-.
-
-axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.
--- /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_2/notation/functions/identity_0.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific inversion lemmas ************************************************)
+
+lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ 0 = n.
+#f #n #H elim (isid_inv_gen … H) -H
+#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/apply_2.ma".
+include "ground_2/relocation/nstream_eq.ma".
+include "ground_2/relocation/rtmap_istot.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+* #n #f cases i -i
+[ @n
+| #i lapply (apply i f) -apply -i -f
+ #i @(⫯(n+i))
+]
+defined.
+
+interpretation "functional application (nstream)"
+ 'Apply f i = (apply i f).
+
+(* Specific properties on at ************************************************)
+
+lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≡ i2.
+#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
+qed.
+
+lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, n@f⦄ ≡ ⫯(n+i2).
+#n elim n -n /3 width=7 by at_push, at_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,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i.
+#f #i1 #i #n #m #H elim m -m /2 width=5 by at_next/
+qed.
+
+(* Specific inversion lemmas on at ******************************************)
+
+lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≡ i2 → n = i2.
+#f #n elim n -n /2 width=6 by at_inv_ppx/
+#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
+#j2 #Hj * -i2 /3 width=1 by eq_f/
+qed-.
+
+lemma at_inv_S1: ∀f,n,j1,i2. @⦃⫯j1, n@f⦄ ≡ i2 →
+ ∃∃j2. @⦃j1, f⦄ ≡ j2 & ⫯(n+j2) = i2.
+#f #n elim n -n /2 width=5 by at_inv_npx/
+#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
+#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 at_mono/ qed-.
+
+(* Spercific forward lemmas on at *******************************************)
+
+lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≡ i2 → i1 + n ≤ i2.
+#f #n *
+[ #i2 #H <(at_inv_O1 … H) -i2 //
+| #i1 #i2 #H elim (at_inv_S1 … H) -H
+ #j1 #Ht * -i2 /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/
+]
+qed-.
+
+lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≡ i → 0 = n.
+#f #n #i #H elim (at_fwd_id_ex … H) -H
+#g #H elim (push_inv_seq_dx … H) -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
+#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
+elim (eq_inv_seq_aux … H) -H normalize //
+#Hn #Hf /4 width=1 by eq_f2, eq_f/
+qed.
+
+lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
+* #n #f * //
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
+ j1 = j2 → f1 ≗ f2 → i1 = i2.
+/2 width=6 by at_inj/ qed-.
(* Basic properties *********************************************************)
-lemma push_eq_repl: eq_stream_repl … (λf1,f2. ↑f1 ≐ ↑f2).
-/2 width=1 by eq_seq/ qed.
-
-lemma next_eq_repl: eq_stream_repl … (λf1,f2. ⫯f1 ≐ ⫯f2).
-* #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
-/2 width=1 by eq_seq/
-qed.
-
-lemma push_rew: ∀f. ↑f = 0@f.
+lemma push_rew: ∀f. 0@f = ↑f.
// qed.
-lemma next_rew: ∀f,n. ⫯(n@f) = (⫯n)@f.
+lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f).
// qed.
-
+(*
lemma next_rew_sn: ∀f,n1,n2. n1 = ⫯n2 → n1@f = ⫯(n2@f).
// qed.
-
+*)
(* Basic inversion lemmas ***************************************************)
lemma injective_push: injective ? ? push.
* #n1 #f1 * #n2 #f2 normalize #H destruct //
qed-.
-lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → n = 0 ∧ g = f.
-#f #g #n >push_rew #H destruct /2 width=1 by conj/
-qed-.
-
-lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → n = 0 ∧ g = f.
-#f #g #n >push_rew #H destruct /2 width=1 by conj/
-qed-.
-
-lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. n = ⫯m & f = m@g.
-* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. n = ⫯m & f = m@g.
-* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma push_inv_dx: ∀x,f. x ≐ ↑f → ∃∃g. x = ↑g & g ≐ f.
-* #m #x #f #H elim (eq_stream_inv_seq ????? H) -H
-/2 width=3 by ex2_intro/
-qed-.
-
-lemma push_inv_sn: ∀f,x. ↑f ≐ x → ∃∃g. x = ↑g & f ≐ g.
-#f #x #H lapply (eq_stream_sym … H) -H
-#H elim (push_inv_dx … H) -H
-/3 width=3 by eq_stream_sym, ex2_intro/
+lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f.
+#f #g #n <push_rew #H destruct /2 width=1 by conj/
qed-.
-lemma push_inv_bi: ∀f,g. ↑f ≐ ↑g → f ≐ g.
-#f #g #H elim (push_inv_dx … H) -H
-#x #H #Hg lapply (injective_push … H) -H //
+lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → 0 = n ∧ g = f.
+#f #g #n <push_rew #H destruct /2 width=1 by conj/
qed-.
-lemma next_inv_dx: ∀x,f. x ≐ ⫯f → ∃∃g. x = ⫯g & g ≐ f.
-* #m #x * #n #f #H elim (eq_stream_inv_seq ????? H) -H
-/3 width=5 by eq_seq, ex2_intro/
+lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. m@g = f & ⫯m = n.
+* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
qed-.
-lemma next_inv_sn: ∀f,x. ⫯f ≐ x → ∃∃g. x = ⫯g & f ≐ g.
-#f #x #H lapply (eq_stream_sym … H) -H
-#H elim (next_inv_dx … H) -H
-/3 width=3 by eq_stream_sym, ex2_intro/
+lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. m@g = f & ⫯m = n.
+* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
qed-.
-lemma next_inv_bi: ∀f,g. ⫯f ≐ ⫯g → f ≐ g.
-#f #g #H elim (next_inv_dx … H) -H
-#x #H #Hg lapply (injective_next … H) -H //
+lemma pn_split: ∀f. (∃g. ↑g = f) ∨ (∃g. ⫯g = f).
+* * /3 width=2 by or_introl, or_intror, ex_intro/
qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.tcs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/relocation/nstream_lift.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-coinductive sle: relation rtmap ≝
-| sle_next: ∀f1,f2,g1,g2. sle f1 f2 → g1 = ↑f1 → g2 = ↑f2 → sle g1 g2
-| sle_push: ∀f1,f2,g1,g2. sle f1 f2 → g1 = ⫯f1 → g2 = ⫯f2 → sle g1 g2
-| sle_weak: ∀f1,f2,g1,g2. sle f1 f2 → g1 = ↑f1 → g2 = ⫯f2 → sle g1 g2
-.
-
-interpretation "inclusion (nstream)"
- 'subseteq t1 t2 = (sle t1 t2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact sle_inv_xO_aux: ∀g1,g2. g1 ⊆ g2 → ∀f2. g2 = ↑f2 →
- ∃∃f1. f1 ⊆ f2 & g1 = ↑f1.
-#g1 #g2 * -g1 -g2
-#f1 #f2 #g1 #g2 #H #H1 #H2 #x2 #Hx2 destruct
-[ lapply (injective_push … Hx2) -Hx2 /2 width=3 by ex2_intro/ ]
-elim (discr_next_push … Hx2)
-qed-.
-
-lemma sle_inv_xO: ∀g1,f2. g1 ⊆ ↑f2 → ∃∃f1. f1 ⊆ f2 & g1 = ↑f1.
-/2 width=3 by sle_inv_xO_aux/ qed-.
-
-fact sle_inv_Sx_aux: ∀g1,g2. g1 ⊆ g2 → ∀f1. g1 = ⫯f1 →
- ∃∃f2. f1 ⊆ f2 & g2 = ⫯f2.
-#g1 #g2 * -g1 -g2
-#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #Hx1 destruct
-[2: lapply (injective_next … Hx1) -Hx1 /2 width=3 by ex2_intro/ ]
-elim (discr_push_next … Hx1)
-qed-.
-
-lemma sle_inv_Sx: ∀f1,g2. ⫯f1 ⊆ g2 → ∃∃f2. f1 ⊆ f2 & g2 = ⫯f2.
-/2 width=3 by sle_inv_Sx_aux/ qed-.
-
-fact sle_inv_OS_aux: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 → f1 ⊆ f2.
-#g1 #g2 * -g1 -g2
-#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
-[ elim (discr_push_next … Hx2)
-| elim (discr_next_push … Hx1)
-| lapply (injective_push … Hx1) -Hx1
- lapply (injective_next … Hx2) -Hx2 //
-]
-qed-.
-
-lemma sle_inv_OS: ∀f1,f2. ↑f1 ⊆ ⫯f2 → f1 ⊆ f2.
-/2 width=5 by sle_inv_OS_aux/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact sle_inv_OO_aux: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 → f1 ⊆ f2.
-#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_xO_aux … H … H2) -g2
-#x1 #H #Hx1 destruct lapply (injective_push … Hx1) -Hx1 //
-qed-.
-
-fact sle_inv_SS_aux: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. g1 = ⫯f1 → g2 = ⫯f2 → f1 ⊆ f2.
-#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_Sx_aux … H … H1) -g1
-#x2 #H #Hx2 destruct lapply (injective_next … Hx2) -Hx2 //
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rat_3.ma".
+include "ground_2/relocation/rtmap_id.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive at: rtmap → relation nat ≝
+| at_refl: ∀f,g,j1,j2. ↑f = g → 0 = j1 → 0 = j2 → at g j1 j2
+| at_push: ∀f,i1,i2. at f i1 i2 → ∀g,j1,j2. ↑f = g → ⫯i1 = j1 → ⫯i2 = j2 → at g j1 j2
+| at_next: ∀f,i1,i2. at f i1 i2 → ∀g,j2. ⫯f = g → ⫯i2 = j2 → at g i1 j2
+.
+
+interpretation "relational application (rtmap)"
+ 'RAt i1 f i2 = (at f i1 i2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma at_inv_ppx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. 0 = i1 → ↑g = f → 0 = i2.
+#f #i1 #i2 * -f -i1 -i2 //
+[ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
+| #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
+]
+qed-.
+
+lemma at_inv_npx: ∀f,i1,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 >(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
+| #f #i1 #i2 #_ #g #j2 * #_ #x #x1 #_ #H elim (discr_push_next … H)
+]
+qed-.
+
+lemma at_inv_xnx: ∀f,i1,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 (discr_next_push … H)
+| #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
+| #f #i1 #i2 #Hi #g #j2 * * #x #H >(injective_next … H) -g /2 width=3 by ex2_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g,j2. 0 = i1 → ↑g = f → ⫯j2 = i2 → ⊥.
+#f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
+#H destruct
+qed-.
+
+lemma at_inv_npn: ∀f,i1,i2. @⦃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 (at_inv_npx … Hf … H1 H) -f -i1
+#x2 #Hg * -i2 #H destruct //
+qed-.
+
+lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥.
+#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
+#x2 #Hg * -i2 #H destruct
+qed-.
+
+lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g,j2. ⫯g = f → ⫯j2 = i2 → @⦃i1, g⦄ ≡ j2.
+#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f
+#x2 #Hg * -i2 #H destruct //
+qed-.
+
+lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = i2 →
+ ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
+#f elim (pn_split … f) *
+#g #H #i1 #i2 #Hf #j2 #H1 #H2
+[ elim (at_inv_ppn … Hf … H1 H H2)
+| /3 width=5 by at_inv_xnn, ex2_intro/
+]
+qed-.
+
+lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g. ⫯g = f → 0 = i2 → ⊥.
+#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
+#x2 #Hg * -i2 #H destruct
+qed-.
+
+lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀j1. ⫯j1 = i1 → 0 = i2 → ⊥.
+#f elim (pn_split f) *
+#g #H #i1 #i2 #Hf #j1 #H1 #H2
+[ elim (at_inv_npp … Hf … H1 H H2)
+| elim (at_inv_xnp … Hf … H H2)
+]
+qed-.
+
+lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → ⫯j2 = i2 →
+ (∃∃g. @⦃j1, g⦄ ≡ j2 & ↑g = f) ∨
+ ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
+#f elim (pn_split f) *
+/4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
+qed-.
+
+lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f →
+ (0 = i1 ∧ 0 = i2) ∨
+ ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2.
+#f * [2: #i1 ] #i2 #Hf #g #H
+[ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
+| >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
+]
+qed-.
+
+lemma at_inv_xpp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f → 0 = i2 → 0 = i1.
+#f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
+#j1 #j2 #_ #_ * -i2 #H destruct
+qed-.
+
+lemma at_inv_xpn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j2. ↑g = f → ⫯j2 = i2 →
+ ∃∃j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1.
+#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f *
+[ #_ * -i2 #H destruct
+| #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i2 →
+ ∃∃g. 0 = i1 & ↑g = f.
+#f elim (pn_split f) *
+#g #H #i1 #i2 #Hf #H2
+[ /3 width=6 by at_inv_xpp, ex2_intro/
+| elim (at_inv_xnp … Hf … H H2)
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2.
+#i2 elim i2 -i2
+[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
+| #i2 #IH * //
+ #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ]
+ /3 width=2 by le_S_S, le_S/
+]
+qed-.
+
+lemma at_increasing_strict: ∀g,i1,i2. @⦃i1, g⦄ ≡ i2 → ∀f. ⫯f = g →
+ i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2.
+#g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
+/4 width=2 by conj, at_increasing, le_S_S/
+qed-.
+
+lemma at_fwd_id_ex: ∀f,i. @⦃i, f⦄ ≡ i → ∃g. ↑g = f.
+#f elim (pn_split f) * /2 width=2 by ex_intro/
+#g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
+#j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
+#H elim (lt_le_false … H) -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+let corec at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2) ≝ ?.
+#i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2
+[ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/
+| #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/
+| #f1 #i1 #i2 #Hf1 #g1 #j2 #H #H2 #f2 #H12 cases (eq_inv_nx … H12 … H) -g1 /3 width=5 by at_next/
+]
+qed-.
+
+lemma at_eq_repl_fwd: ∀i1,i2. eq_repl_fwd (λf. @⦃i1, f⦄ ≡ i2).
+#i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/
+qed-.
+
+lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1.
+#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
+#f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem at_monotonic: ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 →
+ f1 ≗ f2 → i1 < i2 → j1 < j2.
+#j2 elim j2 -j2
+[ #i2 #f2 #Hf2 elim (at_inv_xxp … Hf2) -Hf2 //
+ #g #H21 #_ #j1 #i1 #f1 #_ #_ #Hi elim (lt_le_false … Hi) -Hi //
+| #j2 #IH #i2 #f2 #Hf2 * //
+ #j1 #i1 #f1 #Hf1 #Hf #Hi elim (lt_inv_gen … Hi)
+ #x2 #_ #H21 elim (at_inv_nxn … Hf2 … H21) -Hf2 [1,3: * |*: // ]
+ #g2 #Hg2 #H2
+ [ elim (eq_inv_xp … Hf … H2) -f2
+ #g1 #Hg #H1 elim (at_inv_xpn … Hf1 … H1) -f1
+ /4 width=8 by lt_S_S_to_lt, lt_S_S/
+ | elim (eq_inv_xn … Hf … H2) -f2
+ /4 width=8 by at_inv_xnn, lt_S_S/
+ ]
+]
+qed-.
+
+theorem at_inv_monotonic: ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 →
+ f1 ≗ f2 → j1 < j2 → i1 < i2.
+#j1 elim j1 -j1
+[ #i1 #f1 #Hf1 elim (at_inv_xxp … Hf1) -Hf1 //
+ #g1 * -i1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_O1 … Hj) -Hj
+ #x2 #H22 elim (eq_inv_px … Hf … H1) -f1
+ #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 //
+| #j1 #IH *
+ [ #f1 #Hf1 elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
+ #g1 #Hg1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj
+ elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/
+ | #i1 #f1 #Hf1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj
+ #y2 #Hj #H22 elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ]
+ #g1 #Hg1 #H1
+ [ elim (eq_inv_px … Hf … H1) -f1
+ #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 -H22
+ /3 width=7 by lt_S_S/
+ | elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/
+ ]
+ ]
+]
+qed-.
+
+theorem at_mono: ∀f1,f2. f1 ≗ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1.
+#f1 #f2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_sym/
+qed-.
+
+theorem at_inj: ∀f1,f2. f1 ≗ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2.
+#f1 #f2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_sym/
+qed-.
+
+(* Advanced inversion lemmas on isid ****************************************)
+
+lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
+#i elim i -i
+[ #f #H elim (isid_inv_gen … H) -H /2 width=2 by at_refl/
+| #i #IH #f #H elim (isid_inv_gen … H) -H /3 width=7 by at_push/
+]
+qed.
+
+lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
+/3 width=6 by isid_inv_at, at_mono/ qed-.
+
+(* Advancedd properties on isid *********************************************)
+
+let corec isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄ ≝ ?.
+#f #Hf lapply (Hf 0)
+#H cases (at_fwd_id_ex … H) -H
+#g #H @(isid_push … H) /3 width=7 by at_inv_npn/
+qed-.
+
+(* Advanced properties on id ************************************************)
+
+lemma id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈𝐝 ≗ f.
+/3 width=1 by isid_at, eq_id_inv_isid/ qed-.
+
+lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
+/2 width=1 by isid_inv_at/ 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_2/notation/relations/funexteq_2.ma".
+include "ground_2/relocation/nstream_lift.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive eq: relation rtmap ≝
+| eq_push: ∀f1,f2,g1,g2. eq f1 f2 → ↑f1 = g1 → ↑f2 = g2 → eq g1 g2
+| eq_next: ∀f1,f2,g1,g2. eq f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → eq g1 g2
+.
+
+interpretation "extensional equivalence (rtmap)"
+ 'FunExtEq f1 f2 = (eq f1 f2).
+
+definition eq_repl (R:relation …) ≝
+ ∀f1,f2. f1 ≗ f2 → R f1 f2.
+
+definition eq_repl_back (R:predicate …) ≝
+ ∀f1. R f1 → ∀f2. f1 ≗ f2 → R f2.
+
+definition eq_repl_fwd (R:predicate …) ≝
+ ∀f1. R f1 → ∀f2. f2 ≗ f1 → R f2.
+
+(* Basic properties *********************************************************)
+
+let corec eq_refl: reflexive … eq ≝ ?.
+#f cases (pn_split f) *
+#g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
+qed.
+
+let corec eq_sym: symmetric … eq ≝ ?.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #Hf #H1 #H2
+[ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
+qed-.
+
+lemma eq_repl_sym: ∀R. eq_repl_back R → eq_repl_fwd R.
+/3 width=3 by eq_sym/ qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma eq_inv_px: ∀g1,g2. g1 ≗ g2 → ∀f1. ↑f1 = g1 →
+ ∃∃f2. f1 ≗ f2 & ↑f2 = g2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
+#x1 #H
+[ lapply (injective_push … H) -H /2 width=3 by ex2_intro/
+| elim (discr_push_next … H)
+]
+qed-.
+
+lemma eq_inv_nx: ∀g1,g2. g1 ≗ g2 → ∀f1. ⫯f1 = g1 →
+ ∃∃f2. f1 ≗ f2 & ⫯f2 = g2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
+#x1 #H
+[ elim (discr_next_push … H)
+| lapply (injective_next … H) -H /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma eq_inv_xp: ∀g1,g2. g1 ≗ g2 → ∀f2. ↑f2 = g2 →
+ ∃∃f1. f1 ≗ f2 & ↑f1 = g1.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
+#x2 #H
+[ lapply (injective_push … H) -H /2 width=3 by ex2_intro/
+| elim (discr_push_next … H)
+]
+qed-.
+
+lemma eq_inv_xn: ∀g1,g2. g1 ≗ g2 → ∀f2. ⫯f2 = g2 →
+ ∃∃f1. f1 ≗ f2 & ⫯f1 = g1.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
+#x2 #H
+[ elim (discr_next_push … H)
+| lapply (injective_next … H) -H /2 width=3 by ex2_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma eq_inv_pp: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≗ f2.
+#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
+#x2 #Hx2 * -g2
+#H lapply (injective_push … H) -H //
+qed-.
+
+lemma eq_inv_nn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≗ f2.
+#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
+#x2 #Hx2 * -g2
+#H lapply (injective_next … H) -H //
+qed-.
+
+lemma eq_inv_pn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
+#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
+#x2 #Hx2 * -g2
+#H elim (discr_next_push … H)
+qed-.
+
+lemma eq_inv_np: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
+#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
+#x2 #Hx2 * -g2
+#H elim (discr_push_next … H)
+qed-.
+
+lemma eq_inv_gen: ∀f1,f2. f1 ≗ f2 →
+ (∃∃g1,g2. g1 ≗ g2 & ↑g1 = f1 & ↑g2 = f2) ∨
+ ∃∃g1,g2. g1 ≗ g2 & ⫯g1 = f1 & ⫯g2 = f2.
+#f1 elim (pn_split f1) * #g1 #H1 #f2 #Hf
+[ elim (eq_inv_px … Hf … H1) -Hf /3 width=5 by or_introl, ex3_2_intro/
+| elim (eq_inv_nx … Hf … H1) -Hf /3 width=5 by or_intror, ex3_2_intro/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+let corec eq_trans: Transitive … eq ≝ ?.
+#f1 #f * -f1 -f
+#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
+[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
+/3 width=5 by eq_push, eq_next/
+qed-.
+
+theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2.
+/3 width=3 by eq_trans, eq_sym/ qed-.
+
+theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2.
+/3 width=3 by eq_trans, eq_sym/ 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_2/relocation/nstream_id.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Basic properties *********************************************************)
+
+lemma id_isid: 𝐈⦃𝐈𝐝⦄.
+/3 width=5 by eq_push_isid/ qed.
+
+(* Alternative definition of isid *******************************************)
+
+lemma eq_id_isid: ∀f. 𝐈𝐝 ≗ f → 𝐈⦃f⦄.
+/2 width=3 by isid_eq_repl_back/ qed.
+
+lemma eq_id_inv_isid: ∀f. 𝐈⦃f⦄ → 𝐈𝐝 ≗ f.
+/2 width=1 by isid_inv_eq_repl/ 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_2/notation/relations/isidentity_1.ma".
+include "ground_2/relocation/rtmap_eq.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive isid: predicate rtmap ≝
+| isid_push: ∀f,g. isid f → ↑f = g → isid g
+.
+
+interpretation "test for identity (rtmap)"
+ 'IsIdentity f = (isid f).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isid_inv_gen: ∀g. 𝐈⦃g⦄ → ∃∃f. 𝐈⦃f⦄ & ↑f = g.
+#g * -g
+#f #g #Hf * /2 width=3 by ex2_intro/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma isid_inv_push: ∀g. 𝐈⦃g⦄ → ∀f. ↑f = g → 𝐈⦃f⦄.
+#g #H elim (isid_inv_gen … H) -H
+#f #Hf * -g #g #H >(injective_push … H) -H //
+qed-.
+
+lemma isid_inv_next: ∀g. 𝐈⦃g⦄ → ∀f. ⫯f = g → ⊥.
+#g #H elim (isid_inv_gen … H) -H
+#f #Hf * -g #g #H elim (discr_next_push … H)
+qed-.
+
+let corec isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2 ≝ ?.
+#f1 #f2 #H1 #H2
+cases (isid_inv_gen … H1) -H1
+cases (isid_inv_gen … H2) -H2
+/3 width=5 by eq_push/
+qed-.
+
+(* Basic properties *********************************************************)
+
+let corec isid_eq_repl_back: eq_repl_back … isid ≝ ?.
+#f1 #H cases (isid_inv_gen … H) -H
+#g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px … Hf … H1) -f1
+/3 width=3 by isid_push/
+qed-.
+
+lemma isid_eq_repl_fwd: eq_repl_fwd … isid.
+/3 width=3 by isid_eq_repl_back, eq_repl_sym/ qed-.
+
+(* Alternative definition ***************************************************)
+
+let corec eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄ ≝ ?.
+#f #H cases (eq_inv_px … H) -H /4 width=3 by isid_push, eq_trans/
+qed.
+
+let corec eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f ≝ ?.
+#f * -f
+#f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ]
+@eq_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_2/notation/relations/istotal_1.ma".
+include "ground_2/relocation/rtmap_at.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+definition istot: predicate rtmap ≝ λf. ∀i. ∃j. @⦃i, f⦄ ≡ j.
+
+interpretation "test for totality (rtmap)"
+ 'IsTotal f = (istot f).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma istot_inv_push: ∀g. 𝐓⦃g⦄ → ∀f. ↑f = g → 𝐓⦃f⦄.
+#g #Hg #f #H #i elim (Hg (⫯i)) -Hg
+#j #Hg elim (at_inv_npx … Hg … H) -Hg -H /2 width=3 by ex_intro/
+qed-.
+
+lemma istot_inv_next: ∀g. 𝐓⦃g⦄ → ∀f. ⫯f = g → 𝐓⦃f⦄.
+#g #Hg #f #H #i elim (Hg i) -Hg
+#j #Hg elim (at_inv_xnx … Hg … H) -Hg -H /2 width=2 by ex_intro/
+qed-.
+
+(* Advanced forward lemmas on at ********************************************)
+
+let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ →
+ (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≗ f2 ≝ ?.
+#f1 cases (pn_split f1) * #g1 #H1
+#f2 cases (pn_split f2) * #g2 #H2
+#Hf1 #Hf2 #Hi
+[ @(eq_push … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_push/ -Hf1 -Hf2
+ #i #i1 #i2 #Hg1 #Hg2 lapply (Hi (⫯i) (⫯i1) (⫯i2) ??) /2 width=7 by at_push/
+| cases (Hf2 0) -Hf1 -Hf2 -at_ext
+ #j2 #Hf2 cases (at_increasing_strict … Hf2 … H2) -H2
+ lapply (Hi 0 0 j2 … Hf2) /2 width=2 by at_refl/ -Hi -Hf2 -H1
+ #H2 #H cases (lt_le_false … H) -H //
+| cases (Hf1 0) -Hf1 -Hf2 -at_ext
+ #j1 #Hf1 cases (at_increasing_strict … Hf1 … H1) -H1
+ lapply (Hi 0 j1 0 Hf1 ?) /2 width=2 by at_refl/ -Hi -Hf1 -H2
+ #H1 #H cases (lt_le_false … H) -H //
+| @(eq_next … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_next/ -Hf1 -Hf2
+ #i #i1 #i2 #Hg1 #Hg2 lapply (Hi i (⫯i1) (⫯i2) ??) /2 width=5 by at_next/
+]
+qed-.
+
+(* Main properties on at ****************************************************)
+
+lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2).
+#f #i1 #i2 #Hf lapply (Hf i1) -Hf *
+#j2 #Hf elim (eq_nat_dec i2 j2)
+[ #H destruct /2 width=1 by or_introl/
+| /4 width=6 by at_mono, or_intror/
+]
+qed-.
+
+lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
+#f #i2 #i #Hf elim i -i
+[ #Ht @or_intror * /3 width=3 by at_increasing/
+| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/
+ #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/
+ #H destruct -Ht /2 width=1 by/
+]
+qed-.
+
+lemma is_at_dec: ∀f,i2. 𝐓⦃f⦄ → Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
+#f #i2 #Hf @(is_at_dec_le ?? (⫯i2)) /2 width=4 by lt_le_false/
+qed-.
+
+(* Advanced properties on isid **********************************************)
+
+lemma isid_at_total: ∀f. 𝐓⦃f⦄ → (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄.
+#f #H1f #H2f @isid_at
+#i lapply (H1f i) -H1f *
+#j #Hf >(H2f … Hf) in ⊢ (???%); -H2f //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive sle: relation rtmap ≝
+| sle_push: ∀f1,f2,g1,g2. sle f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sle g1 g2
+| sle_next: ∀f1,f2,g1,g2. sle f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → sle g1 g2
+| sle_weak: ∀f1,f2,g1,g2. sle f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sle g1 g2
+.
+
+interpretation "inclusion (rtmap)"
+ 'subseteq t1 t2 = (sle t1 t2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sle_inv_xp: ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 →
+ ∃∃f1. f1 ⊆ f2 & ↑f1 = g1.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x2 #Hx2 destruct
+[ lapply (injective_push … Hx2) -Hx2 /2 width=3 by ex2_intro/ ]
+elim (discr_push_next … Hx2)
+qed-.
+
+lemma sle_inv_nx: ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 →
+ ∃∃f2. f1 ⊆ f2 & ⫯f2 = g2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #Hx1 destruct
+[2: lapply (injective_next … Hx1) -Hx1 /2 width=3 by ex2_intro/ ]
+elim (discr_next_push … Hx1)
+qed-.
+
+lemma sle_inv_pn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
+[ elim (discr_next_push … Hx2)
+| elim (discr_push_next … Hx1)
+| lapply (injective_push … Hx1) -Hx1
+ lapply (injective_next … Hx2) -Hx2 //
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma sle_inv_pp: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ⊆ f2.
+#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_xp … H … H2) -g2
+#x1 #H #Hx1 destruct lapply (injective_push … Hx1) -Hx1 //
+qed-.
+
+lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
+#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_nx … H … H1) -g1
+#x2 #H #Hx2 destruct lapply (injective_next … Hx2) -Hx2 //
+qed-.
+
+(* properties on isid *******************************************************)
+
+let corec sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2 ≝ ?.
+#f1 * -f1
+#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
+/3 width=5 by sle_weak, sle_push/
+qed.
+
+(* inversion lemmas on isid *************************************************)
+
+let corec sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄ ≝ ?.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #Hf * * #H
+[2,3: elim (isid_inv_next … H) // ]
+lapply (isid_inv_push … H ??) -H
+/3 width=3 by isid_push/
+qed-.
class "grass"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ]
+ [ "rtmap_eq ( ? ≗ ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" * ]
+ [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ]
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
[ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
projects / helm.git / commitdiff