Using implicit parameters

Stream: new members

[Moti Ben-Ari]

I want to prove theorems from the textbook
A Full Axiomatic Development of High School Geometry

I am using explicit parameters Pln.d A C = Pln.d A B + Pln.d B C because the implicit parameter variable {Pln: Plane} gives the error message application type mismatch for Pln.d A C. And similarly for using a proposition from the structure symm Pln B A. Here is a MWE

import Mathlib.Tactic
import Mathlib.Data.Real.NNReal
namespace Geometry

@[ext]
structure Point where
  x : ℝ
  y : ℝ

structure Plane where
  P : Set Point
  d : Point → Point → NNReal
  refl : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A

namespace Plane
variable {Pln : Plane}

def btw (A B C : Point) :=
  Pln.d A C = Pln.d A B + Pln.d B C

lemma sym (A B C : Point) :
    Pln.btw A B C → Pln.btw C B A := by
  intro h
  rw [btw]
  rw [symm Pln B A, symm Pln C B, symm Pln C A, add_comm]
  rw [← btw]
  exact h
  done

def seg (A B : Point) :=
  {A, B} ∪ {D : Point | Pln.btw A D B}

def ray (A B : Point) :=
  {A, B} ∪ {D : Point | Pln.btw A D B ∨ Pln.btw A B D}

def line (A B : Point) :=
  {A, B} ∪ {D : Point | Pln.btw A D B ∨ Pln.btw A B D ∨ Pln.btw D A B}

[Nicolau Oliver]

I am also interested on learning Lean by proving theorems on axiomatic geometry, and later even going later into axiomatic geometry.

Will try to check out the error on your code next month, but I would be grateful to be updated if you make any progress or find similar projects/people working on this