## Stream: Coq users

### Topic: ✔ Height of derivation tree

#### Matthis Kruse (Oct 24 2023 at 13:14):

Hey,

I want to get the height of a derivation tree, but (understandably) get into trouble with universes.
My goal can be summarized with the following snippet, where `height` should "typecheck" in one form or another:

``````Inductive expr : Type :=
| Enat : nat -> expr
| Ebool : bool -> expr
| Eplus : expr -> expr -> expr
| Ecmp : expr -> expr -> expr
.
Inductive ty : Type :=
| Tnat : ty
| Tbool : ty
.
Inductive tcheck : expr -> ty -> Prop :=
| TconstN : forall (n : nat), tcheck (Enat n) Tnat
| TconstB : forall (b : bool), tcheck (Ebool b) Tbool
| Tplus : forall (e1 e2 : expr), tcheck e1 Tnat ->
tcheck e2 Tnat ->
tcheck (Eplus e1 e2) Tnat
| Tcmp : forall (e1 e2 : expr) (τ : ty), tcheck e1 τ ->
tcheck e2 τ ->
tcheck (Ecmp e1 e2) Tbool
.
Fixpoint height {e : expr} {t : ty} (c : tcheck e t) : nat :=
match c with
| TconstN _ => 0
| TconstB _ => 0
| Tplus _ _ H1 H2 => 1 + height H1 + height H2
| Tcmp _ _ _ H1 H2 => 1 + height H1 + height H2
end
.
``````

I tried wrapping into `Inductive PropWrap : Prop := PropWrapC : nat -> Prop`, but that seems to just shift the problem somewhere else and make it all entirely unergonomic.

The code works if I change `tcheck : expr -> ty -> Prop` to `tcheck : expr -> ty -> Type`. However, that's a somewhat hefty price to pay, because now I cannot easily combine this with other propositions (since it is not declared to be a proposition... :^))

How can I approach this?

#### Meven Lennon-Bertrand (Oct 24 2023 at 13:28):

This is a known issue if you put your derivations in `Prop`, and there is no easy way around, because you are hitting a rather fundamental property of propositions. Possibilities that I know of are:

1. add an extra index to you inductive type, representing the height of the derivation (ie have `tcheck : expr -> ty -> nat -> Prop`, and eg `Tplus : forall (e1 e2 : expr) (n1 n2 : nat), tcheck e1 n1 Tnat -> tcheck e2 n2 Tnat -> tcheck (Eplus e1 e2) (1 + n1 + n2) Tnat); downside: every proof needs to handle that extra index, which is tedious
2. do 1. but with a duplicate definition, show that `exists n : nat, tcheck' e t n <-> tcheck e t`, and use that to do height induction only when you need to; downside: code duplication
3. use derivations in `Type`, possibly wrapped in `PropWrap` when necessary; downside: you lose impredicativity of `Prop`, which is sometimes useful, and you now need to be careful where you use `PropWrap`
4. do 3. but you move everything you need in `Type`, so that you never need to wrap anything; downside: you might need to re-do in `Type` a lot of things that exist only in `Prop`
5. structure your trees so that you never need strong induction, but regular induction is enough (typically, by adding premises in rules to get extra induction hypotheses); downside: extra side conditions whenever you want to use a constructor (possibly attenuated by providing "smart" pseudo-constructor which reconstruct these side conditions, as soon as you are able to show they are always admissible)

#### Meven Lennon-Bertrand (Oct 24 2023 at 13:32):

For reference, option 2. is used eg. here, option 4. is used in MetaCoq (an equivalent of `PropWrap` is only used quite late to have well-behaved extraction, that removes the propositional content), there is a bit of 5. in logrel-coq, see for instance `typing_eta'` vs `typing_eta`

#### Meven Lennon-Bertrand (Oct 24 2023 at 13:33):

As far as I can tell, 5. might be best if you can do it without too much disruption, otherwise I'd go for 4, afaict option 1 and 2 incur quite a lot of boilerplate

#### Matthis Kruse (Oct 24 2023 at 13:39):

I'm - in fact - doing the 2nd option already, but hitting a different technical issue with regards to the witness provided by the equivalence `(exists n : nat, tcheck' e t n) <-> tcheck e t`. Consider the assumption `tcheck (Eplus e1 e2) Tnat`. Inverting yields `tcheck e1 Tnat` and `tcheck e2 Tnat`. Unfortunately, applying the equivalence here gives us two witnesses `n1`, `n2` such that `tcheckn n1 e1 Tnat` and `tcheckn n2 e2 Tnat`. But, since I'm interested in the height, I want `n1` and `n2` to be equal in this case, which I'd get from a function that computes the height of the derivation tree.

Looks like a rather nasty situation from a technical point of view in the sense that there appear to be no good solutions...
Thank you nonetheless! :pray:

#### Notification Bot (Oct 24 2023 at 13:53):

Matthis Kruse has marked this topic as resolved.

#### Meven Lennon-Bertrand (Oct 24 2023 at 17:36):

Why should `n1` and `n2` be equal? Or do you mean in the case of `Eplus n1 n2`?

#### Gaëtan Gilbert (Oct 24 2023 at 17:48):

Is there a reason to do `height` on `tcheck` instead of doing it on `expr`? `tcheck` is directed by `expr` in your example so the result should be the same

#### Matthis Kruse (Oct 25 2023 at 05:49):

Gaëtan Gilbert said:

Is there a reason to do `height` on `tcheck` instead of doing it on `expr`? `tcheck` is directed by `expr` in your example so the result should be the same

That's a nice observation! Unfortunately, it's an artifact of my simplified example to demonstrate my problem. The actual type system I'm modelling is not syntax-directed :^)

#### Paolo Giarrusso (Oct 25 2023 at 11:33):

But, since I'm interested in the height, I want n1 and n2 to be equal in this case, which I'd get from a function that computes the height of the derivation tree.

I agree with Meven, that seems surprising — it'd make sense for perfectly balanced trees:

``````| Tplus : forall (e1 e2 : expr) n, tcheck e1 Tnat n ->
tcheck e2 Tnat n ->
tcheck (Eplus e1 e2) Tnat n
``````

but that's not what we expect right? Looking at your code, `height` is also _not_ computing the height of the tree — that's a size.

#### Michael Soegtrop (Oct 25 2023 at 16:25):

Sorry, I accidentially merged two topics - I posted to the wrong topic and then changed the title, but apparently it changed the title for the complete stream. Sorry again for the mess.

#### Notification Bot (Oct 25 2023 at 16:26):

A message was moved here from #Coq users > Coq hangs on Qed by Michael Soegtrop.

#### Michael Soegtrop (Oct 25 2023 at 16:29):

I tried to clean it up again - but I can't set it to resolved again.

#### Notification Bot (Oct 25 2023 at 16:30):

Gaëtan Gilbert has marked this topic as resolved.

Last updated: Jun 13 2024 at 19:02 UTC