From 26c71658340519485e2356d20cdca619e1cd4e19 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 13 Feb 2023 22:42:15 +0000 Subject: [PATCH] refactor(combinatorics/configuration): Refactor `projective_plane` to extend `has_points` and `has_lines` (#18436) This PR refactors `projective_plane` to extend `has_points` and `has_lines`. For this to work in Lean3, we need to use `old_structure_cmd`. Co-authored-by: Eric Wieser --- src/combinatorics/configuration.lean | 43 ++++++++++++---------------- 1 file changed, 18 insertions(+), 25 deletions(-) diff --git a/src/combinatorics/configuration.lean b/src/combinatorics/configuration.lean index 36221045516c0..401a530781ab2 100644 --- a/src/combinatorics/configuration.lean +++ b/src/combinatorics/configuration.lean @@ -34,6 +34,8 @@ Together, these four statements say that any two of the following properties imp open_locale big_operators +set_option old_structure_cmd true + namespace configuration variables (P L : Type*) [has_mem P L] @@ -70,7 +72,7 @@ class has_lines extends nondegenerate P L := (mk_line : Π {p₁ p₂ : P} (h : p₁ ≠ p₂), L) (mk_line_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mk_line h ∧ p₂ ∈ mk_line h) -open nondegenerate has_points has_lines +open nondegenerate has_points (mk_point mk_point_ax) has_lines (mk_line mk_line_ax) instance [nondegenerate P L] : nondegenerate (dual L) (dual P) := { exists_point := @exists_line P L _ _, @@ -79,11 +81,13 @@ instance [nondegenerate P L] : nondegenerate (dual L) (dual P) := instance [has_points P L] : has_lines (dual L) (dual P) := { mk_line := @mk_point P L _ _, - mk_line_ax := λ _ _, mk_point_ax } + mk_line_ax := λ _ _, mk_point_ax, + .. dual.nondegenerate _ _ } instance [has_lines P L] : has_points (dual L) (dual P) := { mk_point := @mk_line P L _ _, - mk_point_ax := λ _ _, mk_line_ax } + mk_point_ax := λ _ _, mk_line_ax, + .. dual.nondegenerate _ _ } lemma has_points.exists_unique_point [has_points P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) : ∃! p, p ∈ l₁ ∧ p ∈ l₂ := @@ -292,7 +296,8 @@ let this : ∀ l₁ l₂ : L, l₁ ≠ l₂ → ∃ p : P, p ∈ l₁ ∧ p ∈ exact ⟨q, (congr_arg _ (subtype.ext_iff.mp hq)).mp (mk_line_ax (this q)).2, q.2⟩, end in { mk_point := λ l₁ l₂ hl, classical.some (this l₁ l₂ hl), - mk_point_ax := λ l₁ l₂ hl, classical.some_spec (this l₁ l₂ hl) } + mk_point_ax := λ l₁ l₂ hl, classical.some_spec (this l₁ l₂ hl), + .. ‹has_lines P L› } /-- If a nondegenerate configuration has a unique point on any two lines, and if `|P| = |L|`, then there is a unique line through any two points. -/ @@ -300,41 +305,29 @@ noncomputable def has_points.has_lines [has_points P L] [fintype P] [fintype L] (h : fintype.card P = fintype.card L) : has_lines P L := let this := @has_lines.has_points (dual L) (dual P) _ _ _ _ h.symm in { mk_line := λ _ _, this.mk_point, - mk_line_ax := λ _ _, this.mk_point_ax } + mk_line_ax := λ _ _, this.mk_point_ax, + .. ‹has_points P L› } variables (P L) /-- A projective plane is a nondegenerate configuration in which every pair of lines has an intersection point, every pair of points has a line through them, and which has three points in general position. -/ -class projective_plane extends nondegenerate P L := -(mk_point : Π {l₁ l₂ : L} (h : l₁ ≠ l₂), P) -(mk_point_ax : ∀ {l₁ l₂ : L} (h : l₁ ≠ l₂), mk_point h ∈ l₁ ∧ mk_point h ∈ l₂) -(mk_line : Π {p₁ p₂ : P} (h : p₁ ≠ p₂), L) -(mk_line_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mk_line h ∧ p₂ ∈ mk_line h) +class projective_plane extends has_points P L, has_lines P L := (exists_config : ∃ (p₁ p₂ p₃ : P) (l₁ l₂ l₃ : L), p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃) namespace projective_plane -@[priority 100] -- see Note [lower instance priority] -instance has_points [h : projective_plane P L] : has_points P L := { .. h } - -@[priority 100] -- see Note [lower instance priority] -instance has_lines [h : projective_plane P L] : has_lines P L := { .. h } - variables [projective_plane P L] instance : projective_plane (dual L) (dual P) := -{ mk_line := @mk_point P L _ _, - mk_line_ax := λ _ _, mk_point_ax, - mk_point := @mk_line P L _ _, - mk_point_ax := λ _ _, mk_line_ax, - exists_config := by - { obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := - @exists_config P L _ _, - exact ⟨l₁, l₂, l₃, p₁, p₂, p₃, h₂₁, h₃₁, h₁₂, h₂₂, h₃₂, h₁₃, h₂₃, h₃₃⟩ }, - .. dual.nondegenerate P L } +{ exists_config := + let ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := + @exists_config P L _ _ in + ⟨l₁, l₂, l₃, p₁, p₂, p₃, h₂₁, h₃₁, h₁₂, h₂₂, h₃₂, h₁₃, h₂₃, h₃₃⟩, + .. dual.has_points _ _, + .. dual.has_lines _ _ } /-- The order of a projective plane is one less than the number of lines through an arbitrary point. Equivalently, it is one less than the number of points on an arbitrary line. -/