# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC