The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

On 29/08/2012 03:18, like wrote:
> Hi: Pierre Casteran
> I am a fish in this area. How can I fix this problem. Can you give me some
> suggestions.Is there something wrong with model_p?

Hi,

 (according to the .v file you sent us) the problem comes from the
predicate "derivable" you just declared and did not really define.
So, your goal reduces to something like

H : derivable t1 pi
----------------------
derivable t2 pi

where t1 and t2 are formulas.

Since your type of formulas contains a lot of constructors ( For, Fnext, 
prj, etc. ) it seems to be very difficult to prove such a goal with only 
the axiom t2, which doesn't match the current goal.

So you should either define "derivable" (by a cofixpoint maybe) or
give enough axioms for expressing the relationship between derivability
and the constructors of formulas.


What you sent us seems to be related with a formalizatio of temporal 
logic in Coq. I think that some people should have studied this problem
already.


Pierre