The Coq mailing list

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

Hi.

Marko Malikoviæ a écrit :
> Greetings for everybody,
>
> I'm new in Coq. Please, can somebody explain to me this error:
>
> Coq < Section Proba.
>
> Coq < Variable A B:Prop.
> A is assumed
> B is assumed
>
> Coq < Hypothesis H:A.
> H is assumed
>
> Coq < Goal A /\ B.
> 1 subgoal
>
>   A : Prop
>   B : Prop
>   H : A
>   ============================
>    A /\ B
>
> Unnamed_thm < split;assumption.
> Toplevel input, characters 6-16
>   
The tactic "split" generates two subgoals, and the tactic "assumption" 
is applied to each of one (because of the
operator ";").

The first subgoal (proving A) is solved immediately. But the tactic 
"assumption" fails on the second one
(proving B) because you have not assumed B.


If you add the hypothesis H':B, your tactic works.
Notice that with "split; try assumption", the first subgoal is solved, 
and the second one remains unsolved.

Pierre





> > split;assumption.
> >       ^^^^^^^^^^
> >     
> User error: No such assumption
>
> Thank you very much,
>
> Marko Malikoviæ
> Faculty of Arts and Sciences in Rijeka, Croatia
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>