match with toLex

Stream: new members

[Eric Paul]

I would like the following to work but it does not. Any recommendations?

import Mathlib

variable (α : Type*) (β : Type*)

theorem lex_match_fail :
  ∀a : α,
    match ((Sum.inlₗ a) : α ⊕ₗ β) with
   | Sum.inlₗ a => True
   | Sum.inrₗ b => True := by
  simp

[Bjørn Kjos-Hanssen]

You can do this:

import Mathlib

variable (α : Type*) (β : Type*)

theorem lex_match_fail :
  ∀a : α,
    match ((Sum.inlₗ a) : α ⊕ₗ β) with
   | Sum.inlₗ a => True
   | Sum.inrₗ b => True := by exact fun a => trivial

[Eric Paul]

I see, thank you. That is useful but I'm confused as to why it works and I'd really like to be able to simplify the match expression as that would make more complicated situations easier.

To be more specific, this is what I'm trying to prove. What you suggested helped me prove the left_inv and right_inv but now I'm struggling with map_rel_iff'. It really seems like I should be able to simplify the match.

import Mathlib

variable (α : Type*) (β : Type*) (γ : Type*)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

def distribute : ((α ⊕ₗ β) ×ₗ γ ≃o (α ×ₗ γ) ⊕ₗ (β ×ₗ γ)) where
  toFun x :=
    match x.fst with
    | Sum.inlₗ a => Sum.inlₗ (toLex (a, x.snd))
    | Sum.inrₗ b => Sum.inrₗ (toLex (b, x.snd))
  invFun x :=
    match x with
    | Sum.inlₗ a => toLex (Sum.inlₗ a.fst, a.snd)
    | Sum.inrₗ b => toLex (Sum.inrₗ b.fst, b.snd)
  left_inv := by
    simp [Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  right_inv := by
    simp [Function.RightInverse, Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  map_rel_iff' := by
    simp
    constructor <;> intros a b
    <;> constructor <;> intros c d <;> trivial

[Eric Paul]

I was able to prove it as follows, but I had to use change in order to simplify the match. My hope is to be able to reason with toLex without needing to use change.

import Mathlib

variable (α : Type*) (β : Type*) (γ : Type*)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

def distribute : ((α ⊕ₗ β) ×ₗ γ ≃o (α ×ₗ γ) ⊕ₗ (β ×ₗ γ)) where
  toFun x :=
    match x.fst with
    | Sum.inlₗ a => Sum.inlₗ (toLex (a, x.snd))
    | Sum.inrₗ b => Sum.inrₗ (toLex (b, x.snd))
  invFun x :=
    match x with
    | Sum.inlₗ a => toLex (Sum.inlₗ a.fst, a.snd)
    | Sum.inrₗ b => toLex (Sum.inrₗ b.fst, b.snd)
  left_inv := by
    simp [Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  right_inv := by
    simp [Function.RightInverse, Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  map_rel_iff' := by
    simp; constructor <;> intros a b
    <;> constructor <;> intros c d
    · change (Sum.inlₗ (toLex (a, b))) ≤ (Sum.inlₗ (toLex (c, d))) ↔ _; simp [Prod.Lex.le_iff]
    · change (Sum.inlₗ (toLex (a, b))) ≤ (Sum.inrₗ (toLex (c, d))) ↔ _; simp [Prod.Lex.le_iff]
    · change (Sum.inrₗ (toLex (a, b))) ≤ (Sum.inlₗ (toLex (c, d))) ↔ _; simp [Prod.Lex.le_iff]
    · change (Sum.inrₗ (toLex (a, b))) ≤ (Sum.inrₗ (toLex (c, d))) ↔ _; simp [Prod.Lex.le_iff]

[Eric Paul]

Or at least I'd like to hide the change away and have simp work. Something like the following, but the following doesn't work

import Mathlib

variable (α : Type*) (β : Type*) (γ : Type*)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

@[simp]
theorem lex_match_left
    {motive : α ⊕ₗ β → Sort w}
    (a : α)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = left a := by
  change left a = left a
  trivial

[Eric Paul]

Adding these simps let me hide all the change and make map_rel_iff' just a simp but now I'm not sure why right_inv and left_inv are not just simp as well.

import Mathlib

variable (α : Type*) (β : Type*) (γ : Type*)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

@[simp]
theorem lex_fst (a : α) (b : β) : (toLex (a, b)).1 = a := rfl

@[simp]
theorem lex_snd (a : α) (b : β) : (toLex (a, b)).2 = b := rfl

@[simp]
theorem lex_match_left
    {motive : α ⊕ₗ β → Sort w}
    (a : α)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = left a := by
  change left a = left a
  trivial

@[simp]
theorem lex_match_right
    {motive : α ⊕ₗ β → Sort w}
    (b : β)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inrₗ b : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = right b := by
  change right b = right b
  trivial

def distribute : ((α ⊕ₗ β) ×ₗ γ ≃o (α ×ₗ γ) ⊕ₗ (β ×ₗ γ)) where
  toFun x :=
    match x.fst with
    | Sum.inlₗ a => Sum.inlₗ (toLex (a, x.snd))
    | Sum.inrₗ b => Sum.inrₗ (toLex (b, x.snd))
  invFun x :=
    match x with
    | Sum.inlₗ a => toLex (Sum.inlₗ a.fst, a.snd)
    | Sum.inrₗ b => toLex (Sum.inrₗ b.fst, b.snd)
  left_inv := by
    simp [Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  right_inv := by
    simp [Function.RightInverse, Function.LeftInverse]
    constructor <;> intros a b <;> trivial
  map_rel_iff' := by
    simp [Prod.Lex.le_iff]

[Eric Paul]

Here's a smaller mwe that shows the issue I'm struggling with.
Notice how test0 works but test1 does not. I'm not sure why there is a difference.

import Mathlib

variable (α : Type*) (β : Type*) (γ : Type*)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

@[simp]
theorem lex_match_left
    {motive : α ⊕ₗ β → Sort w}
    (a : α)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = left a := by
  change left a = left a
  trivial

theorem test0 (a : α) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ b => 2
  | Sum.inrₗ c => 3) = 2 := by
  simp

theorem test1 (a : α) (g : γ) :
  (match (Sum.inlₗ (toLex (a, g)) : (α ×ₗ γ) ⊕ₗ β) with
  | Sum.inlₗ b => 2
  | Sum.inrₗ c => 3) = 2 := by
  simp

[Eric Paul]

Interestingly, if I use the theorem manually with rewrite to replace all 2s with the whole match expression, then simp is able to automatically turn those matchs back into 2s.

So I inspected the types in the introduced matchs from the rw and the only difference I can find is in the types of numbers. In the 2 and 3 I wrote myself, they have type @OfNat.ofNat ℕ 2 (instOfNatNat 2) : ℕ but the ones that appear form using the rw have the type @OfNat.ofNat ((fun x => ℕ) (Sum.inlₗ c)) 2 (instOfNatNat 2) : (fun x => ℕ) (Sum.inlₗ c) and then after simplifying, the new 2s have type 2 : (fun x => ℕ) (Sum.inlₗ (toLex (a, g))).

I thought that maybe this could be the cause of the issue but I still have 2s and 3s in the example where simp does work. So I can't figure out the difference between the matchs that simp is simplifying and the ones it isn't.

import Mathlib

universe u x w

variable (α : Type u) (β : Type x) (γ : Type w)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

@[simp]
theorem lex_match_left
    (motive : α ⊕ₗ β → Sort w)
    (a : α)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = left a := by
  change left a = left a
  trivial

theorem test1 (a : α) (g : γ) :
  (match (Sum.inlₗ (toLex (a, g)) : (α ×ₗ γ) ⊕ₗ β) with
  | Sum.inl b => 2
  | Sum.inr c => 3) = 2 := by
  rw [←lex_match_left (motive := fun _ => Nat) (α := (α ×ₗ γ)) (β := β) (toLex (a,g) : (α ×ₗ γ)) (fun _ => 2) (fun _ => 3)]
  simp

[Eric Paul]

I guess I have reduced the question to the following MWE:

Why does this rw not work?

import Mathlib

universe u x w z
variable (α : Type u) (β : Type x) (γ : Type w)
  [LinearOrder α] [LinearOrder β] [LinearOrder γ]

theorem lex_match_left
    {α : Type u} {β : Type x}
    {motive : α ⊕ₗ β → Sort z}
    (a : α)
    (left : (val : α) → motive (Sum.inlₗ val))
    (right : (val : β) → motive (Sum.inrₗ val)) :
  (match (Sum.inlₗ a : α ⊕ₗ β) with
  | Sum.inlₗ c => left c
  | Sum.inrₗ d => right d) = left a := by
  change left a = left a
  trivial

theorem test1 (a : α) (g : γ) :
  (match (Sum.inlₗ (toLex (a, g)) : (α ×ₗ γ) ⊕ₗ β) with
  | Sum.inl c => 2
  | Sum.inr d => 3) = 2 := by
  rw [lex_match_left (motive := fun _ => ℕ) (toLex (a,g)) (fun _ => (2 : ℕ)) (fun _ => (3 : ℕ))]

[Kevin Buzzard]

I don't know the answer to your question, but note that rfl closes the goal.

[Eric Wieser]

I think this is a general problem with match and type synonyms, where match unfolds the synonym matchers (such as Sum.inlₗ) in the generated term

[Eric Wieser]

There are at least two problems here:

• The generated lex_match_left.match_1 is about the wrong type
• The first lemma is about lex_match_left.match_1, the second one is about test1.match_1

[Eric Paul]

Eric Wieser said:

There are at least two problems here:

• The generated lex_match_left.match_1 is about the wrong type
• The first lemma is about lex_match_left.match_1, the second one is about test1.match_1

I don't think I understand. I looked at the type of lex_match_left.match_1 and looks like what I expected to be:

lex_match_left.match_1.{u_1, u_2, u_3} {α : Type u_2} {β : Type u_1} (motive : Lex (α ⊕ β) → Sort u_3) :
  (x : Lex (α ⊕ β)) → ((c : α) → motive (Sum.inl c)) → ((d : β) → motive (Sum.inr d)) → motive x

What are the lemmas you're talking about?

I appreciate you having taken a look at this. I hadn't heard of the match_1s before. Is there some documentation about it?

[Eric Wieser]

Eric Paul said:

Eric Wieser said:

There are at least two problems here:

• The generated lex_match_left.match_1 is about the wrong type
• The first lemma is about lex_match_left.match_1, the second one is about test1.match_1

I don't think I understand. I looked at the type of lex_match_left.match_1 and looks like what I expected to be:

lex_match_left.match_1.{u_1, u_2, u_3} {α : Type u_2} {β : Type u_1} (motive : Lex (α ⊕ β) → Sort u_3) :
  (x : Lex (α ⊕ β)) → ((c : α) → motive (Sum.inl c)) → ((d : β) → motive (Sum.inr d)) → motive x

That's not type correct though, that inl should be the lex version

[Eric Paul]

Eric Wieser said:

That's not type correct though, that inl should be the lex version

Ah I see, I missed that. That makes sense.

Do you have a recommendation for how to fix this?

Could I somehow write what the match_1s should be?
Is a fix to how match works something reasonable that I could pursure?

[Eric Wieser]

I think the first step would be to file a mathlib-free bug report against Lean itself