How to use conditional in theorem

Stream: lean4

[Ioannis Konstantoulas]

I am trying to apply the theorem Nat.div_eq in the form

let val : n / d = if 0 < d ∧ d ≤ n then (n - d) / d + 1 else 0 := Nat.div_eq n d

I have terms:

d_pos : 0 < d
d_leq : d ≤ n

How do I conclude that I have a term val : n / d = (n-d)/d + 1?

[Damiano Testa]

Probably, use have rather than let. Then rw [if_pos] at this should create a goal where you can use your two hypothesis. Maybe...

[Ioannis Konstantoulas]

I tried something like:

  have con : n / d = if 0 < d ∧ d ≤ n then (n - d) / d + 1 else 0 := Nat.div_eq n d
  have : n / d = (n - d)/d + 1 := by rw [d_pos, d_leq] at con

but it failed:

tactic 'rewrite' failed, equality or iff proof expected
  0 < d
dn: Nat
x✝: 0 < d ∧ d ≤ n
d_pos: 0 < d
d_leq: d ≤ n
con: n / d = if 0 < d ∧ d ≤ n then (n - d) / d + 1 else 0
⊢ n / d = (n - d) / d + 1

Similarly with simp and simp_arith.

[Damiano Testa]

But did you try rw [if_pos] at con?

[Ioannis Konstantoulas]

Oh, I see, I did not know if_pos was a thing. Let me try it.

[Damiano Testa]

if_pos tells Lean to replace the if ... then ... else ... with the then conclusion and a proof of the if clause.

[Ioannis Konstantoulas]

No, I cannot understand how to use this theorem, either in term or tactic mode. In tactic mode, I am trying:

  have d_pos : 0 < d := sorry
  have d_leq : d ≤ n := sorry
  have con : n / d = if 0 < d ∧ d ≤ n then (n - d) / d + 1 else 0 := Nat.div_eq n d
  have : n / d = (n - d)/d + 1 := by
    rw [if_pos] at con

but whatever I try after that, I get errors.

[Ioannis Konstantoulas]

And I cannot see how to feed the assumptions in term mode.

[Ioannis Konstantoulas]

For instance, how would one continue in term mode here:

  have d_pos : 0 < d := sorry
  have d_leq : d ≤ n := sorry
  have arg : 0 < d ∧ d ≤ n := ⟨d_pos, d_leq⟩
  have con : n / d = if 0 < d ∧ d ≤ n then (n - d) / d + 1 else 0 := Nat.div_eq n d
  have : n / d = (n - d)/d + 1 :=
    if_pos arg

[Scott Morrison]

If you post a #mwe I can try.

[Ioannis Konstantoulas]

Thank you Damiano and Scott, I managed to prove the theorem I wanted:

theorem pos_of_div : 0 < d ∧ d ≤ n → 1 ≤ n / d := fun _ =>
  have : n / d = (n - d)/d + 1 := by
    rw [Nat.div_eq n d, if_pos]
    repeat assumption
  calc
    1 ≤ (n - d) / d + 1 := by simp_arith [Nat.zero_le]
    _ = n / d           := this.symm

I am still not quite sure how if_pos works in term mode, I will experiment and see.

[Yakov Pechersky]

if_pos takes arguments and gives back an equality you can use to rewrite/Eq.subst in term mode.

[Damiano Testa]

In this case, you could prove your have as follows:

  have : n / d = (n - d)/d + 1 := (Nat.div_eq n d).trans (if_pos ‹_›)

but I am not sure that this is better than what you have. Also, assigning a name to a hypothesis you use, improves legibility.

[Damiano Testa]

(Also, repeat assumption can be replaced by assumption.)