## Stream: general

### Topic: match with equation

#### Yury G. Kudryashov (Sep 30 2022 at 07:45):

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 (Sep 30 2022 at 07:49):

Should I move this match to an explicit auxiliary definition?

#### Yakov Pechersky (Sep 30 2022 at 11:13):

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

#### Floris van Doorn (Sep 30 2022 at 11:40):

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 (Sep 30 2022 at 11:46):

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 (Sep 30 2022 at 11:57):

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

#### Eric Wieser (Sep 30 2022 at 22:49):

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

Last updated: Aug 03 2023 at 10:10 UTC