logic - coq how to use apply to "extract" a implication -


sorry weird title, not know how put in words. i'll illustrate using example.

h : r -> p -> q

h0 : r

subgoal:

(q -> p) \ / (p -> q)

so question how extract out (p->q). have r already, when 'apply h in h0', evaluates , gives me q.

any appreciated since started using coq.

you can of:

specialize (h h0). 

to replace h h: p -> q, or:

pose proof (h h0) h1 

to introduce h1: p -> q

you can go forward:

right. exact (h h0). 

Comments

Popular posts from this blog

javascript - jQuery: Add class depending on URL in the best way -

caching - How to check if a url path exists in the service worker cache -

Redirect to a HTTPS version using .htaccess -