The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

This is the short version of your problem, I think:

  Require Coq.Vectors.Vector.

  Goal forall n (v: Vector.t nat (S (n + 0))),
      @Vector.hd (n + 0) v = 0 -> True.
  Proof.
    intros.

    Fail rewrite plus_n_O in v.
    (* Error: Cannot change v, it is used in hypothesis H. *)

    remember (n + 0) as n0 eqn:Heq in *.
    rewrite <- plus_n_O in Heq.
    subst.

The first rewrite fails because H would be ill-typed if it succeeded: you'd 
have (v: S n) and (H: @Vector.hd (n + 0) v); the latter is ill-typed because 
(n + 0) and n are not unifiable.
So what you need to do is rewrite in both hypotheses at once, so that there's 
no ill-typed intermediate stage.  You can do this with [remember] and [subst] 
as I did above (and as you observed) or with revert:

  Require Coq.Vectors.Vector.

  Goal forall n (v: Vector.t nat (S (n + 0))),
      Vector.hd v = 0 -> True.
  Proof.
    intros.

    Fail rewrite plus_n_O in v.
    (* Error: Cannot change v, it is used in hypothesis H. *)

    revert v H.
    rewrite <- plus_n_O.
    intros.

The key is that you can't rewrite an hypothesis' type if that leads other 
hypotheses to being ill-typed.

Clément.

On 12/16/20 11:42 PM, Jeremy Dawson wrote:
> curiouser and curiouser -
> 
> in investigating how I got to this situation I found that
> Coq would substitute (using subst.) the following equality in l and d1
> 
> Γ0 = Γ1 ++ []
> 
> So doing rewrite app_nil_r before substituting solves my problem in this 
> particular case.
> 
> But in general - (1) why can you do subst but not rewrite in d1
> (2) in general, how do you handle this problem
> 
> Jeremy
> 
> On 17/12/20 2:43 pm, Jeremy Dawson wrote:
>>
>> Hi,
>>
>> I have the following goal (only key parts included)
>>
>>    l : LJArules (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
>>          (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p)
>>    d1 : dersrec LJArules prems (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
>>    apd : allDT (no_rpt_same seq_ord (prems:=prems))
>>            (derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) l d1)
>>    ============================
>>    allDT (no_rpt_same seq_ord (prems:=prems))
>>      (derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) ?l ?d1)
>>
>> Now the goal doesn't match apd because the types are wrong,
>> ?l and ?d1 have types which would match those of l and d1 if
>> l and d1 had (Γ1 ++ []) rewritten to Γ1
>>
>> But rewrite app_nil_r in d1.  rewrite app_nil_r in l.
>> fails because
>> Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
>> d1 is used in hypothesis apd.
>> Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
>> l is used in hypothesis apd.
>>
>> How can I handle this situation?
>>
>> Thanks
>>
>> Jeremy
>>