The Coq mailing list

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

Further to this, I have noticed that I can get

Show.

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

Check no_rpt_same seq_ord
    (derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
       l0 d1).

(yes this is exactly cutting and pasting the output of Show)

and this gives a type error.

The term "d1" has type "dersrec LJArules emptyT lpst"
while it is expected to have type
 "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)]"
(cannot unify "lpst" and
"[(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)]").

I don't understand how this can be possible.  Wouldn't you expect Coq to 
refuse to have a goal containing a type error?  What would be happening 
here?

Thanks

Jeremy

On 29/12/20 12:10 am, Jeremy Dawson wrote:
> 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