Stream: Coq users

Topic: How to change the type of a forall variable by name?

Michael Soegtrop (Apr 08 2022 at 16:49):

I am using CompCert integers. For automation control reasons I have aliases signed_int and unsigned_int for the int type. I wonder what the most elegant way to change the type of a forall variable would be. I can do:

Require Import compcert.lib.Integers.
Definition signed_int := Int.int.
Definition unsigned_int := Int.int.
Example E1:
  forall (a b : int), a=b.
  change int with signed_int at 1.
  change int with unsigned_int at 1.

but I would prefer to say something like "change the type of variable a to signed_int. Is there a good way of doing this?

Karl Palmskog (Apr 08 2022 at 17:27):

shallow answer, but might not LibHyps support something like this?

Gaëtan Gilbert (Apr 08 2022 at 18:02):

intro a;change bla in a;revert a?
without introing you would have to use the binder name which is not recommended

Gaëtan Gilbert (Apr 08 2022 at 18:04):

some kind of occurence language to say "! in forall (x : !) y, _" (maybe even "! matching some pattern") would be nice, no idea if such a thing exists somewhere

Michael Soegtrop (Apr 09 2022 at 08:07):

The downside of intro and revert is that if I have 10 binders, possibly with hypothesis in between, it takes quite a bit of book keeping, and extracting binder names and getting them back is not entirely trivial in Ltac2 (I remember a recent discussion on the topic between Guillaume and PMP). But for sure it would be possible.

@Karl Palmskog : thanks for the pointer to LibHyps - I don't think it solves this problem, but it nicely solves another problem I had.

Kenji Maillard (Apr 09 2022 at 08:08):

You can at least do the following with ssreflect's set pattern selection:

From Coq Require Import ssreflect.
Require Import compcert.lib.Integers.
Definition signed_int := Int.int.
Definition unsigned_int := Int.int.
Example E1:
  forall (a b : int), a=b.
  set X := (int as x in (forall a : x, _)).
  change X with signed_int; clear X.

Pierre Courtieu (Apr 10 2022 at 18:48):

It is maybe easier to do this after introducing the variable.

intros a b.
change int with signed_int in a.
change int with unsigned_int in b.

You can write a dedicated tactic

Ltac ch_type H T :=
  let tH := type of H in
  change tH with T in H.

and you can even have a tactic notation for that:

Tactic Notation "retype" hyp(H) "into" constr(T) := (ch_type H T) .

Example E1: forall a b : Z, a = b.
Proof.
  intros a b.
  retype a into signed_int.
  retype b into unsigned_int.

@Karl Palmskog What do you have in mind for LibHyps? Since a and b need to be treated differently I don't see any systematic tactic to apply on each new hyp.

Karl Palmskog (Apr 10 2022 at 19:14):

well, my thinking was that since LibHyps has a bunch of stuff regarding hypotheses, it may have something along those lines (I wasn't sure, hence "shallow answer"). Maybe the retype .. into .. tactic would be a reasonable addition to LibHyps?

Gaëtan Gilbert (Apr 10 2022 at 20:26):

why not Tactic Notation "retype" hyp(H) "into" constr(T) := (change T in H) . or just use it directly?

Pierre Courtieu (Apr 11 2022 at 06:00):

@Gaëtan Gilbert Good point I always forget that change has a variant without with.
@Karl Palmskog I will think about it, thanks.

Michael Soegtrop (Apr 11 2022 at 09:10):

Pierre Courtieu said:

It is maybe easier to do this after introducing the variable.

The issue is that I have many variables and hypothesis and for proof automation I need it all generalized, so this is requires quite a bit of book keeping to introduce everything, change it, and put it back.

Michael Soegtrop (Apr 11 2022 at 09:12):

Kenji Maillard said:

You can at least do the following with ssreflect's set pattern selection:

This does not seem to work - if I replace forall a with forall b, it stiil replaces the type in the first forall, not the second (and renames the variables to b and b0 doing so).

Kenji Maillard (Apr 11 2022 at 09:16):

The name of the bound variable is irrelevant (as it should be), but I seem to remember that you can also use occurence selections with ssreflects' patterns. Anyway, I would probably only use that in the middle of a script rather than inside a tactic.

Michael Soegtrop (Apr 11 2022 at 10:08):

With occurrence selections I can also write what I originally posted:

change int with signed_int at 1.

Michael Soegtrop (Apr 11 2022 at 10:08):

I guess I should just be more consistent about how I name my types, then I won't have the problem that I need to change them later.

Last updated: Oct 13 2024 at 01:02 UTC