The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

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?

-- 
Jianzhou