Enzo Crance (Feb 12 2021 at 13:11): Enzo Crance (Feb 12 2021 at 13:11):Hello. Let me ask my question(s) of the day... Is there a way to give a fresh name f to a term x and add it to the proof context, like Ltac's pose (f := x) would do, but with a fresh f name? Is it possible to declare a new variable without giving its definition? Like having a new x : nat in the context, not knowing anything about it?
I think the only way I have in mind is to generate a goal forall x, forall f, f = blah -> G with blah being the definition of f and G the old goal, then calling Ltac's intros to put these forall headers in the context. This looks like a workaround though, I wonder if something better exists.
Enrico Tassi (Feb 12 2021 at 13:28):There is not much "ltac" written in elpi, but you can find some code in examples/ and the app/eltac/ POC. Both tactics boil down to a call to 'refine' with a letin or a beta redex. About the "freshness" of the names, I would leave the problem on the side and use new_int as a start.
Kazuhiko Sakaguchi (Feb 18 2021 at 08:09):I managed to produce a small example, but this does not work as I expected in my use case... (Probably my bad.)
Elpi Tactic pose.
Elpi Accumulate lp:{{
solve [trm T] [G] GS :-
refine {{ let _ := lp:T in _ }} G GS.
}}.
Elpi Typecheck.
Goal False.
elpi pose (I).
Elpi Tactic pose.
Elpi Accumulate lp:{{
solve [str ID, trm T] [G] GS :-
coq.id->name ID N,
refine (let N _ T _) G GS.
}}.
Elpi Typecheck.
Goal False.
elpi pose "x" (I).
elpi pose "x" (I).
Here N is a "hint", and elpi will not make the variable clash, but rather introduce a funny name instead, which you can't rely upon.
Enrico Tassi (Feb 18 2021 at 10:02):if you want you variable to be fresh and with a "predictable" name, I suggest you pick x1 ... xN and you call pred new_int o:int which grants a fresh integer any time you call it.
Enrico Tassi (Feb 18 2021 at 10:03):FTR, the {{ quotation }} do not let you specify an elpi variable for a name (only for terms). This is why I used the "raw" elpi term for the let in.
Kazuhiko Sakaguchi (Feb 18 2021 at 13:24):By "does not work as I expected", I meant that it does not introduce any assumption. Since it refines the goal with a bigger proof term, I'm having a hard time to identify the source of the issue.
Enrico Tassi (Feb 18 2021 at 16:10):It works here. Which version are you on?
Enrico Tassi (Feb 18 2021 at 17:29):pred assume-constraints i:(list term), i:term, o:term.
assume-constraints [] P P :- !.
assume-constraints (A :: Atoms) P Q :- !,
zify-atom A CA,
assume-constraints Atoms {{ let _ := lp:CA in lp:P }} Q.
The problem is that P does not see _.
You could write {{ let x := lp:CA in lp:{{ P x }} }} to put x in the scope of P (or the shorter and equivalent lp:(P x)) but here P has the wrong elpi type, it should be term -> term for P x to typecheck.
You can also say that P is a term of functional type in Coq, and write {{ let x := lp:CA in lp:P x }} (this time the application is a Coq one, an app node) but this proof term implements a cut anyway, so you don't see a let-in but a forall.
There is another little problem, you wrap the lets around the wrong hole. Here some code which "works". I don't what you really want to do, so I hope I did put you in some direction.
pred assume-constraints i:(list term), i:term, o:term.
assume-constraints [] P P :- !.
assume-constraints (A :: Atoms) P Q :- !,
zify-atom A CA,
assume-constraints Atoms {{ let x := lp:CA in lp:P x }} Q.
% TODO: apply Z-ification for hypotheses.
solve _ [(goal Ctx _ Ty _ as G)] GS :-
Ctx => std.do! [
zify-prop Ty _ _ Ty1->Ty_ Atoms,
close Atoms,
% FIXME: [ZifyProof] contains let-ins for constraints, but they do not
% appear in the goal.
assume-constraints Atoms P_ ZifyMissingProof,
ZifyProof = Ty1->Ty_ ZifyMissingProof,
std.assert-ok! (coq.typecheck ZifyProof _) "bad proof",
coq.say {coq.term->string ZifyProof},
refine ZifyProof G GS
].
the proof term you were generating was (let H in ... (Ty1->Ty_ Kont)), IMO you want H to be visible (hence passed to) Kont.
Enrico Tassi (Feb 18 2021 at 17:52):So this is the new term (Ty1->Ty_ (let H : TH := .. in Kont H)) and the new goal is Kont : TH -> Z.of_nat .. = Z.of_nat ...
Enrico Tassi (Feb 18 2021 at 17:57):Bottom line, if you type check (?e 3 : G) you infer for ?e : nat -> G, the same if you infer (let x := 3 in ?e 3 : G). If you want a let in the type of ?e you have to write it by yourself, since no type inference rule puts a let in the type. This makes a let instead of a forall in the resulting goal: assume-constraints Atoms {{ (lp:P : let x := lp:CA in _) }} Q.
Kazuhiko Sakaguchi (Feb 19 2021 at 00:38):I see. Thank you so much!
Kazuhiko Sakaguchi (Feb 19 2021 at 02:44):FTR, I managed to turn the function application P x into Elpi one, so that constraints appear as assumptions after refine. Here is my solution:
% [letins [T1, ..., Tn] U] states that U = {{ let x1 := T1 in ... let xn := Tn in _ }}.
pred letins i:(list term), o:term.
letins [] U :- !.
letins (T :: TS) (let _ _ T U) :- !, pi x\ letins TS (U x).
But, if I want to touch the innermost placeholder afterward, I don't see how to do that. (For now, it is OK for me.)
Enrico Tassi (Feb 19 2021 at 07:17):What do you mean by touch? You can match an evar if the argument is in input mode using the 'uvar' keyword, see the code of copy for example, or use the 'var' built-in.
Enrico Tassi (Feb 19 2021 at 07:17):I don't know about automatically introduction. Maybe it is good in your case, but is not very SSR style....
Last updated: Oct 13 2024 at 01:02 UTC