构造函数的分解相等
构造函数的分解相等
提问于 2016-05-27 19:22:13
经常在Coq中，我发现自己做了以下工作:我有一个证明目标，例如：
some_constructor a c d = some_constructor b c d我只需要证明a = b，因为其他的一切都是一样的，所以我做了：
assert (a = b).然后证明那个子目标，然后
rewrite H.
reflexivity.完成了证据。
但是，在我的证据的最下面，让那些人在我身边闲逛似乎是不必要的混乱。
Coq中是否有一种一般策略，用于获取构造函数的相等，并将其分解为构造函数参数的相等(类似于split )，但用于等式而不是连词。
回答 2
Stack Overflow用户
回答已采纳
发布于 2016-05-28 09:40:00
特别是，标准Coq提供了f_equal策略。
Inductive u : Type := U : nat -> nat -> nat -> u.
Lemma U1 x y z1 z2 : U x y z1 = U x y z2.
f_equal同时，purpose提供了一种通用的一致性策略congr.
Stack Overflow用户
发布于 2016-05-27 19:52:36
您可以使用Coq的搜索功能：
Search (?X _ = ?X _).
Search (_ _ = _ _).在一些噪声中，它揭示了一个引理。
f_equal: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y以及多参数等式的兄弟关系：f_equal2 . f_equal5 ( Coq版本8.4)。
下面是一个示例：
Inductive silly : Set :=
| some_constructor : nat -> nat -> nat -> silly
| another_constructor : nat -> nat -> silly.
Goal forall x y,
x = 42 ->
y = 6 * 7 ->
some_constructor x 0 1 = some_constructor y 0 1.
intros x y Hx Hy.
apply f_equal3; try reflexivity.在这一点上，您需要证明的就是x = y。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/37490891
复制相关文章
相似问题
腾讯云开发者
