playing with lean4

Stream: lean4

[Huỳnh Trần Khanh]

hmm so i have an inductive predicate and a theorem... i have absolutely no idea how to prove this

inductive less : Nat → Nat → Prop
| intro (a : Nat) : less a (a + 1)
| trans { a b c : Nat } : less a b → less b c → less a c

theorem three_le_seven : less 3 7 := by {
  let a := less.intro 3
  let b := less.intro 4
  let c := less.intro 5
  let d := less.intro 6
  let e := less.trans a b
  let f := less.trans e c
  let g := less.trans f d
}

[Huỳnh Trần Khanh]

hmm... so i am not allowed to use exact? this proof works fine

theorem three_le_seven : less 3 7 :=
  less.trans (less.trans (less.trans (less.intro 3) (less.intro 4)) (less.intro 5)) (less.intro 6)

[David Renshaw]

This works for me:

theorem three_le_seven : less 3 7 := by
  let a := less.intro 3
  let b := less.intro 4
  let c := less.intro 5
  let d := less.intro 6
  let e := less.trans a b
  let f := less.trans e c
  let g := less.trans f d
  exact g

[David Renshaw]

I think the curly braces are the problem

[Deniz Aydin]

Here's my general solution:

theorem three_le_thirty_seven : less 3 37 := by
  repeat
  apply less.trans (less.intro _)
  try exact less.intro _

[Huỳnh Trần Khanh]

hmm... now i want to do induction. help me out!

inductive less : Nat → Nat → Prop
| intro (a : Nat) : less a (a + 1)
| trans { a b c : Nat } : less a b → less b c → less a c

theorem i_want_to_be_extremely_general (a b : Nat) : less a (a + (b + 1))
| 0 0 => -- ???

[Deniz Aydin]

I think the induction tactic is what you want for this, and you should only need to do induction on b. Here's a template:

theorem i_want_to_be_extremely_general (a b : Nat) : less a (a + (b + 1))  := by
  induction b with
  | zero =>
    -- tactics here
  | succ n ih =>
    -- tactics here

[Huỳnh Trần Khanh]

thank you. I still feel like a fish out of water. how can I learn Lean 4 aside from guessing random stuff?

[Huỳnh Trần Khanh]

i'm pretty sure the induction thing is not mentioned in the manual, is it?

[Huỳnh Trần Khanh]

oops i was tripping sorry, it is mentioned in the Tactics section. still, any other resources?

[Huỳnh Trần Khanh]

also I'd like to learn lean4 metaprogramming too, I guess lean4 metaprogramming is much nicer right

[Marc Huisinga]

tba-2021 is one possible place to start, but it assumes that you know nothing about interactive theorem proving and it was taught in a lab environment.

[Mario Carneiro]

Now that the kernel has bignum arithmetic, you can supercharge the proof by converting it to a question about Nat.ble:

namespace Nat

inductive less : Nat → Nat → Prop
| intro (a : Nat) : less a (a + 1)
| trans { a b c : Nat } : less a b → less b c → less a c

theorem succ_less_succ {a b : Nat} (h : less a b) : less (succ a) (succ b) := by
  induction h with
  | intro => exact less.intro _
  | trans h₁ h₂ ih₁ ih₂ => exact less.trans ih₁ ih₂

theorem zero_less_succ : (a : Nat) → less 0 (succ a)
| 0 => less.intro _
| succ a => less.trans (zero_less_succ _) (less.intro _)

theorem less_of_le : {a b : _} → ble b a = false → less a b
| 0, succ b, _ => zero_less_succ _
| succ a, succ b, h => succ_less_succ (@less_of_le a b h)

theorem three_le_seven : less 3 7 := less_of_le rfl

theorem bigger :
  less 2330429062458062834620348502348502
       720432084506248560245680248562034852034582304528 := less_of_le rfl

[Huỳnh Trần Khanh]

Does Lean 4 automatically discard false branches? You didn't handle the succ a, 0 and 0, 0 case.

[Huỳnh Trần Khanh]

And yet the proof still works.