The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 16 Nov 2012 11:59:20 +0100,
Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>
 a écrit :

> > I think there lacks some tactics on eta expansion.
> >
> > Of course I can prove this goal using the change tactic, but I know
> > no otherway than change to expand/contract eta.
> >
> 
> Truth is, pattern-matching in tactics is not really done up to
> conversion, but some limited reduction is done here and there. For
> instance, here is another example that doesn't work, yet doesn't
> involve eta:
> 
> Goal forall x y:nat, x+1=y -> x+1 = y.
> Proof.
>   intros x y h.
>   change (x+1) with ((fun z => z+1) x).
>   rewrite h.
>   (* Error: Found no subterm matching "x + 1" in the current goal. *)
> 
> It's never really clear when to try and reduce terms. That said, when
> we do, there is no eta being done because eta-reduction isn't sound
> (something to do with subtyping). There has been some talk about
> adding some eta in reduction when possible, though. It wouldn't solve
> your case here, I think, but in the case of [y=l -> x=l] it would
> probably work.

What do you mean by 'eta-reduction' is unsound?

> 
> 
> 
> > I know it has nothing to do with that, but will 'native' proof
> > irrelevance be built on a future Coq version (or more precisely will
> > that be planned), like it has been done for eta (I mean
> > automatically unify elements of same Prop without inspecting them)?
> >
> > Or do some people work in theory where proof-irrelevance contradicts
> > the other lemmas.
> >
> 
> It's been on the todo list for more than half a decade I think. It's
> still not entirely clear how to do it (and it may break a few things).