Can we provide proofs to match expressions?

Stream: new members

[Jonathan Lacombe]

Hi, I have been encountering multiple scenarios where a match expression tells me I am "missing cases", even when I know all cases are covered.

Is there a way to provide evidence that all cases are covered? Or if not, would writing a custom match using recursors be possible/feasible?

Example: at the bottom there is a match case with sorry, which should be an unreachable case.

def Vector (N: Nat) := { x: List Nat // x.length = N }

def Vector.mk (ns: List Nat) (h: ns.length = N := by simp): Vector N := Subtype.mk ns h

theorem Vector.of_empty_length (a: Vector N) (k: a.val = []): ([]: List Number).length = N := by
  have p := a.property
  rw [k] at p
  exact p

local macro "access" x:ident "." y:ident : term => `( $(x).$(y) )

local macro "vector_cons " a:ident ha:ident an:ident as:ident : tactic =>
  `(tactic|
    ( have z := List.length_cons $an $as
      have p := access $a . property
      rw [←$ha] at z
      rw [z] at p
      rw [←p]
      simp))

theorem Vector.of_cons_length (a: Vector N) (ha : a.val = an :: as): N - 1 < N := by
  vector_cons a ha an as

theorem Vector.tail_minus_one (a: Vector N) (ha: a.val = an :: as): as.length = N - 1 := by
  vector_cons a ha an as

def Vector.add (a: Vector N) (b: Vector N): Vector N :=
  match ha: a.val, hb: b.val with
  | [],     []      =>
    Vector.mk [] (of_empty_length a ha)

  | an::as, bn::bs  =>
    have termination: N - 1 < N := Vector.of_cons_length a ha

    let vas: Vector (N - 1) := Vector.mk as (Vector.tail_minus_one a ha)
    let vbs: Vector (N - 1) := Vector.mk bs (Vector.tail_minus_one b hb)
    let sum: Vector (N - 1) := Vector.add vas vbs

    have proof: ((an + bn) :: sum.val).length = N := by
      simp
      have g := sum.property
      rw [sum.property]
      have t := termination
      rw [← g] at t
      replace t := Nat.not_eq_zero_of_lt t
      rw [Nat.sub_one_add_one]
      exact t

    Vector.mk ((an+bn)::sum.val) proof

  | _,      _       =>
    sorry

[Chris Bailey]

I don't think I understand the last one, what if one of the sides is empty and the other one isn't?

[Jonathan Lacombe]

Chris Bailey said:

I don't think I understand the last one, what if one of the sides is empty and the other one isn't?

Sorry I didn't explain. The Vector N is a subtype that restricts the length of the vector to size N (defined in first line), so they will always have the same size as defined by the function.

[Jonathan Lacombe]

It is impossible to call Vector.add (Vector.mk [1, 2]) (Vector.mk [1, 2, 3]) since the matching propositions wouldn't be provided

[Jonathan Lacombe]

I did find something interesting though. Just like the have statement I have for the termination proof, you can include have statements before the match to constrain the type.

I tested this by adding the following right before the match:

have restrict_cases: av.length = 0 ∧ bv.length = 0 := by
    sorry

With this I can remove the _, _ differing case but the other an::as, bn::bs case as well (which of course I don't want)

Unlike termination proofs. I do not see what goal I need to be able to prove and remove the cases where one side is empty and the other isn't. So right now, I am just guessing to see if they end up working

[Jonathan Lacombe]

It would be cool if whenever a case is missing from a match, lean could provide a goal to solve to handle that case. I think that could be big especially when programming with a lot of subtypes

[Chris Bailey]

I think there are some typos in the of_empty_length lemma?

[Chris Bailey]

You basically need to show why it's not reachable within the match arm:

def Vector (N: Nat) := { x: List Nat // x.length = N }

def Vector.mk (ns: List Nat) (h: ns.length = N := by simp): Vector N := Subtype.mk ns h

theorem Vector.of_empty_length (a: Vector N) (k: a.val = []): ([]: List Nat).length = N := by
  have p := a.property
  rw [k] at p
  exact p

local macro "access" x:ident "." y:ident : term => `( $(x).$(y) )

local macro "vector_cons " a:ident ha:ident an:ident as:ident : tactic =>
  `(tactic|
    ( have z := List.length_cons $an $as
      have p := access $a . property
      rw [←$ha] at z
      rw [z] at p
      rw [←p]
      simp))

theorem Vector.of_cons_length (a: Vector N) (ha : a.val = an :: as): N - 1 < N := by
  vector_cons a ha an as

theorem Vector.tail_minus_one (a: Vector N) (ha: a.val = an :: as): as.length = N - 1 := by
  vector_cons a ha an as

def Vector.add (a: Vector N) (b: Vector N): Vector N :=
  match ha: a.val, hb: b.val with
  | [],     []      =>
    Vector.mk [] (of_empty_length a ha)

  | an::as, bn::bs  =>
    have termination: N - 1 < N := Vector.of_cons_length a ha

    let vas: Vector (N - 1) := Vector.mk as (Vector.tail_minus_one a ha)
    let vbs: Vector (N - 1) := Vector.mk bs (Vector.tail_minus_one b hb)
    let sum: Vector (N - 1) := Vector.add vas vbs

    have proof: ((an + bn) :: sum.val).length = N := by
      simp
      have g := sum.property
      rw [sum.property]
      have t := termination
      rw [← g] at t
      replace t := Nat.not_eq_zero_of_lt t
      rw [Nat.sub_one_add_one]
      exact t

    Vector.mk ((an+bn)::sum.val) proof
  | [], b'::bs => by
    have h0 := Vector.of_empty_length a ha
    have h1 := List.length_cons b' bs
    have h2 : N = (b' :: bs).length := hb ▸ b.property.symm
    have h3 := List.length_nil ▸ h0
    have h4 := h2 ▸ h1
    have h5 : 0 = bs.length + 1 := h3 ▸ h4
    cases h5
  | a'::as, [] =>
    have h0 := Vector.of_empty_length b hb
    have h1 := List.length_cons a' as
    have h2 : N = (a' :: as).length := ha ▸ a.property.symm
    have h3 := List.length_nil ▸ h0
    have h4 := h2 ▸ h1
    have h5 : 0 = as.length + 1 := h3 ▸ h4
    cases h5

[Chris Bailey]

The goal is to produce an element of the correct type, but for unreachable arms you usually proceed by showing that there's a contradiction present somewhere.

[Jonathan Lacombe]

Chris Bailey said:

The goal is to produce an element of the correct type, but for unreachable arms you usually proceed by showing that there's a contradiction present somewhere.

Thank you so much. There's always something that I just never heard/learned about. You saved me a lot of time I would have spent just staring at this.

[Kyle Miller]

In case it's useful, here are a few patterns you can find in the wild for dispatching impossible match arms:

• ... => by exfalso; ...
• ... => absurd ... ...
• ... => False.elim (...)

The first and third are both for making use of a proof of False.