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

Question

考虑以下发展：

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- 并且done n已经由顶级匹配的第一个分支发送。

如何在done n不明确引用的情况下进行匹配n，如第二个匹配的第一个分支？

Answer 1

我认为您对match工作方式感到困惑。匹配的第一个分支与每个假设匹配，如果总是失败，则测试第二个分支，依此类推。在您的示例中，第一个分支与假设匹配H，但相应策略 ( fail) 的执行失败，因此尝试了第二个分支，该分支也与假设匹配H。

实际上，外部的第一个分支match似乎做了你想要的（即匹配形式的假设done _），所以我真的不明白你的内在match。

例如，

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

打印H，表明正确的假设是匹配的。

请注意，您不需要在策略上ltac:()使用表达式Fail。例如，Fail fail.作品。