The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

There are several way to understand your beginner's question.

1) Are you asking for help to understand subtleties of the  declarative mode ?
2) Are you failing to produce a proof of your theorem using the
declarative mode (that is, you were not able to produce a  proof with
"enough justification", which is blocking for you) ?
3) Are you failing to produce a proof of your theorem at all (a real
beginner's question)?

if 1), then I leave people more versed in the declarative mode to answer.
if 2), then the script attached works, but I would suggest to re-read
the manual: it really helps. Or to use the usual proof mode.
if 3), then re-read any tutorial.

Cheers,
thomas

Variable A B C : Set.

Variable sub : Set -> Set -> Prop.
Axiom ax1: (sub A B).
Axiom ax2: (sub B C).

Axiom transitive : forall A B C, sub A B -> sub B C -> sub A C.
Theorem thm: (sub A C).
proof.
thus thesis by (transitive _ _ _ ax1 ax2).
end proof. Qed.


On Fri, Nov 18, 2011 at 5:47 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> The following source file does not verify, saying "Warning: Insufficient 
> justification."
>
> What is my error?
>
> [[[
> Require Import sset1.
>
> Variable A B C: Set.
>
> Axiom ax1: (sub A B).
> Axiom ax2: (sub B C).
>
> Theorem thm: (sub A C).
> proof.
> š(*thus thesis by ax1, ax2, sub_trans using auto.*)
> šthus thesis by ax1, ax2 using apply sub_trans.
> end proof. Qed.
> ]]]
>
> BTW, here the lemma from GAIA which I use:
>
> Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c.
> Proof. by move => a b c sab sbc x xa; apply sbc; apply sab. Qed.
>
> --
> Victor Porton - http://portonvictor.org
>