Zulip Chat Archive

Stream: new members

Topic: But is it a valid proof?


Dan Piponi (Nov 21 2021 at 02:20):

I have this code

#check sub_self

example (x : ℤ) : x * 0 = 0 :=
calc
  x * 0 = x * (1 - 1)   : by rw sub_self
  ...   = x * 1 - x * 1 : mul_sub x 1 1
  ...   = 0             : sub_self (x * 1)

I run lean filename.lean

And get

sub_self : ∀ (a : ?M_1), a - a = 0

I can't tell if this is telling my attempted proof has failed. Normally I get error or similar if my proof is incorrect. Is this merely an informative message?


Last updated: Dec 20 2023 at 11:08 UTC