Cannot simplify/rewrite scrutinee with hypothesis/proof

Stream: general

[pandaman]

I came across a situation where simp and rw fail to simplify a match scrutinee when proving simplification lemmas for each match branch in a function. There seem to be two issues:

1. simp failed to simplify the match scrutinee when it introduces an equality hypothesis via match h : ....
2. rw failed because it tried to rewrite the proof in the function as well, which caused the motive not type check.

Here is my attempt to minimize the issue. I needed to retain enough dependent types (i.e., use of Fin and WF) to keep the issue happening. Can someone shed light on what's happening? Thanks!

MWE:

set_option autoImplicit false

inductive Node where
  | done
  | epsilon (next : Nat)

def Node.InBounds (n : Node) (size : Nat) : Prop :=
  match n with
  | .done => True
  | .epsilon next => next < size

def WF (nodes : Array Node) : Prop := ∀ i : Fin nodes.size, nodes[i].InBounds nodes.size

def WF.InBounds {nodes : Array Node} {node : Node} (wf : WF nodes) (i : Fin nodes.size) (hn : nodes[i] = node) : node.InBounds nodes.size :=
  hn ▸ wf i

def getNext (nodes : Array Node) (wf : WF nodes) (state : Fin nodes.size) : Option (Fin nodes.size) :=
  match h : nodes[state] with
  | .done => .none
  | .epsilon next =>
    -- This proof makes `rw` fail with `motive is not type correct`. It seems that `rw` tries to rewrite the proof as well?
    have isLt : next < nodes.size := wf.InBounds state h
    some ⟨next, isLt⟩

-- A simplification lemma for each case.
theorem getNext_done {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} (h : nodes[state] = .done) :
  getNext nodes wf state = .none := by
  simp [getNext]
  simp at h

  /-
  Here, we have the following context:

  ```
  nodes : Array Node
  wf : WF nodes
  state : Fin nodes.size
  h : nodes[↑state] = Node.done
  ⊢ (match h : nodes[↑state] with
    | Node.done => none
    | Node.epsilon next => some ⟨next, ⋯⟩) =
    none
  ```

  I want to simplify `nodes[↑state]` using the hypothesis `h`. Even though it perfectly matches the scrutinee in the `match`, `simp` fails for some reason.

  OBSERVATIONS:
  1. if `getNext` uses `match nodes[state] with ...` (no `h`), it works fine.
  2. `rw` doesn't work either, but the reason seems to be different. It tries to rewrite the proof inside `getNext` as well, which causes the motive to fail to typecheck.
  3. `split <;> simp_all` tends to work, but it fails in more complex cases.
  -/

  -- Even though `h` matches the `nodes[↑state]` scrutinee in `match`, `simp` fails.
  -- simp [h]

  -- motive is not type correct
  -- rw [h]
  sorry

-- Other cases fail too.
theorem getNext_epsilon {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} {next : Nat} (h : nodes[state] = .epsilon next) :
  getNext nodes wf state = some ⟨next, sorry⟩ := by
  simp [getNext]
  simp at h

  -- Even though `h` matches the `nodes[↑state]` scrutinee in `match`, `simp` fails.
  -- simp [h]

  -- motive is not type correct
  -- rw [h]
  sorry

[Yann Herklotz]

So in this case I would recommend writing getNext without the dependent h, as you state in the observations.

In the current scenario, rewriting the head of the match statemen with rw[h] will not work, because the type of the proof within one of the match arms is dependent on the structure of the head of the match statement. The solution is therefore to break this dependency. This can be done in multiple ways, but for me the simplest was just to avoid the dependency in the first place. An alternative solution might be to rewrite the proof and it's type, adding a cast, however, I couldn't quite come up with the right formulation to do this.

The following seems to work quite well for me instead. Here, the definition of getNext' does not have to depend on the equality of the match expression.

set_option autoImplicit false

inductive Node where
  | done
  | epsilon (next : Nat)

def Node.InBounds (n : Node) (size : Nat) : Prop :=
  match n with
  | .done => True
  | .epsilon next => next < size

def WF (nodes : Array Node) : Prop := ∀ i : Fin nodes.size, nodes[i].InBounds nodes.size

def WF.InBounds {nodes : Array Node} {node : Node} (wf : WF nodes) (i : Fin nodes.size) (hn : nodes[i] = node) : node.InBounds nodes.size :=
  hn ▸ wf i

def getNext' {sz} (node : Node) (hinbounds : node.InBounds sz) : Option (Fin sz) :=
  match node with
  | .done => .none
  | .epsilon next =>
    have isLt : next < sz := hinbounds
    some ⟨next, isLt⟩

def getNext (nodes : Array Node) (wf : WF nodes) (state : Fin nodes.size) : Option (Fin nodes.size) :=
  getNext' nodes[state] (wf state)

theorem getNext'_done {sz} {a} {hinbounds} :
  a = Node.done →
  getNext' (sz := sz) a hinbounds = .none := by intros; subst a; rfl

theorem getNext_done {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} (h : nodes[state] = .done) :
  getNext nodes wf state = .none := by unfold getNext; rwa [getNext'_done]

theorem getNext'_epsilon {sz next} {a} {hinbounds} (h : a = Node.epsilon next) :
  getNext' (sz := sz) a hinbounds = .some ⟨next, by subst a; assumption⟩ := by intros; subst a; rfl

theorem getNext_epsilon {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} {next : Nat} (h : nodes[state] = .epsilon next) :
  getNext nodes wf state = some ⟨next, wf.InBounds state h⟩ := by
  unfold getNext; rwa [getNext'_epsilon]

[pandaman]

Thank you for the suggestion!
Hmm, this requires two functions for each pattern match, and I have a number of pattern matches of this shape. It might introduce too much boilerplate...

[Aaron Liu]

You can do a "manual rewrite" like this

-- I hope you don't mind me importing this
import Mathlib.Tactic.GeneralizeProofs

set_option autoImplicit false

inductive Node where
  | done
  | epsilon (next : Nat)

def Node.InBounds (n : Node) (size : Nat) : Prop :=
  match n with
  | .done => True
  | .epsilon next => next < size

def WF (nodes : Array Node) : Prop := ∀ i : Fin nodes.size, nodes[i].InBounds nodes.size

def WF.InBounds {nodes : Array Node} {node : Node} (wf : WF nodes) (i : Fin nodes.size) (hn : nodes[i] = node) : node.InBounds nodes.size :=
  hn ▸ wf i

def getNext (nodes : Array Node) (wf : WF nodes) (state : Fin nodes.size) : Option (Fin nodes.size) :=
  match h : nodes[state] with
  | .done => .none
  | .epsilon next =>
    have isLt : next < nodes.size := wf.InBounds state h
    some ⟨next, isLt⟩

theorem getNext_done {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} (h : nodes[state] = .done) :
  getNext nodes wf state = .none := by
  simp only [getNext, Fin.getElem_fin]
  simp only [Fin.getElem_fin] at h
  generalize_proofs h₁ h₂
  refine Eq.rec (motive := fun a h' =>
    getNext.match_1 (fun _ => Option (Fin nodes.size)) a
    (fun _ => none) (fun next h'' => some ⟨next, h₂ next (h.trans (h'.trans h''))⟩) = none) ?_ h.symm
  simp

theorem getNext_epsilon {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} {next : Nat} (h : nodes[state] = .epsilon next) :
  getNext nodes wf state = some ⟨next, sorry⟩ := by
  simp only [getNext, Fin.getElem_fin]
  simp only [Fin.getElem_fin] at h
  generalize_proofs h₁ h₂ h₃
  refine Eq.rec (motive := fun a h' =>
    getNext.match_1 (fun _ => Option (Fin nodes.size)) a
    (fun _ => none) (fun next h'' => some ⟨next, h₂ next (h.trans (h'.trans h''))⟩) =
    some ⟨next, h₃⟩) ?_ h.symm
  simp

[Yann Herklotz]

In this case, the rw! tactic from #metaprogramming / tactics > dependent rewrite tactic by @Aaron Liu also works:

theorem getNext_done {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} (h : nodes[state] = .done) :
  getNext nodes wf state = .none := by
  unfold getNext; rw! [h]

theorem getNext_epsilon {nodes : Array Node} {wf : WF nodes} {state : Fin nodes.size} {next : Nat} (h : nodes[state] = .epsilon next) :
  getNext nodes wf state = some ⟨next, wf.InBounds state h⟩ := by
  unfold getNext; rw! [h]

It will add the right casts around the dependent proof to do the rewrite.

[pandaman]

The rw! tactic worked magically well in my real examples! I really hope it will be upstreamed!

[Aaron Liu]

I think I will try to improve it soon

[Aaron Liu]

In particular, to incorporate Kyle's suggestion

Kyle Miller said:

Unconstrained rewrites are not great to work with, which is a reason that rw and simp don't insert casts just to make a rewrite go through (that's to say, it can lead you deeper into "DTT hell"). However, sometimes there is a "good" cast function available. There might be a way where we can synthesize a good cast with these. For example, docs#Fin.cast could be used when the discrepancy appears inside the Nat argument to Fin inside the type of the term that needs rewriting.