# Lean Proving a Prop that has a match

I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem into this MVE:

import Mathlib.SetTheory.Ordinal.Basic
import Mathlib.SetTheory.Ordinal.Arithmetic
import Init.Prelude
import Mathlib.Init.Logic
import Mathlib.Order.SuccPred.Basic

inductive Maxx: Ordinal.{u} → Type (u+1)
| mk (a b: Ordinal) : Maxx (max a b)

theorem max_succ_max : {α β : Ordinal} → max (Order.succ (max α β)) β = Order.succ (max α β) := by
intro a b
rw [succ_max, max_assoc, max_eq_left_of_lt (Order.lt_succ b)]

def succ {a: Ordinal} (m: Maxx a) : Maxx (Order.succ a) :=
match m with
| Maxx.mk a2 b => (max_succ_max) ▸ Maxx.mk ((max a2 b)+1) (b)

def zerom : Maxx 0 := (Ordinal.max_zero_right 0) ▸ Maxx.mk 0 0
def onem : Maxx 1 := (Ordinal.max_zero_right 1) ▸ Maxx.mk 1 0

def is_eq {a b: Ordinal} (m1: Maxx a) (m2: Maxx b) : Prop :=
match m1 with
| Maxx.mk m1a m1b =>
match m2 with
| Maxx.mk m2a m2b => m1a=m2a ∧ m1b=m2b

theorem m_succ_zero_eq_one : is_eq (succ zerom) onem := by
rw [is_eq, succ, zerom, onem]
split
. case _ am mx mxl mxr maxmx heq =>
split
. case _ an nx nxl nxr maxnx heq2 =>
apply And.intro


I am having trouble proving anything from here, as I have hypotheses

am : Ordinal.{u_1}
mx : Maxx am
mxl mxr : Ordinal.{u_1}
maxmx : Order.succ 0 = max mxl mxr
heq : HEq
(match 0, zerom.proof_1 ▸ Maxx.mk 0 0 with
| .(max a2 b), Maxx.mk a2 b => ⋯ ▸ Maxx.mk (max a2 b + 1) b)
(Maxx.mk mxl mxr)
an : Ordinal.{u_1}
nx : Maxx an
nxl nxr : Ordinal.{u_1}
maxnx : 1 = max nxl nxr
heq2 : HEq (onem.proof_1 ▸ Maxx.mk 1 0) (Maxx.mk nxl nxr)


And want to destructure the match here, but I do not know how. I also want to know how to show that proof ▸ Maxx.mk objects are always still Maxx.mk, but I don't know how. It is basically true by definition since zerom is Maxx.mk 0 0, onem is Maxx.mk 1 0, and succ adds one to the first term. How can I prove m_succ_zero_eq_one?

• I think the way you defined Maxx c is going to give you a lot of pain because you need to work with HEq instead of equality since Maxx.mk a b and Maxx.mk a' b' have syntactically different (but possibly equal) types when max a b = max a' b'. What if you defined it instead as def Maxx (c : Ordinal.{u}) : Type (u+1) := {p : Ordinal × Ordinal // max p.1 p.2 = c}? So each element of Maxx c is the two elements of the pair plus a proof of equality. I think it will be easier to work with that proof explicitly instead of implicitly like you are currently doing. Commented Jul 15 at 2:31
• If you like I can turn my comment into an answer. I just want to make sure it is an acceptable path forward. (One can also use a structure instead of a subtype. It is basically the same thing! The structure would have three parts: a: Ordinal, b: Ordinal, and a proof of a + b = c.) Commented Jul 15 at 2:39

Turning my comment into an answer... Notice in your code, for every function on Maxx you define, you need to invoke a proof that the type of Maxx.mk a b is equal to the desired output type. Unfortunately, that proof is not explicitly part of the data of Maxx c making it hard to work with.

One simple approach is to store that data directly. You have two (almost equivalent options). Use a subtype:

def Maxx (c : Ordinal.{u}) : Type (u+1) := {p : Ordinal × Ordinal // max p.1 p.2 = c}


or use a structure:

structure Maxx (c : Ordinal.{u}) : Type (u+1) where
a : Ordinal
b : Ordinal
h : max a b = c


Subtypes are structures themselves and have some nice built-in features, but lets go with a structure to be explicit.

Then everything is a bit easier to work with:

import Mathlib.SetTheory.Ordinal.Basic
import Mathlib.SetTheory.Ordinal.Arithmetic
import Init.Prelude
import Mathlib.Init.Logic
import Mathlib.Order.SuccPred.Basic

def Maxxx (c : Ordinal.{u}) : Type (u+1) := {p : Ordinal × Ordinal // max p.1 p.2 = c}
structure Maxx (c : Ordinal.{u}) : Type (u+1) where
a : Ordinal
b : Ordinal
h : max a b = c

theorem max_succ_max : {α β : Ordinal} → max (Order.succ (max α β)) β = Order.succ (max α β) := by
intro a b
rw [succ_max, max_assoc, max_eq_left_of_lt (Order.lt_succ b)]

def succ {c: Ordinal} (m: Maxx c) : Maxx (Order.succ c) :=
{
a := (max m.a m.b)+1
b := m.b
h := calc
max (max m.a m.b + 1) m.b = Order.succ (max m.a m.b) := max_succ_max
_ = Order.succ c := by rw [m.h]
}

def zerom : Maxx 0 := ⟨0, 0, Ordinal.max_zero_right 0⟩
def onem : Maxx 1 := ⟨1, 0, Ordinal.max_zero_right 1⟩

def is_eq {a b: Ordinal} (m1: Maxx a) (m2: Maxx b) : Prop :=
m1.a = m2.a ∧ m1.b = m2.b

theorem m_succ_zero_eq_one : is_eq (succ zerom) onem := by
simp [is_eq, zerom, onem, succ]


Your is_eq is very similar to the built in HEq:

theorem m_succ_zero_heq_one : HEq (succ zerom) onem := by
simp only [zerom, onem, succ]
congr!
. simp
. simp


Also, if you can manage to get the parameters of Maxx c to line up, then everything becomes easy equality:

theorem is_eq_is_eq (c : Ordinal) (m1 m2 : Maxx c) (h : is_eq m1 m2) : m1 = m2 := by
induction m1
induction m2
simp only [is_eq] at h
simp [h]


[Edit:] In case it helps, here is a proof using your original definitions. The key was to make some accessors for a and b and to make lemmas for the h ▸ (Maxx.mk a b) representation.

def Maxx.a {c: Ordinal} : (m: Maxx c) -> Ordinal
| Maxx.mk a _ => a

def Maxx.b {c: Ordinal} : (m: Maxx c) -> Ordinal
| Maxx.mk _ b => b

--theorem Maxx.h {c: Ordinal} (m: Maxx c) : (max m.a m.b = c) := by
--  induction m
--  simp [Maxx.a, Maxx.b]

theorem Maxx.alt_a {c: Ordinal} {a b : Ordinal} {h : max a b = c}: (h ▸ (Maxx.mk a b)).a = a := by
have hh : (h ▸ (Maxx.mk a b)).a = (Maxx.mk a b).a := by
congr
. simp [h]
. simp
rw [hh, Maxx.a]

theorem Maxx.alt_b {c: Ordinal} {a b : Ordinal} {h : max a b = c}: (h ▸ (Maxx.mk a b)).b = b := by
have hh : (h ▸ (Maxx.mk a b)).b = (Maxx.mk a b).b := by
congr
. simp [h]
. simp
rw [hh, Maxx.b]

def succ_h {c: Ordinal} (m: Maxx c) : max (max m.a m.b + 1) m.b = Order.succ c := by
induction m
simp [max_succ_max, Maxx.a, Maxx.b]

theorem succ_alt {c: Ordinal} (m: Maxx c) : succ m = (succ_h m) ▸ Maxx.mk ((max m.a m.b) + 1) m.b := by
induction m
simp [succ]
congr

def is_eq_alt {a b: Ordinal} (m1: Maxx a) (m2: Maxx b) : (is_eq m1 m2) = (m1.a = m2.a ∧ m1.b = m2.b) := by
induction m1
induction m2
simp [is_eq, Maxx.a, Maxx.b]

theorem m_succ_zero_eq_one : is_eq (succ zerom) onem := by
simp [is_eq_alt, succ_alt, Maxx.alt_a, Maxx.alt_b, onem, zerom]

• Thank you. I can't quite use HEq since the terms can be actually types in my real project, but including a proof of max a b=c worked to solve this one. Commented Jul 15 at 16:26
• I also just edited with a proof using your original definitions if it helps, but it looks like you have it figured out. Commented Jul 15 at 17:16