我如何在 Coq 的证明中自动计数？

Question

我有一个函数 count，它计算给定谓词在应用于列表元素时可证明的次数。定义如下：

Parameter T : Type.

Parameter dec: forall (p: T -> Prop) (w: T), {p w} + {~ (p w)}.

Fixpoint count (p: T -> Prop) (l: list T) := match l with
  | nil => 0
  | (cons head tail) => if (dec p head) then (1 + (count p tail)) else (count p tail)
end.

然后我使用这个函数来陈述引理，如下所示：

Parameter a b c: T.
Parameter q: T -> Prop.

Axiom Aa: (q a).
Axiom Ab: (q b).
Axiom Ac: ~ (q c).

Lemma example: (count q (cons a (cons b (cons c nil)))) = 2.

我对此类引理的证明往往很乏味：

Lemma example: (count q (cons a (cons b (cons c nil)))) = 2.
Proof.
unfold count.
assert (q a); [apply Aa| auto].
assert (q b); [apply Ab| auto].
assert (~ (q c)); [apply Ac| auto].
destruct (dec q a); [auto | contradiction].
destruct (dec q b); [auto | contradiction].
destruct (dec q c); [contradiction | auto].
Qed.

我可以做些什么来使用我的 count 函数自动执行这些涉及计算的繁琐证明？

Answer 1

让我们创建自定义提示数据库并在其中添加您的公理：

Hint Resolve Aa : axiom_db.
Hint Resolve Ab : axiom_db.
Hint Resolve Ac : axiom_db.

现在，firstorder策略可以利用提示数据库：

Lemma example: count q (cons a (cons b (cons c nil))) = 2.
Proof.
  unfold count.
  destruct (dec q a), (dec q b), (dec q c); firstorder with axiom_db.
Qed.

我们可以使用以下 Ltac 自动化我们的解决方案：

Ltac solve_the_probem :=
  match goal with
  |- context [if dec ?q ?x then _ else _] =>
      destruct (dec q x);
      firstorder with axioms_db;
      solve_the_probem
  end.

那么，unfold count; solve_the_probem.就可以证明引理了。

Answer 2

在这种情况下，您最好通过反思来证明事情。看看事情进展如何顺利（当然我修改了你的例子以避免所有这些公理）：

Require Import List.
Import ListNotations.

Fixpoint count {T : Type} (p : T -> bool) (l : list T) :=
  match l with
  | [] => 0
  | h :: t => if p h then S (count p t) else (count p t)
  end.

Inductive T := a | b | c.

Definition q x :=
  match x with
  | a => true
  | b => true
  | c => false
  end.

Lemma example: (count q [a; b; c]) = 2.
Proof.
  reflexivity.
Qed.

我意识到你对 count 的定义是在类型 T 上采用命题谓词（但假设类型 T 上的所有谓词都是可判定的）并且我建议将 count 定义为取一个布尔谓词。但是你可能会意识到，拥有一个可判定的命题谓词或拥有一个布尔谓词实际上是等价的。

例如根据您的公理，我可以定义一个函数，将任何命题谓词转换为布尔谓词：

Parameter T : Type.

Parameter dec: forall (p: T -> Prop) (w: T), {p w} + {~ (p w)}.

Definition prop_to_bool_predicate (p : T -> Prop) (x : T) : bool :=
  if dec p x then true else false.

当然，由于您的示例中涉及公理，因此实际上无法使用布尔谓词进行计算。但我假设您为了示例的目的而放置了所有这些公理，而您的实际应用程序没有它们。

回复您的评论

正如我告诉过你的，一旦你根据公理（或 Parameter 定义了一些函数，因为这是同一件事），你就无法再用它来计算了.

然而，这里有一个解决方案，其中命题谓词 p 的可判定性是一个引理。我用 Defined instead of Qed 结束了引理的证明，以允许用它进行计算（否则，它不会比公理更好）。如您所见，我还重新定义了 count 函数以获取谓词及其可判定性证明。在这种情况下，反射证明仍然有效。没有bool但严格等价

Require Import List.
Import ListNotations.

Fixpoint count {T : Type}
  (p : T -> Prop) (dec : forall (w: T), {p w} + {~ (p w)}) (l : list T) :=
  match l with
  | [] => 0
  | h :: t => if dec h then S (count p dec t) else (count p dec t)
  end.

Inductive T := a | b | c.

Definition p x := match x with | a => True | b => True | c => False end.

Lemma dec_p: forall (w: T), {p w} + {~ (p w)}.
Proof.
  intros []; simpl; auto.
Defined.

Lemma example2: (count p dec_p [a; b; c]) = 2. Proof. reflexivity. Qed.

我如何在 Coq 的证明中自动计数？

How can I automate counting within proofs in Coq?

coq

coq-tactic

回复您的评论