1

我有一个函数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函数进行计算的乏味证明？

4

2 回答 2

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.

当然，由于您的示例中涉及公理，因此实际上不可能使用布尔谓词进行计算。但是我假设您将所有这些公理用于示例的目的，并且您的实际应用程序没有它们。

回答您的评论

正如我告诉你的，一旦你根据公理（或 a，Parameter因为这是同一件事）定义了某个函数，就无法再用它进行计算。

然而，这是一个解决方案，其中命题谓词的可判定性p是一个引理。我结束了引理的证明，Defined而不是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.
于 2017-03-09T10:51:29.823 回答
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.就能证明引理。

于 2017-03-08T08:52:21.600 回答