CODEWITHSUNDEEP
coqcoq-tactic
HouseCorgi
HouseCorgi

Reputation: 21

Applying lemma using Vectors in Coq

I have proved the following

Lemma exists_distribution: 
forall (a:Prop)(Omega:Set)(p:Omega->Prop),
(exists x:Omega, p x->a)<->
((exists x:Omega,~(p x))\/(exists x:Omega,a)).

Now I would like to prove it for p taking an arbitrary number of arguments from Omega. So I assume the following would be the general case for the previous lemma

Require Import Coq.Vectors.Vector.
Import VectorNotations.


Lemma exists_distribution_n: 
forall (a:Prop)(n:nat)(Omega:Set)(p:Vector.t Omega n->Prop),
(exists x:Vector.t Omega n, p x->a)<->
((exists x:Vector.t Omega n,~(p x))\/(exists x:Vector.t Omega n,a)).

which I proved just fine. However I can't apply it to the following

Lemma implication: 
forall (a: Prop) (Omega:Set) (p: Omega->Prop), 
exists x :Omega, 
p x  -> a.

Coq says that it cannot unify the two expressions, is my approach the wrong one?

Assuming n=3 is p:Vector.t Omega n->Prop the same as p:Omega->Omega->Omega->Prop or p:Omega* Omega* Omega->Prop?

Upvotes: 0

Views: 37

Answers (0)

Related Questions