鉴于使用;战术的有效Coq证明,是否有通用公式将其转换为有效的等效证明并.替换;？
许多Coq证明使用;或战术排序战术.作为一个初学者,我想看的各个步骤执行,所以我想替换.的;,但让我吃惊,我觉得这可能会破坏证据.
文档;很稀疏,我没有找到.任何地方的明确讨论.我确实看到了纸,上面写着非正式的意义t1; t2就是
适用于在当前证据背景下
t2执行的每个子目标t1,
我想知道是否.只对当前的子目标进行操作并解释了不同的行为？但是,尤其是我想知道如果有修复由替换破损的通用解决方案.的;.
通常在Coq我发现自己做了以下事情:我有证据目标,例如:
some_constructor a c d = some_constructor b c d
我真的只需要证明,a = b因为其他一切都是相同的,所以我这样做:
assert (a = b).
然后证明那个subgoal
rewrite H.
reflexivity.
完成证明.
但是,在我的证据的底部悬挂那些似乎是不必要的混乱.
在Coq中是否有一个通用的策略来获取构造函数的相等性并将其分解为构造函数参数的相等性,有点像是一个split但是对于平等而不是连接.
当在Ltac中实现复杂的策略时,有一些Ltac命令或策略调用我期望失败以及预期的位置(例如终止a repeat或导致回溯).这些故障通常在故障级别0时引发.
在较高级别上升的故障"逃离"周围try或repeat阻塞,并且对于发出意外故障是有用的.
我缺少的是一种运行策略tac并将其失败(即使在0级)处于更高水平,同时保留失败信息的方法.这将让我确保repeat不会因为我身边的Ltac编程错误而终止.
我能否在Ltac中实施这种提升级别的高阶战术？
我读到一种类型的归纳原理只是一个关于命题的定理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. …这似乎是一个非常简单的问题，但我找不到任何有用的东西。
我有声明
n - x = n
并想证明
(n - x) + x = n + x
我一直无法找到什么定理允许这样做。
如何rewrite在 ltac 中调用以仅重写一次？我认为 coq 的文档提到了一些关于rewrite at但我无法在实践中实际使用它并且没有示例的内容。
这是我正在尝试做的一个例子：
Definition f (a b: nat): nat.
Admitted.
Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.
Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*) …我正在尝试求解形式的等式
A * B * C * D * E = F
其中*一些复杂的左联想操作。
目前，一切是不透明的（包括*和A通过F），并且可以通过由透明autounfold with M_db。
问题是，如果我全局展开公式中的定义，那么简化将永远存在。相反，我想首先展开A * B，应用一些策略将其简化为正常形式X，然后对X * C诸如此类进行。
知道我将如何做到这一点吗？这是我目前的方法，但是in Aor at A无效。另外，我不清楚这是否是正确的结构，还是reduce_m应该返回某些东西。
Ltac reduce_m M :=
match M with
| ?A × ?B => reduce_m A;
reduce_m B;
simpl;
autorewrite with C_db
| ?A => autounfold with M_db (* in A *);
simpl;
autorewrite with C_db …当我查看 QuickChick 项目时，遇到了这句话“Require Import Ltac.我不知道这是做什么的以及Ltac模块在哪里”。我找到了一个文件plugins/ltac/Ltac.v，但这不可能是这个文件，因为该文件是空的（顺便说一句，包含空文件的目的是什么？）。我尝试过Locate Ltac.，但得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更令人困惑。
该模块的作用是什么Ltac，文件在哪里Ltac.v，为什么该Loacte命令在这种情况下不起作用？谢谢！
我正在考虑编写策略，该策略将考虑多个目标并据此做出决策。但是，当我match goal with盯着一个目标使用时，怎么说“请找到另一个看起来像这样的目标”？
或更确切地说，一个更笼统的问题是，如何在Ltac中切换目标？
我工作在以下定理的证明Sn_le_Sm__n_le_m中IndProp.v的软件基础（第1卷：逻辑基础）。
Theorem Sn_le_Sm__n_le_m : ?n m,
S n ? S m ? n ? m.
Proof.
intros n m HS.
induction HS as [ | m' Hm' IHm'].
- (* le_n *) (* Failed Here *)
- (* le_S *) apply IHSm'.
Admitted.
其中，的定义le (i.e., ?)是：
Inductive le : nat ? nat ? Prop :=
| le_n n : le n n
| le_S n m (H : le n m) : …