The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 25 avr. 2010 à 09:52, Jianzhou Zhao a écrit :

> Hi,

Hi,

> The code bellow was simplified to demonstrate the problem:
> 
> Parameter f : nat -> nat.
> Axiom f_def : forall n:nat, f n = n.
> 
> Lemma L :
>  forall n (eq:f n = n) (p:forall n, f n = n->Prop),
>  p n eq=True -> n = 0.
> intros n.
>  rewrite f_def.
> 
> This last rewrite fails, because if f_def change (f n) to n,
> eq changes its signature, not matching p's type.
> The tactic 'pattern (f n)' fails for the same reason.
> The binder (forall n,) stops rewriting.
> 
> Can setoid_rewrite solve this problem? It claims it
> works under binders 
> (http://coq.inria.fr/refman/Reference-Manual030.html#toc165)
> 
> Coq > intro n. setoid_rewrite f_def.
> Error: found no subterm matching 'f ..." in the current goal.
> 
> Coq > intros n eq p. setoid_rewrite f_def in p.
> Anomaly: build_signature: not enough products. Please report.
> 
> I thought the default eq relation '=' should be also a well-formed setoid.
> Is my case the problem setoid addessed?

Indeed it claims to work under binders, but it's not possible in 
general to rewrite in hypotheses that are used in other hypotheses
(the same limitation appears in the standard rewrite in most cases).
As p's type would change after the rewrite, we would have to modify 
the [p n eq=True] hypothesis in some (as far as I can see) unknown way.
Also, the only "relations" between [p : forall n, f n = n -> Prop]
and [p' : forall n, n = n -> Prop] are heterogenous and currently 
rewriting expects homogeneous relations only (e.g, typeable as [relation 
foo]).
The anomaly you got is now a regular error though.

-- Matthieu