default operator == for structure ?

Stream: new members

[Jz Pan]

Please forgive me for describing problem in C++ way. I have the following code

structure affine_plane_point (K : Type*) [field K] :=
mk :: (x y : K)

and now I try to prove

P: affine_plane_point K
⊢ P = {x := P.x, y := P.y}

but have no ideas. simp refl library_search and hint are all failed. Do I need to define the operator == for affine_plane_point exilicitly ?

[Johan Commelin]

@Jz Pan cases P

[Johan Commelin]

and then dsimp

[Johan Commelin]

What you want is an "ext lemma"

[Yakov Pechersky]

Would tagging the structure as [ext] work?

[Johan Commelin]

You can search mathlib for [ext] to get examples.

[Johan Commelin]

Aside: note that mathlib has quite a bit on euclidean/affine geometry. What are your plans with affine_plane_point?

[Jz Pan]

My plan is also define projective plane and embed affine plane point into it.

[Jz Pan]

An ad-hoc work for Weierstrass equations.

[Jz Pan]

Thanks. The problem solved with

@[ext]
structure affine_plane_point (K : Type*) [field K] :=
mk :: (x y : K)

and the P = {x := P.x, y := P.y} can be proved by

  rw affine_plane_point.ext_iff,
  simp,

[Johan Commelin]

now that you tagged it with @[ext] you can also use the ext tactic (instead of that rw)

[Johan Commelin]

ext stands for "extensionality", and it means something like "if all the components of two things are equal, then the two things are equal"

[Jz Pan]

I tried ext but it splits the goal into two subgoals. So currently I still prefer rw

[Johan Commelin]

does ext; refl work?

[Jz Pan]

Yes. It works.