0 
Require Import ProofWeb.

Variables x y z a : D.
Variables p: D * D * D -> Prop.

Theorem letra_a : (all x, p(a,x,x) /\  (all x, ( all y, ( all z, p(x,y,z))) -> p(f(x),y,f(z)))) -> p(f(a),a,f(a)).
Proof.
intros.
imp_e (p(a,a,a)).
destruct H.

现在问题出在哪里，我需要 p (a, a, a) -> p (fa, a, fa) 从所有 x, all y, all z, p (x, y, z) 中很明显 - > p (fx, y, fz) 只需要实例化 x,y 和 z = a，但我做不到。我所做的任何事情在这里都不被接受。

f_all_e H0.

给我错误：战术失败：（论证不是一个普遍量化的公式或不符合目标）。

如果我尝试 all_e (all x, all y, all z, p (x, y, z) -> p (fx, y, fz))。错误：战术失败：（论点不是普遍的量化）。

你能帮忙吗？我已经全面挖掘 Coq 信息，打印 PDF，一直在尝试但仍然无法掌握 Coq 的语法和逻辑流程，我仍然非常迷失其中。

提前感谢您的任何指点！

找到的解决方案：

Theorem letra_c : (all y, q b y) /\ (all x, (all y, (q x y -> q (s x) (s y))) ) -> ( exi z, (q b z /\ q z (s (s b))) ).
Proof.
intros.
destruct H.
exi_i (s b).
con_i.
apply H.
imp_e (q b (s b)). 
all_e (all y, (q b y -> q (s b) (s y))).
all_e (all x, (all y0, (q x y0 -> q (s x) (s y0)))).
apply H0.
apply H.
Qed.
4

1 回答 1

1 
H : all x, p (a, x, x)
H0 : all x, all y, all z, p (x, y, z) -> p (f x, y, f z)
H1 : p (a, a, a)
============================
 p (f a, a, f a)

在常规 Coq 中，您可以：

  • apply H0，这将产生目标p (a, a, a)，很容易解决；

  • specialize (H0 a a a)，这会给你H0: p (a, a, a) -> p (f a, a, f a)；

  • 或者只是去exact (H0 _ _ _ H1)完成它。

现在，我尝试使用http://prover.cs.ru.nl/index.html来完成您的目标，但我也找不到该命令。

我会考虑某种向前的全部消除，或向后的方式，但我也无法让它发挥作用。你有这方面的文件吗？

于 2012-08-31T00:17:18.597 回答