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!

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.

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: Jun 22 2024 at 23:01 UTC