The Coq mailing list

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

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