lean4 calc developments with simp

Stream: new members

[Augustin d'Oultremont]

Hi ! I started 2 months ago in lean4 (without any prior experience in theorem proving languages, but a good experience in programming), and I encountered a timeout at 'whnf', maximum number of heartbeats (50000) has been reached error using simp.

I am trying to automate solving equalities like (3 * k + 2)^2 = 3 * (3 * k^2 + 4 * k + 1) + 1 using simp. For now, I've added a handful of very basic theorems (listed below), that are sufficient to solve it (works with set_option maxHeartbeats 350000).

My current method solves (3 * k + 1)^2 = 3 * (3 * k^2 + 2 * k) + 1 without problems (with the default maxHeartbeats 50000). For context : I'm trying to prove a % b ≠ 0 → (q^2 % 3 = 1) by development on the different cases, hence the two examples given.

Reading @Leonardo de Moura's response at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/New.20simp.20feature, and other topics (following the trace and trying to understand the process), I get the impression that

• the theorems I've added are too basic and thus require a big development
• developments like that would need better theorems / methods to work well
• mathlib4 might solve the problem but it seems like the theorems that I would need are not implemented yet

Could a more experienced leaner give me a clue on whether this would need (the fully ported) mathlib4 or how to make it work without it (with only the current mathlib4 or only basic lean) ?

Thanks a lot !
Augustin

:down:️ the theorems added to simp

attribute [simp]
    -- addition
      -- swapping
      Nat.add_assoc
      Nat.add_comm
      Nat.add_left_comm
      -- zero & one
      Nat.add_zero
      Nat.zero_add
    -- multiplication
      -- succ
      Nat.mul_succ
      Nat.succ_mul
      -- swapping
      Nat.mul_assoc
      Nat.mul_comm
      Nat.mul_left_comm
      -- zero & one
      Nat.mul_zero
      Nat.zero_mul
      Nat.mul_one
      Nat.one_mul
    -- powers
      -- zero & one
      Nat.pow_zero
      -- succ
      Nat.pow_succ
    -- multiplication to addition
    Nat.left_distrib
    Nat.right_distrib

[Mario Carneiro]

have you met tactic#ring?

[Mario Carneiro]

also you should show a #mwe

[Augustin d'Oultremont]

Mario Carneiro said:

also you should show a #mwe

Sorry about that, here it is :

attribute [simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm Nat.add_zero Nat.zero_add Nat.mul_succ Nat.succ_mul Nat.mul_assoc Nat.mul_comm Nat.mul_left_comm Nat.mul_zero Nat.zero_mul Nat.mul_one Nat.one_mul Nat.pow_zero Nat.pow_succ Nat.left_distrib Nat.right_distrib

-- simple example
example (k : Nat) : (3 * k + 1)^2 = 3 * (3 * k^2 + 2 * k) + 1 := by simp

-- more complex, only works with set_option maxHeartbeats 350000
set_option maxHeartbeats 350000
example (k : Nat) : (3 * k + 2)^2 = 3 * (3 * k^2 + 4 * k + 1) + 1 := by simp

[Mario Carneiro]

to get a sense for why this proof method is so terrible, note that the normal form worked out in the first example is

        (k +
          (k +
            (k +
              (k +
                (k +
                  (k +
                    (k * k + (k * k + (k * k + (k * k + (k * k + (k * k + (k * k + (k * k + (k * k + 1))))))))))))))))

[Mario Carneiro]

ring knows about scalar multiples and performs much better on these goals (and is ultimately what we want to use here)

[Mario Carneiro]

mathlib4 already has the ring tactic well enough for these examples

import Mathlib.Tactic.Ring

example (k : Nat) : (3 * k + 1)^2 = 3 * (3 * k^2 + 2 * k) + 1 := by ring
example (k : Nat) : (3 * k + 2)^2 = 3 * (3 * k^2 + 4 * k + 1) + 1 := by ring