The Coq mailing list

[t x <txrev319 AT gmail.com>]

I've recently been porting http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ to scheme.

Quoting the section on type inference:

** [equal ctx e1 e2] determines whether normalized [e1] and [e2] are equal up to renaming

    of bound variables. *)

let equal ctx e1 e2 =

  let rec equal e1 e2 =

    match e1, e2 with

      | Var x1, Var x2 -> x1 = x2

      | App (e11, e12), App (e21, e22) -> equal e11 e21 && equal e12 e22

      | Universe k1, Universe k2 -> k1 = k2

      | Pi a1, Pi a2 -> equal_abstraction a1 a2

      | Lambda a1, Lambda a2 -> equal_abstraction a1 a2

      | (Var _ | App _ | Universe _ | Pi _ | Lambda _), _ -> false

  and equal_abstraction (x, t1, e1) (y, t2, e2) =

    equal t1 t2 && (equal e1 (subst [(y, Var x)] e2))

  in

    equal (normalize ctx e1) (normalize ctx e2)

Everything in the above section makes sense. However, it lacks:

  match E as y in ... return ... with
    ...

  end

Thus, my question:

  is "the one rule of dependent type matching"

a) a derivation from dependent theory alone?

b) a derivation from inductive types alone?

c) a derivation that only arises from dependent type theory + inductive types?

I believe it's (c), since "a" alone does not provide inductive types / multiple constructors -- thus nothing to match on; and "b" alone ends up being STLC. Now, assuming it's (c), where can I read up on the mathematical foundations of this? [I've looked through chapters in Coq d'Art, but it's not clear if it's defined in the book.]

Thanks!