Define a relation p over X ?

Stream: general

[Mason McBride]

Hey gang, here is my mwe:

universe u v
variable {α : Sort u} {β : Sort v}
def Relation (p : β → β → Prop) (X : β): X → X → Prop := ∀ ⦃x y⦄, p x y

It's telling me "type expected, got (X : β)"
If had another theorem I want to be able to write theorem ... (h: Relation p X) : ... := ... for example? thoughts?

[Yaël Dillies]

What should X → X → Prop mean if X is a β?

[Yaël Dillies]

Did you mean to write

universe v
variable {β : Sort v}
def Relation (p : β → β → Prop) : Prop := ∀ ⦃x y⦄, p x y

[Mason McBride]

p: X, X -> Prop
x, y |-> p(x,y)

[Yaël Dillies]

Okay, but X is not a type, it might be eg a natural number (if you pick β = ℕ).

[Mason McBride]

I want to define a relation over a set X. I was using Beta so I could define relations over Y too if I wanted. How would I change my definition

[Mason McBride]

Yaël Dillies said:

Did you mean to write

universe v
variable {β : Sort v}
def Relation (p : β → β → Prop) : Prop := ∀ ⦃x y⦄, p x y

I want to use this as a definition to prove theorems like "if p is a preorder relation, then p /\ p^op is an equivalence relation and I don't think I could do that with your definition

[Yaël Dillies]

Okay, what about

universe v
variable {X : Sort v}
def Relation (p : X → X → Prop) : Prop := ∀ ⦃x y⦄, p x y

def IsPreorder (p : X → X → Prop) : Prop := sorry

lemma foo {p : X → X → Prop} (hp : IsPreorder p) :
    IsPreorder (fun x y => p x y ∧ p y x) := sorry

[Mason McBride]

universe v
variable {X : Sort v}
def Relation (p : X → X → Prop) : Prop := ∀ ⦃x y⦄, p x y
def Transitive (p : X → X → Prop) : Prop := sorry
def Reflexive (p : X → X → Prop) : Prop := sorry
def Preorder (p : X → X → Prop) : Prop := Transitive p ∧ Reflexive p

lemma foo {p : X → X → Prop} (hp : Preorder p) :
  Preorder (fun x y => p x y ∧ p y x) := sorry

I'm getting an error on my defintion of Preorder

[Kevin Buzzard]

And what is the error?

[Mason McBride]

universe v
variable {X : Sort v}
def Relation (p : X → X → Prop) : Prop := ∀ ⦃x y⦄, p x y
def Transitive (p : X → X → Prop) : Prop := sorry
def Reflexive (p : X → X → Prop) : Prop := sorry
def Symmetric (p : X → X → Prop) : Prop := sorry
def Preorder (p : X → X → Prop) : Prop := Transitive p ∧ Reflexive p
def Equiv (p : X → X → Prop) : Prop := Preorder p ∧ Symmetric p

lemma foo {p : X → X → Prop} (hp : Preorder p) :
  Equiv (fun x y => p x y ∧ p y x) := sorry

This is the actual statement I'm looking for but I'm not sure this is correct lean. My vscode gives me red squiggles under Symmetric p

[Mason McBride]

Screenshot-2023-11-14-at-12.37.15-PM.png

[Mason McBride]

also while you are all here, what tactic should I use to prove that the function provided is Transitive, Reflexive, and Symmetric. I feel like they (you) removed split or cases in lean4

[Kevin Buzzard]

If lean is expecting a function at Symmetric p then that means that the thing after Symmetric p is being interpreted as an input to a function. The thing after it is lemma which isn't a thing in lean 4 so that's probably the issue

[Mason McBride]

oh awesome the squiggles are gone

[Mason McBride]

Screenshot-2023-11-14-at-12.40.39-PM.png
Will you prove this for me if I tell you I beat your natural number game like 1.5 years ago?

[Kevin Buzzard]

They didn't remove split or cases, they renamed split to constructor and cases is still there but has a slightly different syntax.

[Kevin Buzzard]

I can't prove anything for you because I'm on mobile (that was why I asked for the error message)

[Kevin Buzzard]

It doesn't look too difficult to prove though. Start with constructor

[Kevin Buzzard]

And then unfold everything and use tauto or aesop or something?

[Mason McBride]

section Relation
universe v
variable {X : Sort v}
def Relation (p : X → X → Prop) : Prop := ∀⦃x y⦄, p x y

def Reflexive (p : X → X → Prop) : Prop := ∀x, p x x
def Transitive (p : X → X → Prop) : Prop := ∀⦃x y z⦄, p x y ∧ p y z → p x z
def Symmetric (p : X → X → Prop) : Prop := ∀⦃x y⦄, p x y → p y x
def Preorder (p : X → X → Prop) : Prop := Transitive p ∧ Reflexive p
def Equiv (p : X → X → Prop) : Prop := (Transitive p) ∧ (Reflexive p) ∧ (Symmetric p)

theorem Ex5a {p : X → X → Prop} (hp : Preorder p):
  Reflexive (fun x y => p x y ∧ p y x) := by
  intro x
  exact ⟨hp.right x, hp.right x⟩

theorem Ex5b {p : X → X → Prop} (hp : Preorder p):
  Symmetric (fun x y => p x y ∧ p y x) := by
  intro x y expr
  exact ⟨expr.right, expr.left⟩

theorem Ex5c {p : X → X → Prop} (hp : Preorder p):
  Transitive (fun x y => p x y ∧ p y x) := by
  intro x y z expr
  have p_trans := hp.left
  have pxz : p x z := by exact p_trans ⟨expr.left.left, expr.right.left⟩
  have pzx : p z x := by exact p_trans ⟨expr.right.right, expr.left.right⟩
  exact ⟨pxz, pzx⟩

theorem Ex5 {p : X → X → Prop} (hp : Preorder p):
  Equiv (fun x y => p x y ∧ p y x) := by
  exact ⟨Ex5c hp, ⟨Ex5a hp, Ex5b hp⟩⟩
end Relation