The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 22/09/2014 16:13, Rui Baptista a écrit :

(P t) doesn't in general imply (forall x, P x), so if you can prove (forall B : N, B ε A -> B ε el A) from just (B : N) and (B ε A → B ε el A), that's because the tactics you used know something more about ε or el or the variables involved.

 

I don't understand why you are using [generalize] after using [assert]. Neither B nor H17 occur in the conclusion. Doesn't that just copy B and H17 to the conclusion?

 

What [intuition] in [intuition auto] does is it tries to break down logical connectives and solve an intuitionistic propositional calculus problem. Since it doesn't succeed, [auto] then takes over from there by blindly [apply]-ing up to a certain depth all combinations of hypotheses and hints in the database. That search isn't very deep because it has exponential execution time. You can increase the search depth by using [auto n], where n is a natural. [auto] is equivalent to [auto 5]. Also, you can get more info by using [info_auto] instead of [auto].

 

    http://coq.inria.fr/distrib/current/refman/tactic-index.html

 

Regards

Good news! [firstorder] after [generalize B, H17] solves the problem.
All the best.

--

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard