Coq：实例化多重泛化？

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，一，FA）这是从所有的X，Y全部，所有的Z，P很明显（x，y，z） - > p（fx，y，fz）只需要实例化x，y和z = a，但我不能。我没有做任何事情在这里被接受Coq：实例化多重泛化？

f_all_e H0.

给我错误：策略失败：（参数不是普遍量化公式或不适合的目标）。如果我尝试 all_e（所有的x，所有的y，所有的z，p（x，y，z） - > p（f x，y，f z））。错误：战术失败:(参数不是一个通用的量化）。

你能帮忙吗？我已经挖掘了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.

来源

2012-08-30 Jose Fonseca

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)

在常规勒柯克，你既可以：

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来完成你的目标，但我不能完全要么找到的命令。

我会考虑某种前向消除或向后的方式ponens，但我也无法使其工作。你有这个文件吗？

来源

2012-08-31 00:17:18 Ptival

嗨。我想我在#irc看到你的昵称了？感谢您的帮助。我结束了解决这样的：变量问：d - > d - >支柱变量S：d - > D. 变量B：D. 定理letra_c：（所有的Y，QBY）/ \ （所有x，所有y，qxy→q（sx）（sy））→（exi z，qbz/\ qz（s（sb）））。证明。介绍。破坏H. con_i。 exi_i。适用H. Qed。昨天，我放弃了昨天的几个小时后...... 非常感谢，再次。 –

也许发布您的解决方案作为答案，并将其标记为接受。 - 是的，我在IRC上 – Ptival

Coq：实例化多重泛化？

回答

相关问题