The Coq mailing list

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

Thanks Clement, this has been very helpful indeed, and has enabled me to 
solve this sort of problem several times.

But in some cases I still seem to be stuck.

For example (just showing the last two hypotheses), I have


 H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
      (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
  n : no_rpt_same seq_ord
        (derI
           (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], 
Var p)
           ?l0 d1)
  ============================
  no_rpt_same seq_ord
    (derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
       l0 d1)

exact n. fails with the error message

The term "n" has type
 "no_rpt_same seq_ord
    (derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
       ?l0 d1)" while it is expected to have type
 "no_rpt_same seq_ord
    (derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
       l0 d1)"
(cannot unify "[(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0],
                Var p0);
               (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]" 
[note - the above few lines are part of the type of l0]
and
"lpst").

I'm presuming this is because the existential ?l0 is expected to have 
type involving lpst.  Is there a way of getting Coq to show the type of 
an existential?

subst lpst. here gives a really long error message,

> subst lpst.
> ^^^^^^^^^^
Error: Ltac call to "subst (ne_var_list)" failed.
       Abstracting over the term "lpst" leads to a term
fun lpst0 : list (list (PropF V) * PropF V) =>
forall
[snip]
which is ill-typed.
Reason is: Illegal application:
The term "derI" of type
[snip]
cannot be applied to the terms
[snip]
The 7th term has type "dersrec LJArules emptyT lpst0"
which should be coercible to
 "dersrec LJArules emptyT
    [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
    (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]".

So if I'm right in thinking that the type of ?l0 is something containing 
lpst, how to I change that to the corresponding term on the rhs of H?

Thanks for any help

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