代码之家 › 专栏 › 技术社区 › Carl Patenaude Poulin

模式匹配从目标模式匹配中获得的假设

ltac coq

0

Carl Patenaude Poulin · 技术社区 · 6 年前

考虑以下发展:

Definition done {T : Type} (x : T) := True.

Goal Test.
  pose 1 as n.
  assert (done n) by constructor.
  Fail ltac:(
    match goal with 
    | [ H : done _ |- _ ] => fail
    | [ H : _ |- _ ] =>
      match goal with
      | [ _: done H |- _ ] => idtac "H == n"
      | [ _: done n |- _ ] => idtac "H != n"; fail 2
      end
    end
  ).
Abort.

这张照片 H != n . 我发现这非常令人惊讶,因为范围内唯一的假设是 n 和 done n -和 做了N 已由顶级匹配的第一个分支调度。

我如何匹配 做了N 没有明确提及 n 在第二场比赛的第一个分队?

1 回复 | 直到 6 年前

1

eponier 6 年前

我想你是迷路了 match 作品。匹配的第一个分支与每个假设匹配,如果总是失败,则测试第二个分支,依此类推。在您的示例中,第一个分支符合假设 H 但执行相应的策略( fail )失败,因此第二个分支也被尝试匹配假设。 H .

实际上,外部的第一个分支 比赛 似乎做了你想做的(即符合形式假设) done _ )所以我不太明白你内心的意思 比赛 .

例如,

match goal with 
| [ H' : done _ |- _ ] => idtac H'
end.

印刷品 H 说明正确的假设是匹配的。

注意你不需要 ltac:() 要使用的表达式 Fail 战术上的例如, Fail fail. 作品。