Case analysis of pattern-matching definition

Stream: new members

[Jason Orendorff]

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]

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

[Mario Carneiro]

It's not three cases, the presentation is misleading

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

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]

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