coq - Coq 证明自动化没有像我预期的那样工作

Question

我目前正在从事软件基金会的 RedBlack 工作……我正在研究“ins_is_redblack”（您可以在此处找到它https://softwarefoundations.cis.upenn.edu/vfa-current/Redblack.html）。

我正在努力弄清楚为什么我的比赛目标不起作用。目标有很多调用，我应该自动化解决方案。这里有两个有代表性的例子：

nearly_redblack
  match c with
  | Red =>
      match t1 with
      | E =>
          match t2 with
          | T Red b y vy c0 =>
              T Red (T Black t1 k0 v0 b) y vy (T Black c0 k v E)
          | _ => T Black (T c t1 k0 v0 t2) k v E
          end
      | T Red a x0 vx0 b =>
          T Red (T Black a x0 vx0 b) k0 v0 (T Black t2 k v E)
      | T Black _ _ _ _ =>
          match t2 with
          | T Red b0 y vy c0 =>
              T Red (T Black t1 k0 v0 b0) y vy (T Black c0 k v E)
          | _ => T Black (T c t1 k0 v0 t2) k v E
          end
      end
  | Black => T Black (T c t1 k0 v0 t2) k v E
  end 1

和

nearly_redblack
  (if ltb k x then balance Black s1 k v (ins x vx s2) else T Black s1 x vx s2)
  (S n0)

我正在尝试逐步建立我的自动化，但很快就卡住了

repeat match goal with
 (* doesn't work *)
 | |- nearly_redblack (match ?c with Red => _ | Black => _ end) _ => destruct c
 (* works *)
 | |- nearly_redblack (T _ _ _ _ _) 1  => constructor
 (* works *)
 | |- is_redblack E Black 0 => constructor
 (* doesn't work *)
 | |- match ?c with Red => _ | Black => _ end => destruct c
 (* doesn't work *)
 | |- nearly_redblack (if ltb ?k ?x then _ else _) _ => bdestruct (ltb k x); try omega
end.

我有点不知道为什么这不起作用......它似乎与文件中自动化的其他用途相匹配，但我对匹配目标的工作方式并没有一个很好的心理模型。希望这里有人可以帮助我弄清楚发生了什么。Coq 的证明自动化看起来很强大，但是语法是啊......

标签： coqcoq-tactic