The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Fixpoints only reduce if the structural argument is a constructor. In 
your example that was not the case (hence Jason's suggestion to perform 
a [destruct n']). However, since your definition of [closed] is 
non-recursive, a better solution is to declare it using [Definition], so 
this restriction on reductions does not apply.

On 02/13/2014 08:38 AM, Ömer Sinan Ağacan wrote:
> Thank you Jason. Using Definition instead of Fixpoint worked. I don't
> understand the problem, though. Can anyone explain me what's wrong
> with using Fixpoint here?
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net
>
>
> 2014-02-13 1:12 GMT+02:00 Jason Gross 
> <jasongross9 AT gmail.com>:
> > Use [Definition] for [closed] rather than [Fixpoint].  Alternatively, use
> > [destruct n'; simpl in *].
> >
> > -Jason
> >
> >
> > On Wed, Feb 12, 2014 at 4:46 PM, Ömer Sinan Ağacan 
> > <omeragacan AT gmail.com>
> > wrote:
> > > Hi all,
> > >
> > > I'm stuck with this:
> > >
> > >
> > > H3 : (fix closed (n : nat) (t : tm) {struct n} : Prop :=
> > >          fvs n t = empty_set id) n' e'
> > > ==========================================
> > > fvs n' e' = empty_set id
> > >
> > >
> > > Any ideas how to prove this?
> > >
> > > Thanks ..
> > >
> > > ---
> > > Ömer Sinan Ağacan
> > > http://osa1.net