Stream: new members

Topic: a problem about lean4 code

Billlie Franch (Jul 21 2023 at 06:29):

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
have h₁: a - a = a + b := by
sorry
sorry


Can someone help me complete this code?

Johan Commelin (Jul 21 2023 at 06:33):

This is not a complete stand-alone example. See #mwe.

Johan Commelin (Jul 21 2023 at 06:35):

Once you've turned your code into a #mwe, please outline what the next mathematical step is that you would like to take. Then we can explain how to turn it into Lean.

Billlie Franch (Jul 21 2023 at 06:39):

Johan Commelin said:

Once you've turned your code into a #mwe, please outline what the next mathematical step is that you would like to take. Then we can explain how to turn it into Lean.

Sorry, the full code is like this:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
have h₁: a - a = a + b := by
sorry
sorry


Johan Commelin (Jul 21 2023 at 06:40):

This code cannot type check. Without more assumptions on R you can not write things like a + b.

Johan Commelin (Jul 21 2023 at 06:41):

You probably want to assume that R is a group/ring/field or something.

Johan Commelin (Jul 21 2023 at 06:41):

Or maybe you want to use the real numbers, given your list of imports.

Last updated: Dec 20 2023 at 11:08 UTC