Theorem: round_le_round (Fl/Round.lean)

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
⊢ round b ≤ round a
Tactic:
have lolo : trunc n b ≤ trunc n a := trunc_le_trunc npos hba
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
⊢ round b ≤ round a

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
⊢ round b ≤ round a
Tactic:
have lohi : trunc n b ≤ next n (trunc n a) :=
  Nat.le_trans lolo (Nat.le_add_right _ _)
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
⊢ round b ≤ round a

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
⊢ round b ≤ round a
Tactic:
have hihi : next n (trunc n b) ≤ next n (trunc n a) :=
  Nat.add_le_add lolo (ulp_le_ulp n lolo)
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
⊢ round b ≤ round a

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
⊢ round b ≤ round a
Tactic:
rcases hfaithful₁ b, (hfaithful₁ a).symm with ⟨blo | bhi, ahi | alo⟩
State after:
case inl.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a

State before:
case inl.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
. rwa [blo, ahi]
State after:
case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a

State before:
case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a

case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
. rwa [blo, alo]
State after:
case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a

State before:
case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a

case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
. rwa [bhi, ahi]
State after:
case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a

State before:
case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
. cases eq_or_ne b a with
  | inl eq => exact eq ▸ le_rfl
  | inr ne =>
    rewrite [bhi, alo]
    apply Nat.le_of_not_lt
    intro (lt_next_trunc : trunc n a < next n (trunc n b))
    have trunc_eq : trunc n a = trunc n b := by
      apply Nat.le_antisymm
      . rewrite [← trunc_idempotent npos a]
        exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
      . exact lolo
    have ulp_eq : ulp n a = ulp n b := by
      rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
    apply Nat.lt_le_asymm (lt_of_le_of_ne hba ne)
    trans trunc n a + ulp n a / 2
    . exact le_midpoint_of_round_eq_trunc npos hcorrect₀ alo
    . rewrite [trunc_eq, ulp_eq]
      exact midpoint_le_of_round_eq_next_trunc npos hcorrect₁ bhi
State after:
no goals

State before:
case inl.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a
Tactic:
rwa [blo, ahi]
State after:
no goals

State before:
case inl.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
blo : round b = trunc n b
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
rwa [blo, alo]
State after:
no goals

State before:
case inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
ahi : round a = next n (trunc n a)
⊢ round b ≤ round a
Tactic:
rwa [bhi, ahi]
State after:
no goals

State before:
case inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
⊢ round b ≤ round a
Tactic:
cases eq_or_ne b a with
| inl eq => exact eq ▸ le_rfl
| inr ne =>
  rewrite [bhi, alo]
  apply Nat.le_of_not_lt
  intro (lt_next_trunc : trunc n a < next n (trunc n b))
  have trunc_eq : trunc n a = trunc n b := by
    apply Nat.le_antisymm
    . rewrite [← trunc_idempotent npos a]
      exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
    . exact lolo
  have ulp_eq : ulp n a = ulp n b := by
    rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
  apply Nat.lt_le_asymm (lt_of_le_of_ne hba ne)
  trans trunc n a + ulp n a / 2
  . exact le_midpoint_of_round_eq_trunc npos hcorrect₀ alo
  . rewrite [trunc_eq, ulp_eq]
    exact midpoint_le_of_round_eq_next_trunc npos hcorrect₁ bhi
State after:
no goals

State before:
case inr.inr.inl
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
eq : b = a
⊢ round b ≤ round a
Tactic:
exact eq ▸ le_rfl
State after:
no goals

State before:
case inr.inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
⊢ round b ≤ round a
Tactic:
rewrite [bhi, alo]
State after:
case inr.inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
⊢ next n (trunc n b) ≤ trunc n a

State before:
case inr.inr.inr
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
⊢ next n (trunc n b) ≤ trunc n a
Tactic:
apply Nat.le_of_not_lt
State after:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
⊢ ¬trunc n a < next n (trunc n b)

State before:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
⊢ ¬trunc n a < next n (trunc n b)
Tactic:
intro (lt_next_trunc : trunc n a < next n (trunc n b))
State after:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ False

State before:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ False
Tactic:
have trunc_eq : trunc n a = trunc n b := by
  apply Nat.le_antisymm
  . rewrite [← trunc_idempotent npos a]
    exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
  . exact lolo
State after:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
⊢ False

State before:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
⊢ False
Tactic:
have ulp_eq : ulp n a = ulp n b := by
  rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
State after:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ False

State before:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ False
Tactic:
apply Nat.lt_le_asymm (lt_of_le_of_ne hba ne)
State after:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ a ≤ b

State before:
case inr.inr.inr.a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ a ≤ b
Tactic:
trans trunc n a + ulp n a / 2
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ a ≤ trunc n a + ulp n a / 2

n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n a + ulp n a / 2 ≤ b

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ a ≤ trunc n a + ulp n a / 2

n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n a + ulp n a / 2 ≤ b
Tactic:
. exact le_midpoint_of_round_eq_trunc npos hcorrect₀ alo
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n a + ulp n a / 2 ≤ b

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n a + ulp n a / 2 ≤ b
Tactic:
. rewrite [trunc_eq, ulp_eq]
  exact midpoint_le_of_round_eq_next_trunc npos hcorrect₁ bhi
State after:
no goals

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n a = trunc n b
Tactic:
apply Nat.le_antisymm
State after:
case h₁
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n a ≤ trunc n b

case h₂
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n b ≤ trunc n a

State before:
case h₁
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n a ≤ trunc n b

case h₂
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n b ≤ trunc n a
Tactic:
. rewrite [← trunc_idempotent npos a]
  exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
State after:
case h₂
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n b ≤ trunc n a

State before:
case h₂
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n b ≤ trunc n a
Tactic:
. exact lolo
State after:
no goals

State before:
case h₁
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n a ≤ trunc n b
Tactic:
rewrite [← trunc_idempotent npos a]
State after:
case h₁
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n (trunc n a) ≤ trunc n b

State before:
case h₁
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n (trunc n a) ≤ trunc n b
Tactic:
exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
State after:
no goals

State before:
case h₂
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
⊢ trunc n b ≤ trunc n a
Tactic:
exact lolo
State after:
no goals

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
⊢ ulp n a = ulp n b
Tactic:
rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
State after:
no goals

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ a ≤ trunc n a + ulp n a / 2
Tactic:
exact le_midpoint_of_round_eq_trunc npos hcorrect₀ alo
State after:
no goals

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n a + ulp n a / 2 ≤ b
Tactic:
rewrite [trunc_eq, ulp_eq]
State after:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n b + ulp n b / 2 ≤ b

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
ulp_eq : ulp n a = ulp n b
⊢ trunc n b + ulp n b / 2 ≤ b
Tactic:
exact midpoint_le_of_round_eq_next_trunc npos hcorrect₁ bhi
State after:
no goals