Stream: Coq users

Topic: Multiple aliases for nat that does not mix


view this post on Zulip walker (Oct 10 2022 at 14:54):

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

view this post on Zulip Kenji Maillard (Oct 10 2022 at 14:58):

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.

view this post on Zulip walker (Oct 10 2022 at 15:07):

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

view this post on Zulip Pierre-Marie Pédrot (Oct 10 2022 at 15:08):

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

view this post on Zulip Pierre-Marie Pédrot (Oct 10 2022 at 15:09):

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

view this post on Zulip walker (Oct 10 2022 at 15:11):

beautiful, thanks everyone!


Last updated: Mar 28 2024 at 15:01 UTC