Equation In Lean?

Stream: general

[Erika Su]

How is an equation defined in Lean?
For example, an Intuitive polymorphic expression would be (K : field) -> ??? x*x + 1 = 0
Or just reason with (K : field) -> (x : K) -> x * x + 1 = 0 would be sufficient for using? What if i want to implement algorithm about which?
I do find core / init.meta.expr, but i don't quite know its usage.....

[Scott Morrison]

Can I suggest you start with one of the tutorials? Your question doesn't quite make sense, and it's hard to know what you know already and hence what sort of answer would be helpful.

[Scott Morrison]

You don't want to be reading the core files in order to learn Lean. You really need to start with a tutorial.

[Erika Su]

Scott Morrison said:

Can I suggest you start with one of the tutorials? Your question doesn't quite make sense, and it's hard to know what you know already and hence what sort of answer would be helpful.

I have finished reading Theorem Proving in Lean 4 and most part of Functional Programming in Lean and some of the lean manual, and (at least i thought) i understand how to convert Prop, define inductive and quotient object, apply tactics, use typeclass and so on...... If I miss something, please tell me. I suppose you mean converting and reasoning with Subtype predicate already serve the purposes?

[Eric Wieser]

So this is a question about Lean 4 not Lean 3?

[Arthur Correnson]

(deleted)

[Chris Bailey]

Erika Su said:

Scott Morrison said:

Can I suggest you start with one of the tutorials? Your question doesn't quite make sense, and it's hard to know what you know already and hence what sort of answer would be helpful.

I have finished reading Theorem Proving in Lean 4 and most part of Functional Programming in Lean and some of the lean manual, and (at least i thought) i understand how to convert Prop, define inductive and quotient object, apply tactics, use typeclass and so on...... If I miss something, please tell me. I suppose you mean converting and reasoning with (x : Nat) -> p x -> q x already serve the purposes?

I think he's just having a hard time understanding your question. If I understand correctly, you're asking about how to talk about a type or structure that's understood to have certain properties. Lean users generally use type classes for this. I don't know if there's actually a good walkthrough explaining this in depth, but you can kind of get the idea from looking at how some of the algebraic type classes are defined, e.g. https://github.com/leanprover-community/mathlib4/blob/960dc0ee05a539183dbbb745bb0810bfce4c13b5/Mathlib/Algebra/GroupWithZero/Defs.lean#L27

[Kevin Buzzard]

Here is an example of a naive interpretation of your question which is almost certainly not what you mean at all. Let us know what you actually mean. I'll define an equation in Lean below and then prove it's always true. I use Lean 4's maths library mathlib4. We don't have fields yet, but we have commutative rings, and fields are a special case. We have fields in Lean 3's mathlib.

import Mathlib.Tactic.Ring

example (R : Type) [CommRing R] (a b : R) :
  -- an equation
  (a + b)^2 = a^2 + 2*a*b + b^2 :=
  -- a proof
by ring

[Kevin Buzzard]

If you can ask your question by writing Lean code then it's often easier to understand more quickly what you actually want to know. You can post code using #backticks .