0

我是 Coq 的新手，目前在Software FoundationsIndProp章节。我很想学习编写自己的简单策略来自动化某些类型的推理，但不幸的是，作为初学者，官方文档对我来说有点难以理解。

我想写一个适用于以下场景的策略：

  • 目前的目标是False
  • 有一个形式的假设P \/ False

基于以下引理，我们应该能够~P在这种情况下将当前目标替换为：

Lemma orfalse_lemma : forall P : Prop,
  P \/ False -> ~P -> False.
Proof.
  intros P [H|H] HP.
  - apply HP. apply H.
  - apply H.
Qed.

我们可以手动使用引理来达到预期的效果：

Example ex_orfalse_1 :
  (1 <> 2) \/ False -> (False).
Proof.
  intros H. apply (orfalse_lemma (1 <> 2)). apply H.
  (* goal:  ~ (1 <> 2) *)
Admitted.

我想自动化这个，所以我写了一个简单的策略来在目标和上下文匹配这个场景时应用引理：

Ltac orfalse :=
  match goal with
    | [H : ?P \/ False |- False ] => apply (orfalse_lemma P) ; [> apply H | ]
    | _                           => fail "expected goal to be False"
  end.

它按预期工作。但是，当有多个假设与模式匹配时，我们无法在它们之间进行选择：

Example ex_orfalse_1 :
  (1 <> 2) \/ False -> (False).
Proof.
  intros H. orfalse.
  (* goal:  ~ (1 <> 2) *)
Admitted.

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse.
  (* goal:  ~ (1 <> 2) *)
  (* what if we want the goal to be ~ (false <> true) instead? *)
Admitted.

我假设解决这个问题就像将所需的假设orfalse作为参数传递给策略一样简单：

Ltac orfalse H :=
  match goal with
    | [|- False ] =>  match H with
                      | ?P \/ False => apply (orfalse_lemma ?P) ; [> apply H | ]
                      | _  => fail "expected disjunction with false"
                      end
    | _ => fail "expected goal to be False"
  end.

但是，在证明中使用它失败了：

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse H1.
  (* Tactic failure: expected goal to be False. *)
Admitted.

?P如果我用 just和 return替换嵌套匹配的第一种情况idtac ?P，它只会打印我传入的假设的名称（例如H1or H2），所以我的猜测是匹配发生在标识符本身而不是假设上。

所以，我的问题是： 如果我将假设的名称传递给策略，我如何正确匹配该假设的结构？ 谢谢！

4

1 回答 1

1

欢迎来到 Coq！

你的策略有两个小问题。首先，您不能匹配的值H- 这要么是证明项，要么H是简单H且无法进一步评估的值 - 您必须匹配 H 的类型。然后在使用匹配变量时，不是吗？是必须的。这有效：

Lemma orfalse_lemma : forall P : Prop,
  P \/ False -> ~P -> False.
Proof.
  intros P [H|H] HP.
  - apply HP. apply H.
  - apply H.
Qed.

Ltac orfalse H :=
  match goal with
    | [ |- False ] => match type of H with
                      | ?P \/ False => apply (orfalse_lemma P) ; [> apply H | ]
                      | _  => fail "expected disjunction with false"
                      end
    | _ => fail "expected goal to be False"
  end.

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse H1.
Admitted.
于 2021-07-14T13:10:04.437 回答