So here is the problem, In the meta-theory of CCω, nats are used to represent three things:

debruijn levels in free variables,

debruijn indices in bound variables,

universe levels.

But all of them are called `nat`

:

```
Inductive Term : Type :=
| bvar (idx: nat) : Term
| fvar (lvl: nat): Term
| univ (l: nat): Term
.
```

What I want to to come up with three aliases for nat that have all the theories and lemmas nat inherits, but do not mix with one another.

This feels a bit impossible and might sound tricky, becuase while still want tactics like`lia`

to work, I want some other tactics that I wrote be able to differentiate between them for sake of avoiding a mess (the tactics would work anyways but I want to have cleaner proofs).

You could wrap them in distinct types, for instance

```
Variant Idx := mkIdx : nat -> Idx.
Variant Lvl := mkLvl : nat -> Lvl.
Variant Univ := mkUniv : nat -> Univ.
Inductive Term : Type :=
| bvar (idx: Idx) : Term
| fvar (lvl: Lvl): Term
| univ (l: Univ): Term
.
```

You still need to destruct all of them in proofs.

alright that is half the question, the other half is how to make this work nicely with tactics like lia (and normal arithmetic operations ?

There is support for that, look at the documentation of the zify tactic.

there: https://coq.inria.fr/distrib/current/refman/addendum/micromega.html?highlight=zify#coq:tacn.zify

beautiful, thanks everyone!

Last updated: Jun 18 2024 at 00:02 UTC