The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Thanks Clement, that's very helpful!
Cheers, Jeremy

On 17/12/20 5:05 pm, Clément Pit-Claudel wrote:
> 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