# Zulip Chat Archive

## 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
exists_quadrangle := ⟨.p1, .p2, .p3, .p6, Fano.quadrangle1236⟩
point_line_uniq := Fano.point_line_uniq
```

Having to spell out some of these `collinear`

s and `quadrangle`

s 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
exists_quadrangle := sorry
```

#### 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: Dec 20 2023 at 11:08 UTC