# Zulip Chat Archive

## Stream: new members

### Topic: Case analysis of pattern-matching definition

#### Jason Orendorff (Jun 04 2020 at 06:02):

TPIL exercise 8.6 has me proving a theorem about this function:

```
def simp_const : aexpr → aexpr
| (plus (const n₁) (const n₂)) := const (n₁ + n₂)
| (times (const n₁) (const n₂)) := const (n₁ * n₂)
| e := e
```

The obvious way to structure the proof is based on the structure of the definition, a case analysis with 3 cases. How can I do that?

A match expression doesn't seem to work. `intro e, cases e`

instead splits along the structure of the inductive type `aexpr`

.

#### Jason Orendorff (Jun 04 2020 at 06:19):

This fails at line 41: https://gist.github.com/jorendorff/0b1c492b81687e43ebc749ea1b353080

#### Mario Carneiro (Jun 04 2020 at 06:46):

It's not three cases, the presentation is misleading

#### Mario Carneiro (Jun 04 2020 at 06:47):

If you `#print prefix simp_const`

you will see that the equation compiler has to split the wildcard case here into many subcases

#### Mario Carneiro (Jun 04 2020 at 06:48):

You have to split along `aexpr`

(three times, in fact). However you can use tricks like `all_goals`

to provide the same proof for the wildcard cases

#### Jason Orendorff (Jun 04 2020 at 07:13):

It's not so bad, I guess:

```
theorem simp_const_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (simp_const e) = aeval v e
:= begin
intro e, cases e,
case plus : a b {
cases a,
case const : av {
cases b,
all_goals { refl }
},
all_goals { refl }
},
case times : a b {
cases a,
case const : av {
cases b,
all_goals { refl }
},
all_goals { refl }
},
all_goals { refl }
end
```

Thank you!

#### Mario Carneiro (Jun 04 2020 at 07:43):

You can even collapse all the `refl`

cases into one:

```
theorem simp_const_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (simp_const e) = aeval v e
:= begin
intro e, cases e,
swap 3, cases e_a, cases e_a_1,
swap 10, cases e_a, cases e_a_1,
all_goals { refl }
end
```

You used to be able to use `case`

for this but it looks like someone snuck a change in to make `case`

act like `focus`

, which means you can't do partial work on a goal anymore.

#### Mario Carneiro (Jun 04 2020 at 07:50):

Hm, git blame doesn't agree with me, apparently the `solve1`

in `case`

has been there since the beginning. It would be nice to have a variation that doesn't do that though for problems like this

#### Mario Carneiro (Jun 04 2020 at 07:55):

A workaround is to drop the goals and then pick them up later:

```
meta def tactic.interactive.drop := tactic.set_goals []
theorem simp_const_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
begin
intro e, cases e,
case plus : a b {
cases a, case const { cases b, drop },
drop },
case times : a b {
cases a, case const { cases b, drop },
drop },
recover; refl
end
```

#### Sam Lichtenstein (Jun 04 2020 at 12:23):

What about “cases e; try {refl},”

#### Yakov Pechersky (Jun 05 2020 at 21:01):

The followup exercise is stumbling me. Not sure how to tie the knot on the recursive equality. I have that

```
def aeval (v : ℕ → ℕ) : aexpr → ℕ
| (const n) := n
| (var n) := v n
| (plus e₁ e₂) := (aeval e₁) + (aeval e₂)
| (times e₁ e₂) := (aeval e₁) * (aeval e₂)
def simp_const : aexpr → aexpr
| (plus (const n₁) (const n₂)) := const (n₁ + n₂)
| (times (const n₁) (const n₂)) := const (n₁ * n₂)
| e := e
def fuse : aexpr → aexpr
| (plus x y) := simp_const (plus (fuse x) (fuse y))
| (times x y) := simp_const (times (fuse x) (fuse y))
| e := e
```

but proving

```
theorem fuse_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (fuse e) = aeval v e :
```

gets stuck at the plus and times cases, which descend into proving the parent statement again. The parent poster to this thread has a different definition for `fuse`

at https://gist.github.com/jorendorff/8b862caf53a583857dbacbbee22d76a3#file-expressions-lean-L35 but that does not simplify statements as expected. However, it is provably equal to the evaluated expression.

#### Yakov Pechersky (Jun 05 2020 at 21:17):

What I mean by recursive proof is indicated here:

```
theorem fuse_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (fuse e) = aeval v e :=
begin
intro e,
cases e,
case const {refl},
case var {refl},
case plus : a b {
dsimp [fuse],
cases a;
cases b;
try {refl},
rw simp_const_eq,
dsimp [fuse],
dsimp [aeval],
rw simp_const_eq,
dsimp [aeval],
-- a + (aeval v (fuse b_a) + aeval v (fuse b_a_1)) = a + (aeval v b_a + aeval v b_a_1)
-- which is what we basically had at the parent cases split
},
case times {sorry},
end
```

#### Shing Tak Lam (Jun 06 2020 at 01:51):

So you probably need `induction`

and not `cases`

for this. See the `IHf`

and `IHg`

which are in the `plus`

and `times`

cases which you don't get with `cases`

.

```
theorem fuse_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (fuse e) = aeval v e :=
begin
intro e,
induction e,
case const { refl },
case var { refl },
case plus : f g IHf IHg { sorry },
case times : f g IHf IHg { sorry },
end
```

Last updated: May 13 2021 at 06:15 UTC