标签: coq-tactic

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  Fail checkForall H. (* not a forall *)
Abort.

我会天真地期望checkForall H成功,但事实并非如此.

在他的" 依赖类型认证编程"一书中,Adam Chlipala 讨论了依赖类型的模式匹配限制:

问题是统一变量可能不包含本地绑定变量.

这是我在这里看到的行为的原因吗？

我正在尝试为我编写的矩阵库创建一个Hint Rewrite数据库.但是当我写的时候

Hint Rewrite kron_1_r : M_db

我收到以下错误:

Cannot infer the implicit parameter m of kron_1_r whose type is "nat".

kron_1_r具有类型forall {m n : nat} (A : Matrix m n), A ? Id 1 = A,因此应根据调用autorewrite时的上下文推断出m和n.我不确定为什么它想要一个参数,或者如何告诉它推迟.

假设我们试图形式化一些(半)组理论属性,如下所示:

Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, (op e x) = x.
Definition is_right_neutral (e: A) := forall x: A, x = (op x e).

Lemma uniqueness_of_neutral:
  forall a b: A, (is_left_neutral a) -> (is_right_neutral b) -> (a = b).
Proof.
  intro; intro.
  intros lna rnb.
  elim lna with b; elim rnb with a.
  reflexivity.
Qed.

End Group.

它的工作正常,但是,如果我们在上述任一定义中反转方程式,即将定义替换为

Definition is_left_neutral  (e: A) := …

我试图证明基于以下定义的引理。

Section lemma.

Variable A : Type.
Variable P : A -> Prop.

Variable P_dec : forall x, {P x}+{~P x}.

Inductive vector : nat -> Type :=
  | Vnil : vector O
  | Vcons : forall {n}, A -> vector n -> vector (S n).

  Arguments Vcons {_} _ _.

Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') …

作为我的一般问题的最小示例，假设我们有以下内容：

Parameter C: Prop.

Definition blah := C.

我想实施一种策略，该策略会blah在目标的所有假设中自动展开。

我试过这个：

Ltac my_auto_unfold := repeat match goal with 
  | [ H: ?P |- ?P ] => unfold blah in H
end.


Theorem g: blah -> blah -> blah.
Proof.
intros.
my_auto_unfold.

但只有一个假设已经blah展开。

我想通过添加一个定理来扩展Coq'Art中的练习6.10，该定理是：对于不是1月的所有月份，is_January将等于false。

我对月份的定义如下所示：

 Inductive month : Set :=
   | January : month
   | February : month
   | March : month
   | April : month
   | May : month
   | June : month
   | July : month
   | August : month
   | September : month
   | October : month
   | November : month
   | December : month
  .

Check month_rect.

我对is_January的定义如下所示：

Definition is_January (m : month) : Prop :=
  match m with
  | January => True
  | other   => False
  end.

我正在做以下测试，以证明它是正确的。 …

是否有一种策略可以使用而不是replace在下面的示例中来简化此表达式？

Require Import Vector.

Goal forall (n b:nat) (x:t nat n), (map (fun a => plus b a) x) = x.
Proof.
  intros n b x.
  replace (fun a => plus b a) with (plus b) by auto.
  ...

有时我会通过投射到不同的空间来做最好的证明.目前我做了以下事情:

remember (f x) as y eqn:H; clear H; clear x.

我尝试使用Ltac自动执行此操作:

Ltac project x y :=
  let z := fresh in
    remember x as y eqn:z; clear z; clear x.

但是我收到以下错误:

Error: Ltac variable x is bound to f x which cannot be coerced to a variable.

这是什么问题？

我想写一个带有可选变量名的策略.最初的战术看起来像这样:

Require Import Classical.

Ltac save := 
  let H := fresh in
  apply NNPP;
  intro H;
  apply H.

我想让用户有机会选择他想要的名字,并使用它:save a例如.

我用这个解决方案编写了一个变体:

Require Import Classical.

Inductive ltac_No_arg : Set :=
  | ltac_no_arg : ltac_No_arg.

Ltac savetactic h := 
  match type of h with
    | ltac_No_arg => let H := fresh in
      apply NNPP;
      intro H;
      apply H
    | _ => apply NNPP;
      intro h;
      apply h
  end.

Tactic Notation "save" := savetactic ltac_no_arg.
Tactic Notation …

我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身中 - 类似于在 Isar 中的做法。在 Coq 中如何做到这一点？例如：

have Lemma using Lemma1, Lemma2 by auto.

我知道这个exact陈述，想知道是否就是这样……但我也想得到这个陈述的证据，就像在伊萨尔我们有have by auto或using Proof. LEMMA_PROOF Qed.

为了使其具体化，我试图做这些非常简单的证明：

Module small_example.

  Theorem add_easy_induct_1:
    forall n:nat,
      n + 0 = n.
  Proof.
    intros.
    induction n as [| n' IH].
    - simpl. reflexivity.
    - simpl. rewrite -> IH. reflexivity.
  Qed.

  Theorem plus_n_Sm :
    forall n m : nat,
      S (n + m) = n + (S m).
  Proof. …