## Stream: general

### Topic: Modeling the Fano Plane

#### Sebastian Zivota (Jan 24 2023 at 10:02):

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 (Jan 24 2023 at 10:06):

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

#### Sebastian Zivota (Jan 24 2023 at 10:13):

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 (Jan 24 2023 at 10:13):

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

#### Sebastian Zivota (Jan 24 2023 at 10:27):

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 (Jan 24 2023 at 11:01):

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

#### Yaël Dillies (Jan 24 2023 at 11:20):

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 (Jan 24 2023 at 11:21):

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 (Jan 24 2023 at 14:29):

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 (Jan 24 2023 at 16:01):

@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 (Jan 24 2023 at 16:07):

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 (Jan 24 2023 at 16:33):

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 (Jan 24 2023 at 16:35):

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 (Jan 24 2023 at 16:36):

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

#### Kyle Miller (Jan 24 2023 at 16:37):

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 (Jan 24 2023 at 17:11):

Don't we have that instance already for fintypes?

#### Eric Wieser (Jan 24 2023 at 17:11):

Or does deriving Fintype not work yet?

#### Junyan Xu (Jan 24 2023 at 17:12):

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 (Jan 24 2023 at 18:03):

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
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 (Jan 25 2023 at 15:30):

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 (Jan 25 2023 at 15:33):

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

#### Floris van Doorn (Jan 25 2023 at 15:37):

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 (Jan 25 2023 at 16:44):

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 (Jan 25 2023 at 16:56):

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 (Jan 25 2023 at 17:07):

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 (Jan 25 2023 at 17:12):

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 (Jan 25 2023 at 17:40):

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 (Jan 25 2023 at 17:49):

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 (Jan 25 2023 at 17:51):

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 (Jan 25 2023 at 17:54):

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 (Jan 25 2023 at 17:57):

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 (Jan 25 2023 at 17:57):

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 (Jan 25 2023 at 17:58):

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 (Jan 25 2023 at 18:06):

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


#### Kyle Miller (Jan 25 2023 at 18:08):

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 (Jan 25 2023 at 19:20):

@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 (Jan 25 2023 at 19:30):

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 (Jan 25 2023 at 19:30):

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

#### Sebastian Zivota (Jan 25 2023 at 19:31):

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

#### Kyle Miller (Jan 25 2023 at 19:33):

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 (Jan 25 2023 at 19:34):

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

#### Sebastian Zivota (Jan 25 2023 at 19:34):

Yup, that fixed it! Thanks so much!

Last updated: Aug 03 2023 at 10:10 UTC