I have a question regarding arguments renaming in Equations:

Using an inductive type vec defined as follows:

```
Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A 0
| vcons (a : A) (n : nat) (v : vec A n) : vec A (S n).
```

I realized that the following definition is accepted:

```
Equations vnth {A n} (v : vec A n) (x : fin n) : A :=
vnth (vcons _ a) (fin0) := a ;
vnth (vcons _(*<- a *) a(*<- a0*) ) (finS f) := vnth a0 f.
```

My understanding is that in both cases, `v`

is matched as `vcons a a0`

.

Is this an expected behaviour?

I feel like the name Equations choose for placeholder variables should not

take precedence over those chosen by the user.

It looks like a bug indeed, it should use a fresh name!

The issue might come from the order in which the variables are named, the placeholder-variables names should probably be picked after those provided by the user.

Indeed

I mean, it's worse than this, the name it uses on the rhs of the first clause, `a`

refers to the underscore on the left, and not to explicitly named `a`

.

~~Oh, so vnth is getting ~~ EDIT: not quite*miscompiled* ?

But I guess this is a (low severity?) Pollack inconsistency bug: you probably *can* use this to trigger miscompilation, if the bug swaps variables of the same type? I recall Enrico arguing such bugs arise in HOL-based assistants and can be serious, even if they don't affect the "kernel".

Indeed.

I guess in practice you will quickly find out you have the wrong definition but it can slip through

```
From Equations Require Import Equations.
Inductive foo : Type := mkFoo (a b : nat).
Equations snd : foo -> nat :=
snd (mkFoo _ a) := a.
Compute snd (mkFoo 0 1).
Check eq_refl : snd (mkFoo 0 1) = 0.
```

Yep that's pretty terrible

Last updated: Sep 09 2024 at 05:02 UTC