Modeling the Fano Plane

Stream: general

[Sebastian Zivota]

The Fano plane is the smallest projective plane, comprising seven points and seven lines. Three points lie on each line and three lines pass through each point. I am trying to model this structure in lean4 as a pair of types P, L satisfying Membership P L, but my first attempt is turning out extremely tedious and verbose.

inductive FanoPoints where
  <seven constructors p1 … p7>

inductive FanoLines where
  <seven constructors l1 … l7>

Then for the Membership instance I just write down formulas for each of the lines:

instance : Membership FanoPoints FanoLines where
  mem p l := match l with
    | .l1 => p = .p2 ∨ p =.p3 ∨ p = .p6
    | .l2 => p = .p1 ∨ p =.p3 ∨ p = .p4
    […]

This is not very elegant, but bearable. The real problem starts when I try to prove the formula ∀(p q : FanoPoints), ∃ (l : FanoLines), p ∈ l ∧ q ∈ l, i.e. there is a line connecting any two points. I currently have a big case distinction:

match p, q with
    | .p1, .p1 => ⟨.l2, Or.inl rfl, Or.inl rfl⟩
    | .p1, .p2 => ⟨.l3, Or.inl rfl, Or.inr (Or.inl rfl)⟩
    […]

with 49 cases (I haven't written all of them yet).

Is my basic approach sound? Is there a significantly simpler way to do it? Are there ways I can at least have Lean auto-infer the proof part of the existentials I am building in my case distinction, if not the witnesses?

[Johan Commelin]

I think you can derive DecidableEq for FanoPoints. After that, your proofs should hopefully be by decide.

[Sebastian Zivota]

I added the annotation to FanoPoints and FanoLines, but when I try

     | .p1, .p1 => ⟨.l2, by decide, by decide⟩

I get Failed to synthesize Decidable (p1 ∈ FanoLines.l2).

[Johan Commelin]

Right, so after you define membership, you should prove that it's decidable

[Sebastian Zivota]

Ah, I see. So something like this?

instance fanoMemDecidable (p : FanoPoints) (l : FanoLines): Decidable (Membership.mem p l) where
  […]

Would I have to write out every case of (point, line) in this proof?

[Sebastian Zivota]

I got it to work, thank you very much for your help :)

[Yaël Dillies]

You might be interested in Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant to see how they do it in Coq.

[Yaël Dillies]

My personal opinion is that it is terribly ugly and @Bhavik Mehta reimplemented some of Magaud's paper in Lean without the case bashs.

[Mario Carneiro]

isn't there a way to present the fano plane as consisting of the nonzero points of {0,1}^3? (Maybe that's F_2.) I would imagine that using a more uniform representation like that would help to describe the different kinds of lines and points more than a 7-way enumeration

[Kyle Miller]

@Sebastian Zivota It'd probably be better to use an algebraic formulation of the Fano plane, but given your original question this is what I came up with:

inductive FanoPoints where
  | p1 | p2 | p3 | p4 | p5 | p6 | p7
  deriving DecidableEq

inductive FanoLines where
  | l1 | l2 | l3 | l4 | l5 | l6 | l7
  deriving DecidableEq

def FanoLines.points : FanoLines → List FanoPoints
  | .l1 => [.p1, .p2, .p4]
  | .l2 => [.p2, .p3, .p5]
  | .l3 => [.p3, .p4, .p6]
  | .l4 => [.p4, .p5, .p7]
  | .l5 => [.p5, .p6, .p1]
  | .l6 => [.p6, .p7, .p2]
  | .l7 => [.p7, .p1, .p3]

instance FanoMembership : Membership FanoPoints FanoLines where
  mem p l := p ∈ l.points

instance (p : FanoPoints) (l : FanoLines) : Decidable (p ∈ l) := by
  cases l <;> rw [FanoMembership] <;> simp <;> infer_instance

instance (P : FanoLines → Prop) [∀ l, Decidable (P l)] : Decidable (∀ l, P l) :=
  if h : P .l1 ∧ P .l2 ∧ P .l3 ∧ P .l4 ∧ P .l5 ∧ P .l6 ∧ P .l7 then
    isTrue <| by
      repeat
        try rename_i h
        cases h
      intro l
      cases l <;> assumption
  else
    isFalse <| by
      intro H
      apply h
      repeat
        try constructor <;> try apply H

/- mathlib -/
theorem not_forall (p : α → Prop) : ¬ (∀ x, p x) ↔ ∃ x, ¬ p x := sorry

/- mathlib -/
theorem not_exists (p : α → Prop) : ¬ (∃ x, p x) ↔ ∀ x, ¬ p x := sorry

/- mathlib -/
theorem not_not (p : Prop) : ¬¬ p ↔ p := sorry

instance (P : FanoLines → Prop) [∀ l, Decidable (P l)] : Decidable (∃ l, P l) :=
  if h : ∀ l, ¬ P l then
    isFalse <| by simp [not_exists, h]
  else
    isTrue <| by
      simp [not_forall, not_not] at h
      exact h

theorem exists_line (p q : FanoPoints) : ∃ (l : FanoLines), p ∈ l ∧ q ∈ l := by
  cases p <;> cases q <;> decide

[Kyle Miller]

The key Decidable instance here is one for deciding universal quantifiers ∀ (l : FanoLines), P l, which can be done since FanoLines has only finitely many terms.

Then this gives a decidable instance for existentials, and in the end you don't need to go through each of the cases by hand:

theorem exists_line (p q : FanoPoints) : ∃ (l : FanoLines), p ∈ l ∧ q ∈ l := by
  cases p <;> cases q <;> decide

[Sebastian Zivota]

That is really cool, thanks. It didn't occur to me to just use lists for the lines, nor to derive Decidable instances for the quantified formulas. One question though, don't not_forall and not_not turn the entire theory classical (or require it to be such)?

[Kyle Miller]

There are some decidable versions of these in Mathlib that can apply here instead, but I personally don't mind using classical proofs.

[Kyle Miller]

The Decidable instances you get are still computable even if they depend on classical arguments.

[Kyle Miller]

Floris pointed out to me that you can go further and decide the entire proposition with one more instance:

instance (P : FanoPoints → Prop) [∀ l, Decidable (P l)] : Decidable (∀ l, P l) :=
  if h : P .p1 ∧ P .p2 ∧ P .p3 ∧ P .p4 ∧ P .p5 ∧ P .p6 ∧ P .p7 then
    isTrue <| by
      repeat
        try rename_i h
        cases h
      intro l
      cases l <;> assumption
  else
    isFalse <| by
      intro H
      apply h
      repeat
        try constructor <;> try apply H

theorem exists_line : ∀ (p q : FanoPoints), ∃ (l : FanoLines), p ∈ l ∧ q ∈ l := by
  decide

[Eric Wieser]

Don't we have that instance already for fintypes?

[Eric Wieser]

Or does deriving Fintype not work yet?

[Junyan Xu]

Mario Carneiro said:

isn't there a way to present the fano plane as consisting of the nonzero points of {0,1}^3? (Maybe that's F_2.) I would imagine that using a more uniform representation like that would help to describe the different kinds of lines and points more than a 7-way enumeration

Yeah, it's the projective plane over zmod 2. If you use Lean 3 there's docs#projectivization for the points and docs#projectivization.subspace for the lines in mathlib.

[Sebastian Zivota]

Awesome, with that I now have a proof that the Fano plane is indeed a projective plane. (FanoPoints and FanoLines renamed to Fano.Points and Fano.Lines, respectively):

def Fano.exists_connecting_line : ∀ (p q : Points), ∃ l : Lines, p ∈ l ∧ q ∈ l := by
  decide

def Fano.exists_intersection_point : ∀ (l m : Lines), ∃ p : Points, p ∈ l ∧ p ∈ m := by
  decide

theorem Fano.triangle123 : ¬ @collinear _ Lines _ Points.p1 Points.p2 Points.p3 :=
  by simp[collinear]

theorem Fano.triangle126 : ¬ @collinear _ Lines _ Points.p1 Points.p2 Points.p6 :=
  by simp[collinear]

theorem Fano.triangle136 : ¬ @collinear _ Lines _ Points.p1 Points.p3 Points.p6 :=
  by simp[collinear]

theorem Fano.triangle236 : ¬ @collinear _ Lines _ Points.p2 Points.p3 Points.p6 :=
  by simp[collinear]

theorem Fano.quadrangle1236 : @isQuadrangle _ Lines _ Points.p1 Points.p2 Points.p3 Points.p6 :=
  ⟨Fano.triangle123, Fano.triangle126, Fano.triangle136, Fano.triangle236⟩

theorem Fano.point_line_uniq : ∀ {p q : Points} {l m : Lines}, p ∈ l -> q ∈ l -> p ∈ m -> q ∈ m -> p = q ∨ l = m := by
  decide

instance : ProjectivePlane Points Lines where
  exists_connecting_line := Fano.exists_connecting_line
  exists_intersection_point := Fano.exists_intersection_point
  exists_quadrangle := ⟨.p1, .p2, .p3, .p6, Fano.quadrangle1236⟩
  point_line_uniq := Fano.point_line_uniq

Having to spell out some of these collinears and quadrangles is a bit annoying, Lean can't seem to figure out that I want Fano.Lines as the lines type.

[Eric Wieser]

If you find yourself using @ to set an implicit argument (lines) every time you call a function, this is telling you that it should be an explicit argument

[Eric Wieser]

It's hard to suggest better fixes without seeing the rest of your code.

[Floris van Doorn]

Did you define collinear and the other notions yourself? If so, I would change the definitions and start with a structure GeometryData like this

structure GeometryData where
  Points : Type u
  Lines : Type u

def fano : GeometryData :=
  sorry

Next define collinear to take an implicit argument of type GeometryData. Then, if you apply collinear to p : fano.Points, we know what the corresponding type of lines is.

[Sebastian Zivota]

I defined collinear and isQuadrangle purely in terms of membership:

def collinear [Membership P L] (p q r : P) : Prop :=
  ∃ l : L, p ∈ l ∧ q ∈ l ∧ r ∈ l

def isQuadrangle [Membership P L] (p q r s : P) : Prop :=
    ¬ @collinear _ L _ p q r
  ∧ ¬ @collinear _ L _ p q s
  ∧ ¬ @collinear _ L _ p r s
  ∧ ¬ @collinear _ L _ q r s

Then later on I have a type class axiomatizing projective planes:

class ProjectivePlane (P : Type) (L : outParam Type) extends (Membership P L) :=
  exists_connecting_line : ∀ p q : P, ∃ l : L, p ∈ l ∧ q ∈ l
  exists_intersection_point : ∀ l m : L, ∃ p : P, p ∈ l ∧ p ∈ m
  point_line_uniq : ∀ {p q : P} {l m : L}, p ∈ l → q ∈ l → p ∈ m → q ∈ m → p = q ∨ l = m
  exists_quadrangle : ∃ (p q r s : P), @isQuadrangle _ L _ p q r s

If I understand you correctly, Floris, I guess I should introduce the class GeometryData in between Membership and ProjectivePlane?

[Floris van Doorn]

If you want to define collinear in terms of Membership, then the type L has to be explicit: there is no way for Lean to mean what you mean otherwise. However, with GeometryData you have an alternative. Here is a more worked out example (I forgot to add the membership predicate to GeometryData):

structure GeometryData where
  Points : Type u
  Lines : Type u
  membership : Membership Points Lines

attribute [instance] GeometryData.membership

def collinear {G : GeometryData} (p q r : G.Points) : Prop :=
  ∃ l : G.Lines, p ∈ l ∧ q ∈ l ∧ r ∈ l

def isQuadrangle {G : GeometryData} (p q r s : G.Points) : Prop :=
    ¬ collinear p q r
  ∧ ¬ collinear p q s
  ∧ ¬ collinear p r s
  ∧ ¬ collinear q r s

def fano : GeometryData :=
  sorry

[Sebastian Zivota]

I see. I don't really have good intuition for when to use type classes vs structures in Lean yet.

In any case, thank you very much for your help!

[Kevin Buzzard]

Rule of thumb: a class should only have one term, but a structure is allowed to have several terms. For example group G is a class, because it's vanishingly rare that we want to put two different group structures on a type both using * notation, but subgroup G is a structure and not a class, because a general group G can have many subgroups.

[Sebastian Zivota]

I suppose that means it makes sense for ProjectivePlane to be a class, right? I wouldn't expect there to be more than one projective plane with the same points and lines.

[Kyle Miller]

Here's a plausible set of definitions:

class Geometry (P : Type _) where
  line : Type _
  instMem : Membership P line

attribute [instance] Geometry.instMem

def Geometry.collinear [Geometry P] (p q r : P) : Prop :=
  ∃ l : line P, p ∈ l ∧ q ∈ l ∧ r ∈ l

def Geometry.isQuadrangle [Geometry P] (p q r s : P) : Prop :=
    ¬ collinear p q r
  ∧ ¬ collinear p q s
  ∧ ¬ collinear p r s
  ∧ ¬ collinear q r s

class ProjectivePlane (P : Type _) extends Geometry P :=
  exists_connecting_line : ∀ p q : P, ∃ l : line, p ∈ l ∧ q ∈ l
  exists_intersection_point : ∀ l m : line, ∃ p : P, p ∈ l ∧ p ∈ m
  point_line_uniq : ∀ {p q : P} {l m : line}, p ∈ l → q ∈ l → p ∈ m → q ∈ m → p = q ∨ l = m
  exists_quadrangle : ∃ (p q r s : P), Geometry.isQuadrangle p q r s

[Kyle Miller]

The idea is that (likely) if you have a particular type for your points, you will have a particular type in mind for your lines, so the points type determines the lines type.

In general, the binder that introduces a line of points of type P is (l : line P), which reads nicely as "l is a line of points from P".

[Kevin Buzzard]

Setting up the definitions in a way which makes progress painless is a very hard part of Lean for beginners. Once people are proving theorems they can have lots of fun, but if the definitions are wrong then the theorems can be nigh-on impossible to prove.

[Kyle Miller]

One weakness with my suggestion is that it might be more awkward to state things that involve swapping the roles of points and lines in a projective plane, versus exposing both the points and lines as parameters to ProjectivePlane.

[Mario Carneiro]

where "wrong" does not mean "mathematically wrong"! It might be that a definition is totally correct from a mathematical perspective but still hell to work with

[Sebastian Zivota]

Kyle Miller said:

One weakness with my suggestion is that it might be more awkward to state things that involve swapping the roles of points and lines in a projective plane.

Yes, duality is indeed something I have been tinkering with.

[Kyle Miller]

It seems fine:

open Geometry

instance [ProjectivePlane P] : ProjectivePlane (line P) where
  line := P
  instMem := ⟨fun l p ↦ p ∈ l⟩
  exists_connecting_line := ProjectivePlane.exists_intersection_point
  exists_intersection_point := ProjectivePlane.exists_connecting_line
  point_line_uniq := by
    intros
    rw [or_comm]
    apply ProjectivePlane.point_line_uniq <;> assumption
  exists_quadrangle := sorry

[Kyle Miller]

This would have been one of the things I'd have worried about, but it's true by definition (thanks Lean 4!):

example [h : ProjectivePlane P] :
  let h' : ProjectivePlane (line (line P)) := inferInstance
  h = h' := rfl

(The structure of the projective plane of the double dual is the exact same as the original projective plane structure.)

[Sebastian Zivota]

@Kyle Miller with your definition of Geometry and ProjectivePlane, is it possible to write the following definition without explicitly naming the instance? I can't figure out how to get access to line otherwise.

def connectingLine [inst : ProjectivePlane P] (p q : P) : inst.line := Exists.choose (exists_connecting_line p q)

Also, this restructuring somehow breaks the proof that 1236 is a quadrangle in the Fano plane.

theorem Fano.quadrangle1236 : Geometry.isQuadrangle Points.p1 Points.p2 Points.p3 Points.p6 :=
  ⟨by simp[Geometry.collinear], by simp[Geometry.collinear], by simp[Geometry.collinear], by simp[Geometry.collinear]⟩

unsolved goals
P L : Type
⊢ ∀ (x : Geometry.line Points), Points.p1 ∈ x → Points.p2 ∈ x → ¬Points.p3 ∈ x

Also, I pushed the whole thing to github now: https://github.com/loewenheim/projective-plane

[Kyle Miller]

I haven't tested it, but I'd expect it to be

def connectingLine [ProjectivePlane P] (p q : P) : line P := Exists.choose (exists_connecting_line p q)

[Kyle Miller]

That might be Geometry.line if you haven't done open Geometry

[Sebastian Zivota]

Yeah I just realized that I only had to open Geometry for it to work

[Kyle Miller]

With Fano.quadrangle1236 it might be that the decidability instances aren't seeing they can apply to Geometry.line Points universal quantification. Maybe you can just change those simps to simp [Geometry.collinear, Geometry.line]? (I haven't tested this)

[Kyle Miller]

(What I'm thinking is that Geometry.line Points isn't literally Lines, and typeclass inference is syntactically driven.)

[Sebastian Zivota]

Yup, that fixed it! Thanks so much!