# Problems with dependent sums

Very simple trees (I trew away everything unnecessary)

Inductive Tree : Set :=
| pair : Tree -> Tree -> Tree.

Fixpoint height (M : Tree) : nat :=
match M with
| pair M N => match ((height N) - (height M)) with
| 0 => height M
| _ => height N
end
end.


Let A n be the type of all trees of height n and B n be the type of all trees of height at most n. Then B n = A 0 + A 1 + ... + A n and any tree of height n has form (pair M N) where (height M = n & height N <= n) or (height M < n & height N = n)

Inductive B : forall (n:nat), Set :=
| a : forall (n:nat), A n -> B n
| b : forall (n:nat), B n -> B (S n)
with A : forall (n:nat), Set :=
| pair1 : forall (n:nat), A n -> B n -> A n
| pair2 : forall (n:nat), B n -> A (S n) -> A (S n).


Trying to find a tallest subtree (disappointment)

Fixpoint subtree (M : Tree) : A (height M) :=
match M with
| pair M N => match ((height N) - (height M)) with
| 0 => subtree M
| _ => subtree N
end
end.


Really I want to write functions

foo (n:nat) (M : A n) : Tree
bar (M : Tree) : A (height M)


and to prove they are mutually inverse

forall (n:nat) (M : A n), height (foo n M) = n.
forall (n:nat) (M : A n), bar (foo n M) = M.
forall (M : Tree), foo (height M) (bar M) = M.


I can define foo and prove the first theorem.

• Your Tree type is empty. Did you forget to add a leaf constructor? Commented Jun 11 at 10:52
• @NaïmFavier I know it is empty, I removed leaf constructors for simplicity (the problems are the same with leaf constructors) Commented Jun 11 at 11:06

You can use match with a return clause to specify the part of the return type that you are matching on, so that the type can be simplified in each branch, knowing what the result of the match is:

Fixpoint subtree (M : Tree) : A (height M) :=
match M with
| pair M N =>
match height N - height M as u return
A (match u with 0 => height M | S _ => height N end) with
| O => subtree M
| S _ => subtree N
end
end.


match with return clauses comes out of the box as part of the Coq language, but it is a poor way of programming with dependent types. It's highly recommended to use Equations instead. Here's your definition in Equations:

From Equations Require Import Equations.

(* ... *)

Equations subtree (M : Tree) : A (height M) :=
| (pair M N) with (height N - height M) => {
| 0 => subtree M
| S _ => subtree N }.


BTW Note that the last one of the properties you expected is broken, because subtree throws away part of the tree when M = pair M1 M2:

forall (M : Tree), foo (height M) (subtree M) = M. (* wrong *)


(where foo is a certain function forall n, A n -> Tree).