Search code examples
coq

Coq: unfold tricky notations

Suppose I want to convert ~X to X -> False using unfold tactic.

I have two options how to do it: either by unfold not or by unfold "~". The second way is apparently more convenient since there is no need to remember what definition name stays behind the notation.

However I haven't managed to do it in more complex cases:

Definition assn_sub X a P : Assertion :=
  fun (st : state) =>
    P (X !-> aeval st a ; st).

Notation "P [ X |-> a ]" := (assn_sub X a P)
  (at level 10, X at next level).

and I want to unfold it in expression

((fun st0 : state => st0 Y = st0 X + st0 Z) [Z |-> Y - X]) st

without using assn_sub. Is it possible?

Solution

  • With underscores, it seems to work.

    unfold "_ [ _ |-> _ ]".