match with equation

Stream: general

[Yury G. Kudryashov]

I have the following definition:

import data.fin.basic

inductive generator
| a : generator
| bcd : fin 3 → generator

def cancel : list generator → list generator
| [] := []
| [a] := [a]
| (a :: a :: l) := cancel l
| (a :: bcd n :: l) := a :: cancel (bcd n :: l)
| (bcd n :: l) :=
  match cancel l with
  | [] := [bcd n]
  | (a :: l) := bcd n :: a :: l
  | (bcd m :: l) := bcd (-n - m) :: l
  end

Then I want to prove that length (cancel l) ≤ length l (and a few other properties). How do I deal with match? If I write

lemma length_cancel_le : ∀ l : free_monoid generator, length (cancel l) ≤ length l
| [] := le_rfl
| [a] := le_rfl
| (a :: a :: l) := nat.le_succ_of_le $ nat.le_succ_of_le $ length_cancel_le l
| (a :: bcd n :: l) := nat.succ_le_succ $ length_cancel_le _
| (bcd n :: l) :=
  match cancel l with
  | [] := _
  | (a :: l') := _
  | (bcd m :: l') := _
  end

then Lean doesn't know that bcd m :: l' = cancel l.

[Yury G. Kudryashov]

Should I move this match to an explicit auxiliary definition?

[Yakov Pechersky]

Will it work if you have helper definitional lemmas about what "cancel (bcd n :: [])" is equal to,

[Floris van Doorn]

I assume you want to use the term-mode match notation? In tactics you can do induction h : cancel l, to record a hypothesis h that cancel l = [] and cancel l = _ :: _.

[Floris van Doorn]

Here is a workaround using the match notation that should work:

  let c := cancel l in
  let h : c = cancel l := rfl in
  match cancel l, h with
  | [], h := _
  | (a :: l'), h := _
  | (bcd m :: l'), h := _
  end

[Yury G. Kudryashov]

I decided to move this case to an explicit auxiliary definition.

[Eric Wieser]

https://proofassistants.stackexchange.com/a/529/347 is perhaps relevant