walker (Oct 10 2022 at 14:54): 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).
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.
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 ?
Pierre-Marie Pédrot (Oct 10 2022 at 15:08):There is support for that, look at the documentation of the zify tactic.
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
walker (Oct 10 2022 at 15:11):beautiful, thanks everyone!
Last updated: Oct 01 2023 at 19:01 UTC