标签: coq-tactic

在Coq中，当试图证明记录相等时，是否有一种策略可以将其分解为所有字段相等？例如，

Record R := {x:nat;y:nat}.

Variables a b c d : nat.

Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.

有没有一种策略可以将其减少到a = c /\ b = d？请注意，一般而言，任何一个a b c d可能都是复杂的大型证明术语（然后我可以使用证明不相关公理来执行）。

我读到一种类型的归纳原理只是一个关于命题的定理P.所以我构建了一个List基于右(或反向)列表构造函数的归纳原理.

Definition rcons {X:Type} (l:list X) (x:X) : list X := 
  l ++ x::nil.

归纳原理本身是:

Definition true_for_nil {X:Type}(P:list X -> Prop) : Prop :=
  P nil.

Definition true_for_list {X:Type} (P:list X -> Prop) : Prop :=
  forall xs, P xs.

Definition preserved_by_rcons {X:Type} (P: list X -> Prop): Prop :=
  forall xs' x, P xs' -> P (rcons xs' x).

Theorem list_ind_rcons: 
  forall {X:Type} (P:list X -> Prop),
    true_for_nil P ->
    preserved_by_rcons P ->
    true_for_list P. …

我正在考虑编写策略，该策略将考虑多个目标并据此做出决策。但是，当我match goal with盯着一个目标使用时，怎么说“请找到另一个看起来像这样的目标”？

或更确切地说，一个更笼统的问题是，如何在Ltac中切换目标？

我发现自己经常想通过类型而不是名称来引用假设。尤其是在语义规则倒置的证明中，即具有几种情况的规则，每种情况可能都有多个先例。

我知道如何使用来完成此操作match goal with ...，如以下简单示例所示。

Lemma l0:
  forall P1 P2,
    P1 \/ (P1 = P2) ->
    P2 ->
    P1.
Proof.
  intros.
  match goal with H:_ \/ _ |- _ => destruct H as [H1|H2] end.
  assumption.
  match goal with H: _ = _ |- _ => rewrite H end.
  assumption.
Qed.

有没有更简洁的方法？还是更好的方法？

（诸如的引入模式intros [???? HA HB|??? HA|????? HA HB HC HD]不是一个选择，我已经厌倦了找到正确数量的?s！）

例如，是否可以编写grab将模式和策略结合起来的策略，如

  grab [H:P1 \/ _] => rename H into HH.
  grab …

在使用 Coqapply ... with策略时，我看到的所有示例都涉及明确给出要实例化的变量的名称。例如，给定一个关于等式传递性的定理。

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.

给apply它：

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m. 
  apply trans_eq with (m := 1). Qed.

请注意，在最后一行中apply trans_eq with (m := 1).，我必须记住要实例化的变量的名称是m，而不是oorn或其他一些名称y。

对我来说，在定理的原始陈述中是否使用m n o或x …

我多次遇到这个问题：我在 Coq 中有一个证明状态，其中包括等式两边相同的匹配项。

是否有一种标准方法可以将多个匹配重写为一个？

例如。

match expression_evaling_to_Z with
    Zarith.Z0 => something
    Zartih.Pos _ => something_else
    Zarith.Neg _ => something_else
end = yet_another_thing.

如果我破坏，expresion_evaling_to_Z我会得到两个相同的目标。我想找到一种方法来实现其中一个目标。

我创建了这个示例类型来演示我遇到的问题：

Inductive foo : nat -> Prop :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

现在很清楚foo_1 0 <> foo_2 0，但我无法证明这一点：

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H.

这将返回错误

不是可歧视的平等。

inversion H根本不会改变上下文。奇怪的是，如果我foo从Prop改为 ，Type那么证明会通过，但我不能在我的实际代码中这样做，因为它会导致其他地方出现问题。

我怎样才能得到这个证明？为什么这首先是有问题的？

我有以下引理证明不完整:

Lemma (s_is_plus_one : forall n:nat, S n = n + 1).
Proof.
  intros.
  reflexivity.
Qed.

这个证明失败了

Unable to unify "n + 1" with "S n".

似乎eq_S是证明这一点的方法,但我无法应用它(它不承认n + 1为S n:) Error: Unable to find an instance for the variable y..我也试过ring,但找不到关系.当我使用rewrite它时,它只会降低到相同的最终目标.

我怎样才能完成这个证明？

我正在尝试编写一个返回值的策略，在此过程中需要检查某些内容是否是 evar。

不幸的是，我无法使用is_evar，因为这样该策略不被视为返回值（而是另一种策略）。下面是一个例子。

有什么建议么？

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => is_evar e; 
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

我的问题与下面链接中提出的问题非常相似，但基于假设而不是目标。

在 Coq 中将函数应用于等式两边？

假设我有以下定义：

Definition make_couple (a:nat) (b:nat) := (a, b).

并证明以下引理：

a, b : nat
H : (a, b) = make_couple a b
-------------------------------
(some goal to prove)

我想提出以下假设：

new_H : fst (a, b) = fst (make_couple a b)

一种方法是显式编写断言，然后使用 eapply f_equal ：

assert (fst (a, b) = fst (make_couple a b)). eapply f_equal; eauto.

但如果可能的话，我想避免显式地编写断言。我想要一些像这样工作的策略或等效策略：

apply_in_hypo fst H as new_H

Coq 中有什么东西可以接近这个吗？

感谢您的回答。