What to do to report an error？

Stream: lean4

[👀？]

def foo (x : ℕ) (h : x < 5) : ℕ := x
def bar (x : ℕ) (h : x ≥ 6) : ℕ :=
  if h₀ : x < 4 then
    foo x (by have h₁ : 4 ≤ 5 := by simp
              revert h₀
              revert h₁
              apply le.trans_lt')
  else 0

[Ruben Van de Velde]

What's your question?

[👀？]

contradictory conditions, but do not report borrowing.

[Kevin Buzzard]

What do you think the error is here? I'm assuming the code compiles and it looks ok to me. What you're doing is weird but I see no logical problem with it

[👀？]

How to get lean to warn at h₀

[👀？]

This conditional branch is not possible to execute

[Andrew Yang]

Lean won't know that it is impossible without you proving it first.

[👀？]

example (x : ℕ) (h : x ≥ 6) : bar x = x := sorry

Prove it in this way?

[Kyle Miller]

That gives an error since bar takes two arguments

[Andrew Yang]

If you have a proof of false (h : false) in a conditional branch / goal, you can close the branch / goal by casing on h (or applying h.elim if it works in Lean4).

[Kyle Miller]

Here is a working example of the code so far:

def foo (x : Nat) (h : x < 5) : Nat := x
def bar (x : Nat) (h : x ≥ 6) : Nat :=
  if h₀ : x < 4 then
    foo x (Nat.le.step h₀)
  else 0

example (x : Nat) (h : x ≥ 6) : bar x h = 0 := by
  unfold bar
  split
  · rename_i h'
    apply False.elim
    have := Nat.lt_of_le_of_lt h h'
    simp at this
  · exact rfl

[Kyle Miller]

I had to change the example to prove bar x h = 0 since bar x h = x isn't true.

[Kyle Miller]

Lean won't do analysis for you that cases certain cases are impossible, if this is what you're asking about.

[Kyle Miller]

Another way to write bar is to use False.elim to essentially tell Lean the case can't happen.

def foo (x : Nat) (h : x < 5) : Nat := x
def bar (x : Nat) (h : x ≥ 6) : Nat :=
  if h₀ : x < 4 then
    False.elim $ by { have := Nat.lt_of_le_of_lt h h₀; simp at this }
  else 0

example (x : Nat) (h : x ≥ 6) : bar x h = 0 := by
  unfold bar
  split
  · sorry -- ⊢ False.elim (_ : False) = 0
  · exact rfl

I'm not sure the best way to fill in this sorry though... The term has a proof of False in it, so there's probably some good lemma or tactic for this somewhere.

[Andrew Yang]

There's generalize_proofs in mathlib, and it seems like it is already ported into mathlib 4.

[Mario Carneiro]

Rather than using split, I would just prove that not (x < 4) and simp with it

[Leonardo de Moura]

@Kyle Miller

I'm not sure the best way to fill in this sorry though... The term has a proof of False in it, so there's probably some good lemma or tactic for this somewhere.

You can use contradiction.

[Kyle Miller]

Ah, great, thanks! (For the curious, where it searches for False.elim in the target)