LPCIC
Fix #386
From the log:
2022-09-06T16:46:41.1234079Z - File "./tests/test_invert.v", line 19, characters 0-25:
2022-09-06T16:46:41.1234435Z - Error:
2022-09-06T16:46:41.1234834Z - 1st non uniform parameter, named idx0, not found in constructor nilR_inv
2022-09-06T16:46:41.1235163Z -
So it is not that simple. Maybe lift 1 is simplistic, maybe it is a "lift from n_uniform_params"... but I had no time to dig into this
I took some time to investigate. I think I found the bug. Short: a lift is needed, but only for indices mentioning uniform parameters.
Consider the following inductive type:
Inductive t (A : Type) (l : list A) (e : l = l) : Type :=
| K : t A (@nil A) (@eq_refl A l) -> t A l e.
Here is its Elpi representation (simplified):
parameter {{ Type }} A\
inductive
(parameter {{ list A }} l\ parameter {{ l = l }} e\ arity {{ Type }})
t\ [
constructor K
(parameter {{ list A }} l\ parameter {{ l = l }} e\
arity {{ t A (@nil A) (@eq_refl A l) -> t A l e }}
]
If we give this indt-decl value to coq.env.add-indt, before trying to add the inductive to Coq, it will call check_consistency_and_drop_nuparams to check that the non-uniform parameters found in the arity of the inductive and in the arity of each constructor are equal, but the check is performed up to consistency of the de Bruijn indices, because the arities of the constructors have an additional binder for the inductive.
IIUC, the previous solution to equate the indices was to shift by 1 all the indices in the arity of the inductive. But let's see the DB declaration:
parameter {{ Type }} λ.
inductive
(parameter {{ list #1 }} λ. parameter {{ #1 = #1 }} λ. arity {{ Type }})
λ. [
constructor K
(parameter {{ list #2 }} λ. parameter {{ #1 = #1 }} λ.
arity {{ ... }}
]
The two lists to compare are the following:
[ {{ list #1 }}, {{ #1 = #1 }} ]
[ {{ list #2 }}, {{ #1 = #1 }} ]
As you can see, lifting all the indices in the first list makes the equality fail. IMO what we should do is lift only the indices that mention a value beyond the binder for the inductive, because they are the only ones losing their meaning if we add an additional binder under them. The ones mentioning something "closer" are unaffected, so already equal in both compared arities.
If you had a pointer to a helper function able to do that selective lift, it would be great. Otherwise I can try to write it.
maybe https://coq.github.io/doc/v8.10/api/coq/Vars/index.html#val-liftn , otherwise you will have craft a subst, same file.
Both test_invert.v and my code seem to work with the selective lift update.