Luko van der Maas (Nov 28 2023 at 15:13): Luko van der Maas (Nov 28 2023 at 15:13):I am creating a proof in elpi and the elaborator seems to be acting weird. During a proof I am using the following code to apply a lemma:
if-debug (coq.say "intui1" Proof),
@no-tc! => coq.elaborate-skeleton {{ tac_wand_intro_intuitionistic _ lp:T _ _ _ _ _ _ _ _ }} Type Proof ok,
if-debug (coq.say "intui2" Proof),
Proof = {{ tac_wand_intro_intuitionistic _ lp:T _ _ _ _ lp:FromWand lp:IP lp:TCOR lp:IntProof }},
if-debug (coq.say "intui3" IntProof),
Proof is the variable I have to assign the proof to and IntProof is what I will continue the proof with. This results int the following output
intui1 X41 c2 c3 c4
intui2
app
[global (const «tac_wand_intro_intuitionistic»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (indc «Envs»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (indc «Enil»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
app
[global (indc «Esnoc»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[global (indc «Enil»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
app
[global (indc «INamed»),
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)],
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «true»), global (indc «true»),
global (indc «false»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)], global (indc «EmptyString»)]]],
app
[global (const «is_list_pre»), global (const «is_list»), c2, c3]],
global (indc «xH»)],
app
[global (indc «INamed»),
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)],
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «true»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)], global (indc «EmptyString»)]]],
X42 c2 c3 c2 c3 c4, X43 c2 c3 c2 c3 c4, X44 c2 c3 c2 c3 c4,
app
[global (const «bi_wand»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (const «bi_intuitionistically»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (const «bi_forall»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
global (indt «val»),
fun `_` (global (indt «val»)) c5 \
app
[global (const «bi_forall»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app [global (indt «list»), global (indt «val»)],
fun `_` (app [global (indt «list»), global (indt «val»)]) c6 \
app
[global (const «bi_wand»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app [global (const «is_list_pre»), c4, c5, c6],
app [c4, c5, c6]]]]], app [c4, c2, c3]], X45 c2 c3 c2 c3 c4,
X46 c2 c3 c2 c3 c4, X47 c2 c3 c2 c3 c4, X48 c2 c3 c2 c3 c4]
intui3 X48 c2 c3 c2 c3 c4
When I then continue with the proof I end up in a Unification problem outside the pattern fragment in a later step of the proof, I think because of the double c2 c3 applied to X48.
Luko van der Maas (Nov 28 2023 at 15:14):How can I solve this?
Luko van der Maas (Nov 28 2023 at 15:24):It only seems to happen when I have to apply a piece of LTac code and open the resulting goal and continue my proof like above
Luko van der Maas (Nov 28 2023 at 15:27):It seems to want to add c0 and c1 to X48 but for some reason adds them as c2 and c3. When I use the same piece of code for another lemma with less context variables I get the following output:
intui1 X35 c1 c2
intui2
app
[global (const «tac_wand_intro_intuitionistic»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (indc «Envs»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (indc «Enil»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
app
[global (indc «Esnoc»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[global (indc «Enil»),
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
app
[global (indc «INamed»),
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)],
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «true»), global (indc «true»),
global (indc «false»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)], global (indc «EmptyString»)]]],
app [global (const «is_l_pre»), global (const «is_l»), c1]],
global (indc «xH»)],
app
[global (indc «INamed»),
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «false»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)],
app
[global (indc «String»),
app
[global (indc «Ascii»), global (indc «true»),
global (indc «false»), global (indc «false»),
global (indc «true»), global (indc «false»),
global (indc «false»), global (indc «true»),
global (indc «false»)], global (indc «EmptyString»)]]],
X36 c1 c1 c2, X37 c1 c1 c2, X38 c1 c1 c2,
app
[global (const «bi_wand»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (const «bi_intuitionistically»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app
[global (const «bi_forall»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
global (indt «val»),
fun `_` (global (indt «val»)) c3 \
app
[global (const «bi_wand»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app [global (const «is_l_pre»), c2, c3], app [c2, c3]]]],
app [c2, c1]], X39 c1 c1 c2, X40 c1 c1 c2, X41 c1 c1 c2, X42 c1 c1 c2]
intui3 X42 c1 c1 c2
This one only has one fewer context variable and now it only replaces c0 with c1
Enrico Tassi (Nov 29 2023 at 08:19):Yes, that is the problem, but without looking at your code I can't really help, and I'm quite busy. Can we make a visio, like on monday?
Luko van der Maas (Nov 30 2023 at 09:47):Yes sounds good
Last updated: Oct 13 2024 at 01:02 UTC