Edward van de Meent

Stream: new members

[Edward van de Meent]

Hi everyone, I'm an undergraduate Utrecht University, i will be working with Lean for my bachelors thesis (under supervision of @Johan Commelin ). my study is mathematics, with a minor of computer science.

i was doing some preparation for my thesis, which includes creating an instance of the field of order four. taking inspiration from Mathematics in Lean, i defined a struct, made instances of One, Zero, Add, Mul, Sub, but now i'm at the part where it says we can prove therorems like

theorem zero_def : (0 : gaussInt) = ⟨0, 0⟩ :=
  rfl

so i tried to do the same for my definition of F4, but it complains about a type mismatch? my instance of zero is with this code:

instance :Zero F4 := ⟨0,0⟩

and i'm getting this error:
image.png
can someone explain what this error means, why it is supposed to work for the tutorial, and why it doesn't work for my instance?

[Eric Wieser]

You're confusing rfl and refl

[Eric Wieser]

refl _ (with the underscore) is the same as rfl

[Edward van de Meent]

what's the difference?

[Eric Wieser]

The _. It's really important to know how to read the error message you got there. It is telling you "you wrote refl but there's a ∀ left over; so I bet you meant refl _"

[Kevin Buzzard]

The error says "what you wrote has type "for all (something), x = y", and you were supposed to give me something of type "x=y" ", so what it means is "please supply the something"

[Edward van de Meent]

then the _ means that you don't care what example of quantification you use?

[Eric Wieser]

No, it means "I don't know what to put here; work it out automatically if you can, error if you can't"

[Edward van de Meent]

right... if i wanted to be explicit, what should i put there?

[Eric Wieser]

You can #print your proof afterwards to see what lean put there for you

[Eric Wieser]

But you really should not care about being explicit here

[Edward van de Meent]

Thanks!

[Eric Wieser]

You could probably put something stupid like (0 + 0 + 0) if you really wanted, which shows that the explicitness is worthless

[Edward van de Meent]

yea, it says { x0 := 0, x1 := 0 }, that's not helpful at all :sweat_smile: