Luko van der Maas (Nov 07 2023 at 13:24): Luko van der Maas (Nov 07 2023 at 13:24):I am getting some unification failures in the tracer for which I don't know the reason and I was wondering if there is some way to find out why it failed. The failure is:
unify [X514, X515] with
[app [global (const «is_list_pre»), c0],
app [global (const «is_list_pre»), c1]]
in std.drop in the following piece of code:
pred relation-on i:term, o:term, o:term.
relation-on {{ envs_entails _ lp:{{ (app AS) }} }} L R :- !,
std.take-last 2 AS [L, R].
Which is called as follows:
relation-on
(app
[global (const «envs_entails»),
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 «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 «IAnon»), global (indc «xH»)],
app
[global (const «iPointwise_relation»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
global (indt «val»),
prod `_` (app [global (indt «list»), global (indt «val»)]) c2 \
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[global (const «iPointwise_relation»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app [global (indt «list»), global (indt «val»)],
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[primitive (proj iris.bi.interface.bi_wand 12),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
c0, c1]],
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 «xO»), global (indc «xH»)]],
app
[global (const «iPointwise_relation»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
global (indt «val»),
prod `_` (app [global (indt «list»), global (indt «val»)]) c2 \
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[global (const «iPointwise_relation»),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]],
app [global (indt «list»), global (indt «val»)],
app
[primitive (proj iris.bi.interface.bi_car 0),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]],
app
[primitive (proj iris.bi.interface.bi_wand 12),
app
[global (const «uPredI»),
app [global (const «iResUR»), global (const «Σ»)]]]],
app [global (const «is_list_pre»), c0],
app [global (const «is_list_pre»), c1]]]) X514 X515
X514 is bound to L and X515 is bound to R
Luko van der Maas (Nov 07 2023 at 13:26):std.take-last has the following definition:
pred take-last i:int, i:list A, o:list A.
take-last N L R :-
length L M,
D is M - N,
drop D L R.
Let me explain the syntax here:
unify [X514, X515] with
[app [global (const «is_list_pre»), c0],
app [global (const «is_list_pre»), c1]]
Here X514 is a unification variable "al level 0", it has no bound variables in scope.
At the same time c0 and c1 are the first and second bound variables erspectively.
Enrico Tassi (Nov 07 2023 at 13:28):Take this example:
main :-
pi x\
not (A = x),
B x = x,
sigma C\
C = x.
Here x is locally bound (quantified) by pi, and A and B are quantified before it (outside the clause).
So they don't see x. Since I pass x to B (hence B is a function), it can use its input to produce x.
C is quantified (allocated) when x is in scope, so it see it. And it is printed by elpi as X3^1 since it sees c0 (the internal name for x).
Enrico Tassi (Nov 07 2023 at 13:32):I need more context to know why your X514 does not see c0 nor c1.
Enrico Tassi (Nov 07 2023 at 13:33):I kind of explain this here: https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html#allocation-of-variables
Luko van der Maas (Nov 07 2023 at 13:36):Now it makes sense. I am trying to take a term out of an opened goal and of course that won't work since there are bound variables in the term, bound by the opened goal. I could try to set the terms as arguments and pass them around like that. Would that be the best way?
Luko van der Maas (Nov 07 2023 at 13:39):So this is the context it is called in:
pred do-step i:sealed-goal, o:list sealed-goal.
do-step G GL :-
open (do-step.conn C LF RF) G _,
do-step.aux C LF RF G GL.
pred do-step.conn o:term, o:term, o:term, i:goal, o:list sealed-goal.
do-step.conn R LF RF (goal _Ctx _Trigger Type _Proof _Args as G) [seal G] :-
top-relation Type R, !,
relation-on Type LF RF.
and do-step.aux matches on LF and RF to find out what step it should do
Enrico Tassi (Nov 07 2023 at 13:49):The answer is going to be a bit verbose.
Because of binders, you can't organize your code as you may be used to do in functional languages.
And "tactics" do not help much either. I wrote the usual combinators but as you just found out you can't pass data from one tactic to the other one that easily. Setting arguments for the next tactic is the best you can do (and the arguments are inside the sealed goal).
So, IMO, you have to open once at the beginning and then work under the same context.
The problem does not go away, but at least it does not pop up for the variables in the proof context.
The problem is there in general, you can not use HO functions as you do in functional programming like find to extract an element of a list, since you can't extrude it out of its context. I know a few ways out:
find, but you write your recursion and when you find the element you call the code that does something with it (my preferred)find predicate takes a continuation and calls it on the found element (in its context)nabla and seal for goals, and you close up the term in order to extract it from its context (but then you may need to open it up again and again).I usually prefer the first solution, in general the code you save by reusing simple HO iterators (like find, map, ..) is not much.
But if you give me more details I can give a more precise suggestion.
Luko van der Maas (Nov 07 2023 at 13:56):The full context can be found here: inductive.v
But to summarize:
My do-step.aux looks first at the relation R and then at the the LF and RF and depending on that we call often do a refine and then deal with the resulting goals by calling LTac wrappers. Thus that looks like
do-step.aux {{ @iPersistent_relation }} _ _ G GL :- !,
coq.say "□>",
go_iModIntro G GL.
which calls:
type go_iModIntro tactic.
go_iModIntro G GL :-
open go_iStartProof G [GoalStarted],
@no-tc! => open (refine {{ tac_modal_intro _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ }}) GoalStarted [G1, G2, G3, G4, G5, G6],
open tc_solve G1 [],
open tc_solve G2 [],
open tc_solve G3 [],
open pm_reduce G4 [G4'],
open tc_solve G4' [],
open (coq.ltac.call "iSolveSideCondition" []) G5 [],
open pm_prettify G6 GL.
Earlier I ran into the issue that if I am already in an opend goal it is very hard to call an ltac wrapper after a refine because you open a goal while a goal is already opened. Thus I switched to the msolve way of doing things and only opening goals when I actually work on them.
Luko van der Maas (Nov 07 2023 at 13:59):This specific step would be fine as don't look at bound variables, but the following two steps are harder:
do-step.aux R (app FS) _ G GL :-
std.exists { std.iota {std.length FS} } (n\ std.take n FS F),
coq.say "Apply relation" R "with" {coq.term->string (app F)},
go_iApplyProper R (app F) G GL.
do-step.aux _ (app [global (const F) | ]) _ G GL :-
coq.say "Unfolding" F,
open (unfold-gref (const F)) G GL.
The first one tries to apply a proper for a function in a relation with an increasing amount of its arguments applied to find if there is a proper definition for that function with the relation R. The second if that fails tries to unfold that the F if it is a definition.
Enrico Tassi (Nov 07 2023 at 14:05):From what I understand, it is more natural to call do-step.aux inside do-step.conn
Enrico Tassi (Nov 07 2023 at 14:05):but I don't know what your problem was initially.
Enrico Tassi (Nov 07 2023 at 14:06):I mean, your problem in calling ltac after having opened a goal.
Luko van der Maas (Nov 07 2023 at 14:07):it was this issue
Enrico Tassi (Nov 07 2023 at 14:29):(deleted)
Luko van der Maas (Nov 07 2023 at 14:31):(deleted)
Luko van der Maas (Nov 07 2023 at 14:31):(deleted)
Luko van der Maas (Nov 07 2023 at 14:32):(deleted)
Last updated: Oct 13 2024 at 01:02 UTC