Stream: Coq users

Topic: Change, but with evars


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 25 2022 at 11:20):

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

view this post on Zulip Gaëtan Gilbert (Nov 25 2022 at 11:22):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 25 2022 at 11:29):

try refine (_ : 1 >> _).

view this post on Zulip 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…

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 12:10):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 25 2022 at 12:11):

Fair enough, but maybe some echange?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre Courtieu (Nov 27 2022 at 10:51):

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

view this post on Zulip 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...

view this post on Zulip 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'.

view this post on Zulip Pierre Courtieu (Nov 29 2022 at 17:47):

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

view this post on Zulip Pierre Courtieu (Nov 29 2022 at 17:49):

This way we ensure it behaves like exactly like change.

view this post on Zulip 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.

view this post on Zulip Pierre Courtieu (Nov 29 2022 at 20:01):

great! I didn't know about unify.


Last updated: Jun 14 2024 at 19:02 UTC