cases' confuses the equation compiler

Stream: metaprogramming / tactics

[Jannis Limperg]

I'm trying to fix an unfortunate interaction between docs#tactic.interactive.cases' and the equation compiler. cases' is a variant of the induction' tactic which is supposed to be a drop-in replacement for cases. However, using cases' in a definition involving the equation compiler may fail where cases would succeed. Afaict, the problem is that cases' generates a different proof term than cases and the termination checker can't process that term.

Example:

import tactic.induction
import tactic.simp_result

inductive btree (α : Type) : Type
| empty {} : btree
| node     : α → btree → btree → btree

def mirror {α : Type} : btree α → btree α
| btree.empty        := btree.empty
| (btree.node a l r) := btree.node a (mirror r) (mirror l)

inductive is_full {α : Type} : btree α → Prop
| empty : is_full btree.empty
| node (a : α) (l r : btree α)
    (hl : is_full l) (hr : is_full r)
    (hiff : l = btree.empty ↔ r = btree.empty) :
  is_full (btree.node a l r)

lemma is_full_mirror {α : Type} :
  ∀t : btree α, is_full t → is_full (mirror t)
| btree.empty        := id
| (btree.node a l r) :=
  begin
    rw mirror,
    intro ht,
    dsimp_result { cases' ht with _ _ _ hl hr hiff },
    tactic.trace_result,
    apply is_full.node,
    { exact is_full_mirror _ hr },
    { apply is_full_mirror _ hl },
    { sorry }
  end

The last lemma fails because the equation compiler doesn't realise that hr and hl are about trees that are structurally smaller than node a l r. If you replace cases' with cases, the proof goes through. Any ideas how I could address this?

[Jannis Limperg]

(deleted) (Zulip strikes again)