Theorem: interval_shift (Fl.lean)

State before:
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxwy : x ≤ w ∧ w ≤ y ∨ y ≤ w ∧ w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
rcases hxwy with ⟨hxw, hwy⟩ | ⟨hyw, hwx⟩
State after:
case inl.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

case inr.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

State before:
case inl.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

case inr.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
. exact interval_shift₁ npos hfaithful₀ hfaithful₁ hml hfx hfy hfz hfw hzx hzy hyx ht hs₁ hs₂ hxw hwy
State after:
case inr.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

State before:
case inr.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
. exact interval_shift₂ npos hfaithful₀ hfaithful₁ hml hfx hfy hfw hxy ht hs₂ hyw hwx
State after:
no goals

State before:
case inl.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
exact interval_shift₁ npos hfaithful₀ hfaithful₁ hml hfx hfy hfz hfw hzx hzy hyx ht hs₁ hs₂ hxw hwy
State after:
no goals

State before:
case inr.intro
n : ℕ
round : ℕ → ℕ
x y z w s t : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyx : ulp n y ≤ 2 * x
hxy : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
exact interval_shift₂ npos hfaithful₀ hfaithful₁ hml hfx hfy hfw hxy ht hs₂ hyw hwx
State after:
no goals