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: Oct 04 2023 at 20:01 UTC