Problems with dependent sums

Question

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.

Answer 1

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