Ssreflect Users Discussion List

[Guillaume Cano <>]

Thank you.

Best,
Guillaume.

----- Mail original -----
> De: "Cyril Cohen" <>
> À: "Guillaume Cano" <>, 
> Envoyé: Jeudi 20 Juin 2013 18:00:14
> Objet: Re: problem with done and convertibility
> 
> 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
>