Ssreflect Users Discussion List

[Cyril Cohen <>]

Yes, I think that the tactic trivial tries to match the pattern against the
goal without conversion (or too few).
(sorry, I forgot to answer to the list)

Le 20/06/2013 17:45, Guillaume Cano a écrit :
> Hi Cyril,
> 
> That means that the tactic trivial checks the pattern of the Hint
> and tries to apply it only if they are the same pattern of the Goal ?
> 
> Because just "apply normr_ge0" solves the Goal.
> 
> Cheers,
> Guillaume.
> 
> ----- Mail original -----
>> De: "Cyril Cohen" <>
>> À: "Guillaume Cano" <>
>> Envoyé: Jeudi 20 Juin 2013 17:14:23
>> Objet: Re: problem with done and convertibility
>>
>> Hi Guillaume,
>>
>> Le 20/06/2013 13:53, Guillaume Cano a écrit :
>>> Lemma H (x : R) : true && (0 <= `|x|). Proof. by rewrite /=. Qed.
>>> Why I can't replace   "by rewrite /="  by "done" ?
>>
>> I think the reason is the following:
>> The reason why 0 <= `|x| is solved by done is that there is a Hint
>> (namely
>> normr_ge0) with priority 0 (and done, tries the tactic "trivial").
>> But if you
>> have true && (0 <= `|x|) instead, trivial doesn't recognize a Hint is
>> applicable, hence your need to simplify first.
>>
>> Cheers,
>> --
>> Cyril
>>
> 

-- 
Cyril