Yann Leray (Jul 22 2024 at 13:46): Yann Leray (Jul 22 2024 at 13:46):In this line, I can only read this transition as (t [↑^n]) [l] -> t [↑^n ∘ l], which would be wrong. Am I wrong or is there really an issue ?
Gaëtan Gilbert (Jul 22 2024 at 13:54):IDK what those symbols mean
Enrico Tassi (Jul 22 2024 at 14:00):Ans easy test is to fix it as you believe is right and run Coq's CI ;-)
Yann Leray (Jul 22 2024 at 14:00):They are the symbols of σ-calculus (consensual AFAICT): t[s] is term t applied to substitution s, ↑ is the shifting substitution and ∘ is substitution composition (st. t[s∘s'] = (t[s])[s'])
Gaëtan Gilbert (Jul 22 2024 at 14:02):then what's wrong with (t [↑^n]) [l] -> t [↑^n ∘ l]?
Yann Leray (Jul 22 2024 at 14:09):Sorry, it was something like ↑^n (l) following the description given in the documentation, but with this formalism it translates to l ∘ ↑^n (I think)
Yann Leray (Jul 22 2024 at 15:52):Enrico Tassi said:
Ans easy test is to fix it as you believe is right and run Coq's CI ;-)
Hugo Herbelin (Jul 22 2024 at 18:20):At first view, there seems indeed to be a bug. In the absence of el_lft in l, this is equivalent, but otherwise not.
I see el_lft in fix/cofix/let but those are used immediately (in subst_constr), so, the invariant that lfts in to_constr is made only of el_shft seems ok (a way to be sure would be to check that lfts can be replaced by just a k). So, indeed, as it is, and as far as I understand the code, this would not scale to the presence of el_lftand it is incorrect.
Yann Leray (Jul 22 2024 at 18:44):I wonder whether fast_test could return a false positive because of that
Yann Leray (Jul 24 2024 at 17:10):After thinking about it some more, I think the documented typing rule for el_shft is wrong and is actually the one needed in to_constr and fast_test : Assuming Γ ⊢ σ : Δ₁, Δ₂ and |Δ₂| = n, then Γ ⊢ el_shft n σ : Δ₁.
In other words, t[el_shft n σ] = t[↑^n][σ] and not t[σ][↑^n].
This would mean that Esubst.pop is wrong, and maybe the other uses of el_shft outside of CClosure / Conversion.
This would also mean that the typing rule of subs_shft is not aligned anymore to that of el_shft since the former is a proper weakening.
Yann Leray (Jul 24 2024 at 17:24):I tried to exploit the resulting bug in pop (to confirm that it is indeed a bug), but I can't find a way to reach the branch [that would trigger the bug].
Hugo Herbelin (Jul 24 2024 at 18:14):Yann Leray said:
After thinking about it some more, I think the documented typing rule for
el_shftis wrong and is actually the one needed into_constrandfast_test:Assuming Γ ⊢ σ : Δ₁, Δ₂ and |Δ₂| = n, then Γ ⊢ el_shft n σ : Δ₁.
It seems you're right (according to the code of reloc_rel). My bad, as it is probably me who wrote the incorrect comment. Can you make a PR that includes fixing the comment?
An argument that the bug cannot be triggered would be good.
More generally, I wonder what we could do to resolve the confusions shift/lift and shift/pop in terminology.
Also, are parts of esubst.ml already proved in metacoq?
Yann Leray (Jul 24 2024 at 18:21):Hugo Herbelin said:
An argument that the bug cannot be triggered would be good.
I put it in the same PR as the previous one, #19410
Also, are parts of
esubst.mlalready proved in metacoq?
The inductive constructions of weakenings and substitutions is not described in MetaCoq, but since full renamings and instantiations are this wouldn't be very difficult
Last updated: Oct 13 2024 at 01:02 UTC