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

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:

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: Oct 13 2024 at 01:02 UTC