The Coq mailing list

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

On Sun, Apr 25, 2010 at 11:08 AM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
>
> 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.

Could you elaborate the definition of heterogenous relations?
Intuitively, we cannot simply show p can be replaced by p'.
p represents a proof of "forall n, f n = n -> Prop", and p' is a constructive
proof of "forall n, n = n -> Prop", they can be quite different.
We must show in any context where these proofs are manipulated,
p and p' are equivalent. Thanks.

>
> -- Matthieu



-- 
Jianzhou