failed to synthesize instance Membership G ↑(Line ell b c)

Stream: new members

[Abdullah Uyu]

import Mathlib.Tactic

open Set

variable [DecidableEq G]

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

abbrev Line
  (ell : G → G → G → Prop)
  (a b : G) :
    Set G :=
  {c : G | a ≠ b ∧ ell a b c}

abbrev Plane
  [PG : ProjectiveGeometry G ell]
  (a b c : G)
  (δ : Line (ell := ell) b c)
  (a_nin_δ : a ∉ δ) :
    Set G :=
  sUnion {star (ell := ell) a x | x ∈ δ}

Line ell b c is a Set G. What is the problem here?

[Richard Copley]

δ is an element of G along with a proof that δ ∈ Line ell b c. It isn't a set.

[Abdullah Uyu]

Ah, I still confuse this apparently! Thank you.

[Abdullah Uyu]

So should I say (δ := Line (ell := ell) b c) instead?

[Eric Wieser]

No, that means "δ is some arbitrary set which may or may not be Line b c"

[Abdullah Uyu]

Hmm, I just wanted to give it a name, actually, to not repeat the expression again and again.

[Abdullah Uyu]

Yeah it's not actually a parameter, I realize that right now. I use the order of a b c for determining the line.

[Abdullah Uyu]

And why can't I write this?

abbrev Plane
  [ProjectiveGeometry G ell]
  (b c a : G) :
    Set G :=
  sUnion {star (ell := ell) a x | x ∈ Line (ell := ell) b c ∧ a ∉ Line (ell := ell) b c}

[Abdullah Uyu]

Am I doomed with this?

abbrev Plane
  [ProjectiveGeometry G ell]
  (b c a : G)
  (a_nin_δ : a ∉ Line (ell := ell) b c) :
    Set G :=
  sUnion {star (ell := ell) a x | x ∈ Line (ell := ell) b c}

[Abdullah Uyu]

Which naturally has unused variable a_nin_δ.

[Abdullah Uyu]

I guess I will continue with

class Plane
  [ProjectiveGeometry G ell]
  (b c a : G) where
  π : sUnion {star (ell := ell) a x | x ∈ Line (ell := ell) b c}
  a_nin_δ : a ∉ Line (ell := ell) b c

[Abdullah Uyu]

But again I am I made the same mistake. pi is an element of that Set G, right? I want it to be that set.

[Abdullah Uyu]

@Eric Wieser Can I now say π := sUnion ... and it's fine?

class Plane
  [ProjectiveGeometry G ell]
  (b c a : G) where
  π := sUnion {star (ell := ell) a x | x ∈ Line (ell := ell) b c}
  a_nin_δ : a ∉ Line (ell := ell) b c

[Eric Wieser]

No, that has the same problem; a := b means "use b as a default for a" not "a is always b"

[Abdullah Uyu]

@Eric Wieser I guess I have profound misconception, then.

[Abdullah Uyu]

I infer that it's not possible or reasonable. My goal is to write plane that is defined as a subset of the form $\pi = \cup \{ a \star x | x \in \delta \}$, where $\delta \subseteq G$ is a line and $a \in G \setminus \delta$.

[Abdullah Uyu]

I hope I am not overwhelming, but do you think this is fixable?

import Mathlib.Tactic

open Set

namespace Structure

variable [DecidableEq G]

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

abbrev Line
  (ell : G → G → G → Prop)
  (a b : G) :
    Set G :=
  {c : G | a ≠ b ∧ ell a b c}

abbrev Plane
  [ProjectiveGeometry G ell]
  (b c a : G) :
    Set G :=
  /-
  application type mismatch
    And (Line ell b c)
  argument
    Line ell b c
  has type
    Set G : Type ?u.289
  but is expected to have type
    Prop : Type
  -/
  /-
  failed to synthesize instance
    Membership ?m.324 Prop
  -/
  sUnion {(star (ell := ell) a x) : Set G | (x ∈ Line (ell := ell) b c) ∧ (a ∈ Line (ell := ell) b c)}

end Structure