## Stream: new members

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

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

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