The Coq mailing list

[Clement Renard <Clement.Renard AT inria.fr>]

Hi,



On Thu, 4 Oct 2001, Bauer, Robert wrote:

> Hi,
> 
> I want to complete a simple proof without using "auto" - here's the relevant
> part:
> 
> a: Prop
> b: Prop
> H: a /\ b
> H0 : a
> H1 : b
> ============
> a \/ b
> 
> I know that a -> a \/ b, but can't seem to figure out what command to give
> for the next step in the proof.

You can use "Left." if you want to prove "a" or "Right." if you want to
prove "b". 

> Along the same lines, suppose I had
> 
> H0: a
> H1: a->b
> ========
> b
> 
> In hol, I would do something like modus ponens on the assumptions, and
> rewrite - I can't figure out how to do the modus ponens on the
> assumption to get H2: b - so that I could use Exact.

You can use the tactic "Apply". Here You can use "Apply H1." and you
will have to prove "a". Then you can conclude with "Exact H0."

> Thanks.

You should have a look at the Coq tutorial where you can find some
examples to get started with Coq. 
http://coq.inria.fr/doc/tutorial.html ;


Clement Renard