The Coq mailing list

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

Hi all,
I have the following problem with the tactic "intuition auto".
Starting with simple variables of type (N : Type) and a relation ε : N ->N->Prop

B : N
H7 : B ε A → B ε el A

then, applying tactic :  assert (H1 : forall B, (B ε A -> B ε el A)).

followed by :

generalize B, H7.
intuition auto.

Succeeds by adding hypothesis: H1 : ∀ B : N, B ε A → B ε el A.

However, the same mechanism fails in the following case :

with hypothesis : H17 : B ε el A → ∃ C D : N, C ε a ∧ D ε el C ∧ D ε el B.

the sequence :

assert (H18 : forall B, (B ε el A → exists C D, (C ε a /\ D ε (el C) /\ D ε (el B)))).

generalize B, H17.
intuition auto.
-> does not add hypothesis H18.

If somebody has an idea...
Thanks in advance,
Richard

--

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