Exdending an extension of a class

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

I am getting an error when I extend axioms2, itself being an extension of incidence_geometry. Why is this the case? The error pops up in the following line variable [A3 : axioms3 point]

import  data.set tactic.interactive set_theory.zfc
class incidence_geometry (point : Type):=
(lines : set (set point))
(eqd : point → point → point → point → Prop)

(B: point → point → point → Prop)
[dec_B : ∀ a b c, decidable (B a b c)]
-- Equidistance of 4 Points
(P1 {} : point) (P2 {} : point) (P3 {} : point)

(I1a : ∀ (a b : point), a≠b → ∃ (l ∈  lines) , a∈ l ∧ b∈ l)
open incidence_geometry

variables {point : Type} [A : incidence_geometry point]


class axioms2 (point : Type) extends incidence_geometry point :=
(B1 : ∀ a b c : point, B a b c → B c b a )
open axioms2

variable [A2 : axioms2 point]
include A2

lemma trivi (a b c d: point) : eqd a a a a → eqd a a a a:=
begin
have := B1 a a a,
simp,
end

class axioms3 (point : Type) extends incidence_geometry point :=
(Ax: ∀ (a : point), a=a)
open axioms3



variable [A3 : axioms3 point]
include A3

lemma eqdsym (a b c d: point) : eqd a b c d → eqd c d a b:=
begin
intro hyp,

have := C2 a b a b c d (C4 a b) hyp,
end

[Andre Hernandez-Espiet (Rutgers)]

PS: Maybe this is unnecessary, is there a way to make definitions that require proofs within a class?

[Kevin Buzzard]

In general you should not be naming class instances -- if you need to name them then this might be an indication that they should not be classes but might be better off as structures. Naming class instances means you have to all this include malarkey, and if you include things then you should omit them the moment you don't need to include them any more. None of your imports are relevant. If you remove all your instance names and includes and imports then you get

class incidence_geometry (point : Type):=
(lines : set (set point))
(eqd : point → point → point → point → Prop)

(B: point → point → point → Prop)
[dec_B : ∀ a b c, decidable (B a b c)]
-- Equidistance of 4 Points
(P1 {} : point) (P2 {} : point) (P3 {} : point)

(I1a : ∀ (a b : point), a≠b → ∃ (l ∈  lines) , a∈ l ∧ b∈ l)
open incidence_geometry

variables {point : Type} [incidence_geometry point]


class axioms2 (point : Type) extends incidence_geometry point :=
(B1 : ∀ a b c : point, B a b c → B c b a )
open axioms2

variable [axioms2 point]

lemma trivi (a b c d: point) : eqd a a a a → eqd a a a a:=
begin
  exact id,
end

class axioms3 (point : Type) extends incidence_geometry point :=
(Ax: ∀ (a : point), a=a)
open axioms3



variable [axioms3 point]

lemma eqdsym (a b c d: point) : eqd a b c d → eqd c d a b:=
begin
intro hyp,

have := C2 a b a b c d (C4 a b) hyp,
end

which compiles other than the bit about C2, because there is no C2 defined anywhere in the file.

[Andre Hernandez-Espiet (Rutgers)]

Thanks! I guess I would also like to have a hypothesis like H: l\in lines as part of a theorem. In that case I needed the hypothesis to look something like H\in A.lines, which was already a lot of work. Would using structures avoid these issues? I tried reading about them from https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html , but I was having a hard time turning my class into a structure. Do you recommend me learning from somewhere else?

Also, how do I write latex inside a block of code, like $\in$. I keep having it come out as $$\in$$.

[Alex J. Best]

For the last question, you can just copy and paste the symbols from your lean editor (vscode)

[Alex J. Best]

And a class is a structure already, just a structure tagged with the @[class] attribute, which means it can be automatically inserted, have you read https://leanprover.github.io/theorem_proving_in_lean/type_classes.html ?