What can be in a structure?

Stream: new members

[Moti Ben-Ari]

(Please ignore my previous message.)

Can a Prop be in a structure? In the MWE below, the structure is OK until the declaration of mid which is not an equation or type but a Prop. The error is unexpected token namespace, expected ,.

I have tried writing it as a separate definition which is accepted:

def mid (A B : Point) : Prop :=
  A ≠ B → ∃ C : Point, Plane.btw A C B

but then I can't use it in the lemma below. Since it is an implication of the form P→Q, I should be able to apply it since the goal is Q and then the goal will be P which is the hypothesis h, but I get the error failed to unify.

import Mathlib.Tactic
import Mathlib.Data.Real.NNReal

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

structure Cartesian_Plane where
  P : Set Point
  d : Point → Point → NNReal
  zero : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A
  btw : ∀ A B C : Point, d A C = d A B + d B C
  mid : ∀ A B : Point, A ≠ B → ∃ C Point : btw A C B

namespace Cartesian_Plane
variable (Plane : Cartesian_Plane)

lemma L (A B : Point) (h : A ≠ B) : ∃ C : Point, Plane.btw A C B := by
  apply Plane.mid A B

[Eric Rodriguez]

I think mid should be spelt ∃ (C : Point), btw A C B, or slightly less clearly ∃ C, btw A C B. Note that zero, symm, and btw are all Props/

[Moti Ben-Ari]

Eric Rodriguez said:

I think mid should be spelt ∃ (C : Point), btw A C B, or slightly less clearly ∃ C, btw A C B. Note that zero, symm, and btw are all Props/

I get:

type mismatch
  btw A C B
has type
  d A B = d A C + d C B : Prop
but is expected to have type
  Prop : Type

[Logan Murphy]

The term btw A B C is a proof of d A C = d A B + d B C, not the proposition itself. I think instead, btw should be defined as a predicate (i.e., a Prop-valued function rather than a proof-valued function).

Since it seems like the type of btw is intending to define what "between" means, one option is to just use that definition in the specification of mid:

structure Cartesian_Plane where
  P : Set Point
  d : Point → Point → NNReal
  zero : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A
  mid : ∀ A B : Point, A ≠ B → ∃ C: Point, d A C = d A B + d B C

If you want to keep the spelling/name btw, you can also abstract it out of the structure definition:

def btw (d : Point → Point → NNReal) (A B C : Point) : Prop :=
 d A C = d A B + d B C

structure Cartesian_Plane where
  P : Set Point
  d : Point → Point → NNReal
  zero : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A
  mid : ∀ A B : Point, A ≠ B → ∃ C: Point, btw d A B C

[Matt Diamond]

something seems a bit off about the Cartesian_Plane definition... the set of points P isn't referenced in any of the other fields

[Matt Diamond]

maybe it's unnecessary?

at the same time, I understand the desire to specify the points in the plane

just seems odd to define a structure where there's a carrier set but nothing else references it... it makes me think there's some confusion in the design

just my 2 cents

[Moti Ben-Ari]

Matt Diamond said:

maybe it's unnecessary?

at the same time, I understand the desire to specify the points in the plane

just seems odd to define a structure where there's a carrier set but nothing else references it... it makes me think there's some confusion in the design

just my 2 cents

Yes. It works without P. I was naively copying the definition in the book that a Plane is a set of points and a distance function.

[Moti Ben-Ari]

Logan Murphy said:

If you want to keep the spelling/name btw, you can also abstract it out of the structure definition:

def btw (d : Point → Point → NNReal) (A B C : Point) : Prop :=
 d A C = d A B + d B C

structure Cartesian_Plane where
  P : Set Point
  d : Point → Point → NNReal
  zero : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A
  mid : ∀ A B : Point, A ≠ B → ∃ C: Point, btw d A B C

The problem with this is that I have to keep giving the parameter d at every use. I would prefer if all definitions and axioms could be encapsulated in one structure. This is keeping too confusing for me so I'lll drop it :sad:

[Matt Diamond]

@Moti Ben-Ari Don't be discouraged! You could do this:

structure Cartesian_Plane where
  d : Point → Point → NNReal
  zero : ∀ A : Point, d A A = 0
  symm : ∀ A B : Point, d A B = d B A
  btw := fun (A B C) => d A C = d A B + d B C
  mid : ∀ A B : Point, A ≠ B → ∃ C : Point, btw A B C

though it does mean that someone instantiating their own instance of Cartesian_Plane would be able to define btw however they wanted. I wonder if there's a way to define a structure field as derived and read-only...