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?

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

`intro a;change bla in a;revert a`

?

without introing you would have to use the binder name which is not recommended

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

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.

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.
```

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.

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?

why not `Tactic Notation "retype" hyp(H) "into" constr(T) := (change T in H) .`

or just use it directly?

@Gaëtan Gilbert Good point I always forget that `change`

has a variant without `with`

.

@Karl Palmskog I will think about it, thanks.

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.

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).

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.

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

```
change int with signed_int at 1.
```

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: Jun 25 2024 at 19:01 UTC