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.
Now here's where the problem is, I need p (a, a, a) -> p (f a, a, f a) Which is pretty obvious from all x, all y, all z, p (x, y, z) -> p (f x, y, f z) Just need to instantiate x,y and z = a, but I can't. Nothing I do is accepted here.
f_all_e H0.
Gives me Error: Tactic failure: (argument is not a universally quantified formula or does not fit the goal).
If I try all_e (all x, all y, all z, p (x, y, z) -> p (f x, y, f z)). Error: Tactic failure: (the argument is not a universal quantification).
Can you please help? I've mined Coq information all over, printed PDF's, been trying but still can't get a hang of Coq's syntax and logic flow, I'm still pretty much lost in it.
Thanks in advance for any pointers!
Solution found:
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.
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)
In regular Coq, you could either:
apply H0, which would yield the goal p (a, a, a), easily solved ;
specialize (H0 a a a), which would give you H0: p (a, a, a) -> p (f a, a, f a) ;
or just go exact (H0 _ _ _ H1) and finish that already.
Now, I tried using http://prover.cs.ru.nl/index.html to finish your goal, but I can't quite find the command either.
I would have thought about some sort of forward forall elimination, or backward modus ponens, but I cannot make it work either. Do you have a documentation for this?