list_solve no longer solves a goal

[joscoh]

On VST 2.9.1, list_solve solved the following goal:

l: list A
i: Z
x: A
H: 0 <= i < Zlength l
----------------------------------------------------------------------
sublist 0 i (upd_Znth i l x) ++
sublist (i + 1) (Zlength (upd_Znth i l x)) (upd_Znth i l x) = 
sublist 0 i l ++ sublist (i + 1) (Zlength l) l

On VST 2.11.1, list_solve fails. It can easily be solved manually:

rewrite sublist_upd_Znth_l by lia.
rewrite Zlength_upd_Znth, sublist_upd_Znth_r by lia. 
reflexivity.

[QinshiWang]

You need an Inhabitant A to make it work.

Require Import VST.zlist.Zlist.
Require Import Coq.ZArith.BinInt.
Open Scope list_scope.
Open Scope Z_scope.

Goal forall A (d : Inhabitant A) i l (x : A),
  0 <= i < Zlength l ->
  sublist 0 i (upd_Znth i l x) ++
  sublist (i + 1) (Zlength (upd_Znth i l x)) (upd_Znth i l x) = 
  sublist 0 i l ++ sublist (i + 1) (Zlength l) l.
Proof. list_solve. Qed.

[andrew-appel]

In some sense this is "not a bug" because, indeed, and Inhabitant is needed. However, if list_solve could detect this situation and give a useful error message, that would be a big improvement.

[joscoh]

I agree that it is not a bug, but I thought it was strange that this goal used to be solved and now isn't.

[QinshiWang]

I tried to test it. But VST 2.9.1 is not compatible with Coq 8.15.2, which I use. So it'll need a chance that I can downgrade the Coq.