The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Thanks a lot, using R_bool_of_nat and R_bool_of_nat_complete as hints for 
eauto, the goal is solved automatically in my case.
Have a nice weekend,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Friday 24 February 2012 18:15:27 Pierre Courtieu wrote:
> I don't think there is something for this exactly but there is
> something that probably fits (better?) your needs: functional
> inversion.
> 
> See for example below how it deduces automatically from hypothesis
> "bool_of_nat n = true" that n is "S of something".
> 
> You have to either define your function with Function or use Functional
> Scheme.
> 
> P.
> 
> -------------8X------------------------
> 
> Function bool_of_nat (n:nat): bool :=
>   match n with O => false | S x => true end.
> 
> Goal forall n, bool_of_nat n = true -> exists m, n = S m.
> 
> intros n H.
> functional inversion H.
> exists x.
> reflexivity.
> Qed.
> 
> -----------------------68X----------------------
> 
> 2012/2/24 Paolo Herms 
> <paolo.herms AT cea.fr>:
> > Hello,
> > is there a tactic to solve something like this automatically?
> > 
> > Definition bool_of_nat n := match n with O => false | S x => true end.
> > Goal exists n, bool_of_nat n = true.
> > 
> > Thank you,