The Coq mailing list

[Victor Porton <porton AT narod.ru>]

(Thomas Braibant, it is a modified version of the email I've sent to you. Now 
I also send it to the mailing list which I forgotten in my previous email.)

18.11.2011, 22:46, "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 ?

No, I understand that tactics here would be similar for the declarative mode 
and plain tactic scripts.

> 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) ?

Yes, I am failing.

> 3) Are you failing to produce a proof of your theorem at all (a real
> beginner's question)?

Yes, I'm failing to produce a proof of my theorem at all. (Maybe I would be 
able to write a long highly manual proof, but that's irrelevant.)

> if 1), then I leave people more versed in the declarative mode to answer.

Not the case.

> 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.

Thanks I am to read stuff about tactics.

I found an other trouble:

This does not compile:

[[[[
Require Import sset1.

Variable A B C : Set.

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

(*Axiom sub_trans : forall a b c, sub a b -> sub b c -> sub a c.*)
Theorem thm: (sub A C).
proof.
thus thesis by (sub_trans _ _ _ ax1 ax2).
end proof. Qed.
]]]]

It compiles only in the case if I add @ to sub_trans:

[[[[
Require Import sset1.

Variable A B C : Set.

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

(*Axiom sub_trans : forall a b c, sub a b -> sub b c -> sub a c.*)
Theorem thm: (sub A C).
proof.
thus thesis by (@sub_trans _ _ _ ax1 ax2).
end proof. Qed.
]]]]

I wonder why now it requires @, as sub_trans defined in sset1.v (in GAIA) 
seems to not have any implicit arguments. Why @ is required?

> 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

-- 
Victor Porton - http://portonvictor.org