Stream: Coq users

Topic: Change, but with evars

Meven Lennon-Bertrand (Nov 25 2022 at 11:15):

Is there a way to perform the same operation as change (ie, replace the goal with a convertible one given by the user), but where the user-given goal contains evars? Here is an example usecase:

``````Variables (P0 P1 P2 Q : bool -> Type).

Definition f (n : nat) (m : bool) :=
match n with
| 0 => P0 m
| 1 => P1 m
| S (S _) => P2 m
end.

Hypothesis foo : forall (n : nat) (b : bool), 1 <= n -> f n b -> Q b.

Variable complicated_boolean_much_too_long_to_copy : bool.

Goal P1 complicated_boolean_much_too_long_to_copy -> Q complicated_boolean_much_too_long_to_copy.
intros HP.
Fail eapply foo in HP.
(*cannot directly apply foo: unification is not smart enough to find out the first argument should be 1 *)
Fail change (f 1 _) in HP.
(* I cannot use change with a hole, letting it be filled by unification *)
change (f 1 complicated_boolean_much_too_long_to_copy) in HP.
(* If I copy the boolean, then change works… *)
eapply foo in HP.
(* Of course now eapply finds the right unification *)
Undo 2.
apply (foo 1) in HP.
(* in the case of apply though, unification is smart enough to unify f 1 _ and P1 complicated_boolean_much_too_long_to_copy *)
Abort.
``````

I hope the general idea is clear: I want to be able to give a pattern with the "interesting" changes to perform to `change`, and let unification infer the holes.

Gaëtan Gilbert (Nov 25 2022 at 11:20):

`eassert (HP' : f 1 _) by exact HP.` ?

Gaëtan Gilbert (Nov 25 2022 at 11:22):

(AFAIK change uses conversion not unification so using `change` specifically for this is impossible)

Meven Lennon-Bertrand (Nov 25 2022 at 11:23):

Gaëtan Gilbert said:

(AFAIK change uses conversion not unification so using `change` specifically for this is impossible)

This is what I figured… Is there any reason for this? Or could it in principle be possible to either change `change` or implement `echange` if we want to keep `change` intact?

Meven Lennon-Bertrand (Nov 25 2022 at 11:24):

Note that AFAICT `fold` suffers the same defect (here using `fold 1 _ in HP.` fails just like change, while `fold (f 1 complicated_boolean_much_too_long_to_copy) in HP` does succeed).

Meven Lennon-Bertrand (Nov 25 2022 at 11:27):

And maybe I should give my actual use case, which is closer to the following:

``````Variables (P0 P1 P2 Q : bool -> Type).

Definition f (n : nat) (b : bool) :=
match n with
| 0 => P0 b
| 1 => P1 b
| S (S _) => P2 b
end.

Notation "n >> b" := (f n b) (at level 50).

Hypothesis foo : forall b : bool, P1 b -> Q b.

Variable complicated_boolean_much_too_long_to_copy : bool.

Goal Q complicated_boolean_much_too_long_to_copy.
apply foo.
Fail change (1 >> _).
Fail fold (1 >> _).
change (1 >> complicated_boolean_much_too_long_to_copy).
Undo.
fold (1 >> complicated_boolean_much_too_long_to_copy).
``````

But the issue is the same, really: I just wanna tell Coq it can use the notation, without filling in the gaps.

Gaëtan Gilbert (Nov 25 2022 at 11:29):

no idea what fold does, most of the time when I try it, it does nothing

Gaëtan Gilbert (Nov 25 2022 at 11:29):

try `refine (_ : 1 >> _).`

Meven Lennon-Bertrand (Nov 25 2022 at 11:34):

Looks like a reasonable enough compromise :) Still, I think there might be a reasonable feature missing there…

Pierre-Marie Pédrot (Nov 25 2022 at 12:10):

For atomic behaviour purposes, I don't think you want change to perform unification.

Meven Lennon-Bertrand (Nov 25 2022 at 12:11):

Fair enough, but maybe some `echange`?

Pierre-Marie Pédrot (Nov 25 2022 at 12:15):

change is about conversion, period. Why don't you want to use refine with a cast?

Janno (Nov 25 2022 at 12:18):

I've run into this limitation countless times. It is always easy to fix but even the simplest fix performed a few hundred times will become annoying. I would love `echange` or a similar tactic that does the right thing.

Meven Lennon-Bertrand (Nov 25 2022 at 12:20):

Because change has more features than just `refine`: you have occurrence selection, can convert only a subterm, do it in hypothesis… I could easily use the `refine`-based solution for the simpler case, but I'm not expert enough in Ltac to easily implement the more expressive version

Pierre Courtieu (Nov 27 2022 at 10:49):

I think you can more or less define echange like this:

``````Tactic Notation "echange" open_constr(trm) "in" hyp(h) :=
let h' := fresh h in
rename h into h';
eassert trm as h by (exact h');clear h'.

Tactic Notation "echange" open_constr(trm) :=
refine (_: trm).
``````

Pierre-Marie Pédrot said:

change is about conversion, period. Why don't you want to use refine with a cast?

I don't see your point: `echange` would be a different tactic than `change`.

Pierre Courtieu (Nov 27 2022 at 10:51):

Subterm is probably easy to add. Occurrence selection I don't know.

Paolo Giarrusso (Nov 27 2022 at 19:27):

that `echange ... in h` won't work if `h` is mentioned by other assumptions, I assume? Not sure if `change` does, but it could be done by reverting `h` (and anything depending on it), using `change` in the goal, then reintroducing everything as needed...

Pierre Courtieu (Nov 29 2022 at 17:46):

True. I didn't thought about that. This should do it:

``````Tactic Notation "echange" open_constr(trm) "in" hyp(h) :=
let h' := fresh h in
eassert trm as h' by (exact h);
let t := type of h in
let t' := type of h' in
change t with t' in h;
clear h'.
``````

Pierre Courtieu (Nov 29 2022 at 17:47):

oops sorry let me edit that first.
There it is.

Pierre Courtieu (Nov 29 2022 at 17:49):

This way we ensure it behaves like exactly like change.

Gaëtan Gilbert (Nov 29 2022 at 17:55):

instead of doing a dummy assert for the unification, how about

``````Tactic Notation "echange" open_constr(trm) "in" hyp(h) :=
let t := type of h in
unify t trm;
change trm in h.
``````

Pierre Courtieu (Nov 29 2022 at 20:01):

great! I didn't know about unify.

Last updated: Jun 14 2024 at 19:02 UTC