Arnaud DABY-SEESARAM (Feb 06 2023 at 13:07): Arnaud DABY-SEESARAM (Feb 06 2023 at 13:07):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.
Matthieu Sozeau (Feb 06 2023 at 13:36):It looks like a bug indeed, it should use a fresh name!
Arnaud DABY-SEESARAM (Feb 06 2023 at 13:46):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.
Matthieu Sozeau (Feb 06 2023 at 14:06):Indeed
Théo Winterhalter (Feb 06 2023 at 15:15):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.
Paolo Giarrusso (Feb 06 2023 at 15:19):Oh, so vnth is getting miscompiled ? EDIT: not quite
Paolo Giarrusso (Feb 06 2023 at 15:29):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".
Matthieu Sozeau (Feb 06 2023 at 15:34):Indeed.
Matthieu Sozeau (Feb 06 2023 at 15:35):I guess in practice you will quickly find out you have the wrong definition but it can slip through
James Wood (Feb 06 2023 at 15:47):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