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?

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:

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

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

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

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`

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

Thanks for your reply!

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:

Matthis Kruse has marked this topic as resolved.

Why should `n1`

and `n2`

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

?

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

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 :^)

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.

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.

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

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

Gaëtan Gilbert has marked this topic as resolved.

Last updated: Jun 13 2024 at 19:02 UTC