Stream: Elpi users & devs

Topic: Goal manipulation

view this post on Zulip Enzo Crance (Feb 15 2021 at 11:04):

Good morning. I am looking for a way to delete a goal of type T and replacing it with 2 new goals, one having another type U and the other one having the type of the implication needed for the change to be accepted by Coq, that is, U -> T. My current code looks like this:

solve [] [goal Ctx Proof GoalTy _] [NewGoal, Impl] :- std.do! [
    my-goal-generator GoalTy NewGoalTy,
    NewGoal = goal Ctx NGProof NewGoalTy _,
    Impl = goal Ctx ImplProof {{ lp:NewGoalTy -> lp:GoalTy }} _,
    Proof = {{ lp:ImplProof lp:NGProof }}
  ].

Elpi does not crash so I think the typing is ok, but the two generated goal types displayed are Type and Type, so I did something wrong but cannot find what. Does someone have an idea? Thank you in advance for the help!

view this post on Zulip Enrico Tassi (Feb 15 2021 at 13:59):

What you wrote is sensible, but I'm afraid it does not work for "technical" reasons. It think you may use refine, but I have to try it out myself I'm afraid.

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2021 at 05:39):

Here is an example with the use of refine. (The elpi suff tactic takes a proposition as an argument instead of generating it internally.) Just instantiating Proof with a term with holes also works for me.

Elpi Tactic suff.
Elpi Accumulate lp:{{
solve [trm Type] [G] GS :-
    refine {{ (_ : _ -> _) (_ : lp:Type) }} G GS.
}}.
Elpi Typecheck.

Goal False.
elpi suff (True).

Last updated: Oct 13 2024 at 01:02 UTC