The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Hi,

then "rew eq_prf in x" from 
https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html can 
potentially help.

An example would be:
Require Import Coq.Vectors.Vector.

Inductive Tree (L: Set): Prop :=
| Node : forall (label: L) (arity: nat), (t L arity) -> Tree L.

Import EqNotations.

Inductive TreeRel (L: Set) (R: L -> L -> Prop): Tree L -> Tree L -> Prop :=
| InRel : forall l1 l2 arity1 arity2 (xs: t L arity1) (ys: t L arity2)
          (arity_eq: arity2 = arity1),
          R l1 l2 ->
          Forall2 R xs (rew [t L] arity_eq in ys) ->
          TreeRel L R (Node L l1 arity1 xs) (Node L l2 arity2 ys).

where the "rew [t L] arity_eq in ys" can also be written as "rew 
arity_eq in ys" whenever Coq is smart enough to detect the dependency of 
the rewritten expression on the subject of the equation.
There is also "rew <- arity_eq in" to get a right to left version of the 
equation.
In any case the equation can of course can be proven anywhere, 
especially in a lemma.

Also note, that datatypes formulated like this often get "stuck" in 
later proofs, where you have situations like
Foo xs (rew P in xs)
which you want to be
Foo xs xs

Should that be the case, Eqdep_dec 
(https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.Eqdep_dec.html) 
is very useful to replace P by eq_refl, which then causes rew eq_refl in 
xs to reduce to xs.

Bests,
 Jan


On 04/29/2017 01:50 PM, Klaus Ostermann wrote:
> Hi Jan,
>
> thanks for your answer! I'm not sure how to apply your suggestion, though.
> This error does not happen in a proof but in the definition of an
> inductive datatype.
> I tried to formulate your assertion (adapted to my situation) as a lemma
> and add it to the rewrite hint database,
> but that doesn't change the error.
>
> Any ideas? Maybe I need some kind of cast?
>
> Klaus
>
>
>
> Am 29/04/17 um 11:59 schrieb Jan Bessai:
> > Hi,
> >
> > > The term "fds" has type "id -> id -> {n : nat & eqn n}"
> > > while it is expected to have type "id -> id -> {n : nat & eqn n}"
> > > (cannot
> > > satisfy constraint
> > > "eqn (length tys1)" == "(fun n : nat => eqn n) (projT1 (fds f c))").
> > >
> > > The types that it wants to be identical are identical, and they are also
> > > identical if all implicit arguments, universe levels etc. are printed.
> >
> > I came across issues like that when porting a proof from Coq 8.5 to
> > 8.6. My guess is reduction during unification got less intelligent but
> > more predictable. I usually get around these cases doing something like
> >
> > assert (x_eq: x = f y). {
> >   unfold f; destruct y; simpl; reflexivity.
> > }
> > rewrite x_eq.
> >
> > potentially using "rewrite in" or simpler proofs for x_eq.
> >
> > This is a bit explicit and brittle, but I tend to prefer it over
> > overly intelligent magic.
> > Hope this helps.
> >
> > Bests,
> >  Jan