Week 12: Dependent inductives

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

Subset types and their relatives help us integrate verification with programming. In particular, we have only scratched the tip of the iceberg that is Coq's inductive definition mechanism.

A motivating example

Consider the problem of defining a type of combinational circuits. With the tools we previously studied, we might chose to use a simple inductive type and an interpreter to give the semantics:

Module SimpleTypes.
  Inductive circuit: Set :=
  | ReadRegister (idx: nat) (* Variables *)
  | Constant (bs: list bool)
  | And (c0 c1: circuit)
  | Not (c: circuit)
  | Firstn (c: circuit) (len: nat)
  | Skipn (c: circuit) (idx: nat)
  | Append (c0 c1: circuit)
  | Mux (c c0 c1: circuit).

  Fixpoint simulate (regs: nat -> option (list bool)) (c: circuit)
    : list bool :=
    match c with
    | ReadRegister idx =>
        match regs idx with
        | Some bs => bs
        | None => []
        end
    | Constant bs => bs
    | And c0 c1 =>
        List.map (fun '(b0, b1) => andb b0 b1)
                 (List.combine (simulate regs c0) (simulate regs c1))
    | Not c =>
        List.map negb (simulate regs c)
    | Firstn c len =>
        List.firstn len (simulate regs c)
    | Skipn c idx =>
        List.skipn idx (simulate regs c)
    | Append c0 c1 =>
        simulate regs c0 ++ simulate regs c1
    | Mux c c0 c1 =>
        match simulate regs c with
        | [] => []
        | b :: _ => simulate regs (if b then c0 else c1)
        end
    end.

The resulting simulator can be run like this:

  Definition regs idx :=
    match idx with
    | 0 => Some [false;true;false]
    | 1 => Some [true]
    | _ => None
    end.

  Compute (simulate regs
             (Mux (ReadRegister 1)
                (And (ReadRegister 0) (Constant [false]))
                (Skipn (ReadRegister 1) 2))).= [false]
: list bool

End SimpleTypes.

Unfortunately, this specification is not very readable: we need a default case for undefined registers; the And operation truncates if an argument is longer than the other; Firstn may return less than n bits, and Skipn may run out of bits before skipping as many as requested, etc.

In contrast, if we could ensure that circuits all have the expected bitwidth and that all register references are in bounds, we could eliminate all the unnecessary cruft. With dependent types, we can do just that. Vector.t A n is a list of exactly n elements of type A; and Fin.t n is a number < n.

Module DependentTypes.
  Section DependentTypes.
    Context {nregs: nat} {reg_widths: Vector.t nat nregs}.

    Import VectorDef.VectorNotations.

    Inductive circuit : forall w: nat, Set :=
    | ReadRegister (idx: Fin.t nregs) : circuit reg_widths[@idx]
    | Constant {w} (bs: Vector.t bool w) : circuit w
    | And {w} (c0 c1: circuit w) : circuit w
    | Not {w} (c: circuit w) : circuit w
    | Firstn {w} (c: circuit w) (len: Fin.t (S w))
      : circuit (proj1_sig (Fin.to_nat len))
    | Skipn {w} (c: circuit w) (idx: Fin.t (S w))
      : circuit (w - (proj1_sig (Fin.to_nat idx)))
    | Append {w0 w1} (c0: circuit w0) (c1: circuit w1)
      : circuit (w0 + w1)
    | Mux {w} (c: circuit 1) (c0 c1: circuit w) : circuit w.

    Fixpoint simulate {w}
      (regs: forall idx: Fin.t nregs, Vector.t bool reg_widths[@idx])
      (c: circuit w) : Vector.t bool w :=
      match c with
      | ReadRegister idx => regs idx
      | Constant bs => bs
      | And c0 c1 =>
          Vector.map2 (fun b0 b1 => andb b0 b1)
            (simulate regs c0) (simulate regs c1)
      | Not c =>
          Vector.map negb (simulate regs c)
      | Firstn c len =>
          firstn len (simulate regs c)
      | Skipn c idx =>
          skipn idx (simulate regs c)
      | Append c0 c1 =>
          (simulate regs c0) ++ (simulate regs c1)
      | Mux c c0 c1 =>
          simulate regs (if Vector.hd (simulate regs c) then c0 else c1)
      end.
  End DependentTypes.
End DependentTypes.

Length-Indexed Lists

Many introductions to dependent types start out by showing how to use them to eliminate array bounds checks. When the type of an array tells you how many elements it has, your compiler can detect out-of-bounds dereferences statically. Since we are working in a pure functional language, the next best thing is length-indexed lists, which the following code defines.

Module ilist.
  Section ilist.
    Context {A : Set}.

Note how now we are sure to write out the type of each constructor in full, instead of using the shorthand notation we favored previously. The reason is that now the index to the inductive type ilist depends on details of a constructor's arguments. We are also using Set, the type containing the normal types of programming.

    Inductive ilist : nat -> Set :=
    | Nil : ilist O
    | Cons : forall {n}, A -> ilist n -> ilist (S n).

We see that, within its section, ilist is given type nat -> Set. Previously, every inductive type we have seen has either had plain Set as its type or has been a predicate with some type ending in Prop. The full generality of inductive definitions lets us integrate the expressivity of predicates directly into our normal programming.

The nat argument to ilist tells us the length of the list. The types of ilist's constructors tell us that a Nil list has length O and that a Cons list has length one greater than the length of its tail. We may apply ilist to any natural number, even natural numbers that are only known at runtime. It is this breaking of the phase distinction that characterizes ilist as dependently typed.

In expositions of list types, we usually see the length function defined first, but here that would not be a very productive function to code. Instead, let us implement list concatenation.

    Succeed Fixpoint app
            {n1} (ls1 : ilist n1)
            {n2} (ls2 : ilist n2) : ilist (n1 + n2) :=
      match ls1 with
      | Nil => ls2
      | Cons x ls1' => Cons x (app ls1' ls2)
      end.The command has succeeded and its effects have been reverted.

Past Coq versions signalled an error for this definition. The code is still invalid within Coq's core language, but current Coq versions automatically add annotations to the original program, producing a valid core program. These are the annotations on match discriminees that we began to study with subset types. We can rewrite app to give the annotations explicitly.

    Fixpoint app
             {n1} (ls1 : ilist n1)
             {n2} (ls2 : ilist n2) : ilist (n1 + n2) :=
      match ls1 in (ilist n1) return (ilist (n1 + n2)) with
      | Nil => ls2
      | Cons x ls1' => Cons x (app ls1' ls2)
      end.

Using return alone allowed us to express a dependency of the match result type on the value of the discriminee. What in adds to our arsenal is a way of expressing a dependency on the type of the discriminee. Specifically, the n1 in the in clause above is a binding occurrence whose scope is the return clause.

We may use in clauses only to bind names for the arguments of an inductive type family. That is, each in clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for parameters to the type family must all be underscores. Parameters are those arguments declared with section variables or with entries to the left of the first colon in an inductive definition. They cannot vary depending on which constructor was used to build the discriminee, so Coq prohibits pointless matches on them. It is those arguments defined in the type to the right of the colon that we may name with in clauses.

Here's a useful function with a surprisingly subtle type, where the return type depends on the value of the argument.

    Fixpoint inject (ls : list A) : ilist (length ls) :=
      match ls with
      | nil => Nil
      | h :: t => Cons h (inject t)
      end.

We can define an inverse conversion and prove that it really is an inverse.

    Fixpoint unject {n} (ls : ilist n) : list A :=
      match ls with
      | Nil => nil
      | Cons h t => h :: unject t
      end.

    Theorem inject_inverse : forall ls, unject (inject ls) = ls.A: Set
forall ls : list A, unject (inject ls) = ls
    Proof.A: Set
forall ls : list A, unject (inject ls) = ls
      induction ls; simpl; congruence.
    Qed.

Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so. We write _ for a term that we wish Coq would fill in for us, but we'll have no such luck.

    Fail Definition hd {n} (ls : ilist (S n)) : A :=
      match ls with
      | Nil => _
      | Cons h _ => h
      end.The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (fun (n : nat) (ls : ilist (S n)) =>
   match
     ls in (ilist n0)
     return match n0 with
            | 0 => IDProp
            | S _ => A
            end
   with
   | Nil => ?i
   | Cons h _ => h
   end)
More precisely: 
- ?i: Cannot infer this placeholder of type "IDProp"
  in environment:
  A : Set
  n : nat
  ls : ilist (S n)

It is not clear what to write for the Nil case, so we are stuck before we even turn our function over to the type checker. We could try omitting the Nil case.

    Succeed Definition hd {n} (ls : ilist (S n)) : A :=
      match ls with
      | Cons h _ => h
      end.The command has succeeded and its effects have been reverted.

Actually, these days, Coq is smart enough to make that definition work! However, it will be educational to look at how Coq elaborates this code into its core language, where, unlike in ML, all pattern matching must be exhaustive. We might try using an in clause somehow.

    Succeed Definition hd {n} (ls : ilist (S n)) : A :=
      match ls in (ilist (S n)) with
      | Cons h _ => h
      end.The command has succeeded and its effects have been reverted.

Due to some relatively new heuristics, Coq does accept this code, but in general it is not legal to write arbitrary patterns for the arguments of inductive types in in clauses. Only variables are permitted there, in Coq's core language. A completely general mechanism could only be supported with a solution to the problem of higher-order unification, which is undecidable.

Our final, working attempt at hd uses an auxiliary function and a surprising return annotation.

    Definition hd' {n} (ls : ilist n) :=
      match ls in (ilist n)
            return (match n with O => unit | S _ => A end) with
      | Nil => tt
      | Cons h _ => h
      end.

    Check hd'.hd'
     : ilist ?n ->
       match ?n with
       | 0 => unit
       | S _ => A
       end
where
?n : [A : Set |- nat]

    Definition hd {n} (ls : ilist (S n)) : A := hd' ls.

We annotate our main match with a type that is itself a match. We write that the function hd' returns unit when the list is empty and returns the carried type A in all other cases. In the definition of hd, we just call hd'. Because the index of ls is known to be nonzero, the type checker reduces the match in the type of hd' to A.

In fact, when we "got lucky" earlier with Coq accepting simpler definitions, under the hood it was desugaring almost to this one.

    Definition easy_hd {n} (ls : ilist (S n)) : A :=
      match ls with
      | Cons h _ => h
      end.

    Print easy_hd.easy_hd =
fun (n : nat) (ls : ilist (S n)) =>
match
  ls in (ilist n0)
  return match n0 with
         | 0 => IDProp
         | S _ => A
         end
with
| Nil => idProp
| Cons h _ => h
end
     : forall {n : nat}, ilist (S n) -> A

Arguments easy_hd {n}%nat_scope ls
easy_hd uses section variable A.
  End ilist.

  Arguments ilist A n : clear implicits.
End ilist.

Functions on ilist can be extracted, and are quite readable:

Extraction ilist.app.(** val app :
    nat -> 'a1 ilist -> nat -> 'a1 ilist -> 'a1 ilist **)

let rec app _ ls1 n2 ls2 =
  match ls1 with
  | Nil -> ls2
  | Cons (n, x, ls1') ->
    Cons ((add n n2), x, (app n ls1' n2 ls2))

The One Rule of Dependent Pattern Matching in Coq

The rest of this chapter will demonstrate a few other elegant applications of dependent types in Coq. Readers encountering such ideas for the first time often feel overwhelmed, concluding that there is some magic at work whereby Coq sometimes solves the halting problem for the programmer and sometimes does not, applying automated program understanding in a way far beyond what is found in conventional languages. The point of this section is to cut off that sort of thinking right now! Dependent type-checking in Coq follows just a few algorithmic rules, with just one for dependent pattern matching of the kind we met in the previous section.

A dependent pattern match is a match expression where the type of the overall match is a function of the value and/or the type of the discriminee, the value being matched on. In other words, the match type depends on the discriminee.

When exactly will Coq accept a dependent pattern match as well-typed? Some other dependently typed languages employ fancy decision procedures to determine when programs satisfy their very expressive types. The situation in Coq is just the opposite. Only very straightforward symbolic rules are applied. Such a design choice has its drawbacks, as it forces programmers to do more work to convince the type checker of program validity. However, the great advantage of a simple type checking algorithm is that its action on invalid programs is easier to understand!

We come now to the one rule of dependent pattern matching in Coq. A general dependent pattern match assumes this form (with unnecessary parentheses included to make the syntax easier to parse):

match E as y in (T x1 ... xn) return U with
  | C z1 ... zm => B
  | ...
end

The discriminee is a term E, a value in some inductive type family T, which takes n arguments. An as clause binds the name y to refer to the discriminee E. An in clause binds an explicit name xi for the i`th argument passed to `T in the type of E.

We bind these new variables y and xi so that they may be referred to in U, a type given in the return clause. The overall type of the match will be U, with E substituted for y, and with each xi substituted by the actual argument appearing in that position within E's type.

In general, each case of a match may have a pattern built up in several layers from the constructors of various inductive type families. To keep this exposition simple, we will focus on patterns that are just single applications of inductive type constructors to lists of variables. Coq actually compiles the more general kind of pattern matching into this more restricted kind automatically, so understanding the typing of match requires understanding the typing of matches lowered to match one constructor at a time.

The last piece of the typing rule tells how to type-check a match case. A generic constructor application C z1 ... zm has some type T x1' ... xn', an application of the type family used in E's type, probably with occurrences of the zi variables. From here, a simple recipe determines what type we will require for the case body B. The type of B should be U with the following two substitutions applied: we replace y (the as clause variable) with C z1 ... zm, and we replace each xi (the in clause variables) with xi'. In other words, we specialize the result type based on what we learn from which pattern has matched the discriminee.

This is an exhaustive description of the ways to specify how to take advantage of which pattern has matched! No other mechanisms come into play. For instance, there is no way to specify that the types of certain free variables should be refined based on which pattern has matched.

A few details have been omitted above. Inductive type families may have both parameters and regular arguments. Within an in clause, a parameter position must have the wildcard _ written, instead of a variable. (In general, Coq uses wildcard _'s either to indicate pattern variables that will not be mentioned again or to indicate positions where we would like type inference to infer the appropriate terms.) Furthermore, recent Coq versions are adding more and more heuristics to infer dependent match annotations in certain conditions. The general annotation-inference problem is undecidable, so there will always be serious limitations on how much work these heuristics can do. When in doubt about why a particular dependent match is failing to type-check, add an explicit return annotation! At that point, the mechanical rule sketched in this section will provide a complete account of "what the type checker is thinking." Be sure to avoid the common pitfall of writing a return annotation that does not mention any variables bound by in or as; such a match will never refine typing requirements based on which pattern has matched. (One simple exception to this rule is that, when the discriminee is a variable, that same variable may be treated as if it were repeated as an as clause.)

Exercise: The eq type

Use your understanding of these rules to define (from first principles) the nat_ind and eq_rect recursors:

Check nat_ind.nat_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n

Solution

Fixpoint nat_ind
         (P : nat -> Prop)
         (H0 : P 0)
         (HS : forall n : nat, P n -> P (S n))
         (n: nat) :=
  match n with
  | 0 => H0
  | S n' => HS n' (nat_ind P H0 HS n')
  end.

Check eq_rect.eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall y : A, x = y -> P y

Solution

Definition eq_rect
           (A : Type) (x : A) (P : A -> Type)
           (Px: P x) (y : A) (Hxy: eq x y): P y :=
  match Hxy in eq _ x' return P x' with
  | eq_refl => Px
  end.

A Tagless Interpreter

A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a tagless interpreter that both removes this source of runtime inefficiency and gives us more confidence that our implementation is correct.

Inductive type : Set :=
| Nat : type
| Bool : type
| Prod : type -> type -> type.

Inductive exp : type -> Set :=
| NConst : nat -> exp Nat
| Plus : exp Nat -> exp Nat -> exp Nat
| Eq : exp Nat -> exp Nat -> exp Bool

| BConst : bool -> exp Bool
| And : exp Bool -> exp Bool -> exp Bool
| If : forall {t}, exp Bool -> exp t -> exp t -> exp t

| Pair : forall {t1 t2}, exp t1 -> exp t2 -> exp (Prod t1 t2)
| Fst : forall {t1 t2}, exp (Prod t1 t2) -> exp t1
| Snd : forall {t1 t2}, exp (Prod t1 t2) -> exp t2.

We have a standard algebraic datatype type, defining a type language of naturals, Booleans, and product (pair) types. Then we have the indexed inductive type exp, where the argument to exp tells us the encoded type of an expression. In effect, we are defining the typing rules for expressions simultaneously with the syntax.

We can give types and expressions semantics in a new style, based critically on the chance for type-level computation.

Fixpoint typeDenote (t : type) : Set :=
  match t with
    | Nat => nat
    | Bool => bool
    | Prod t1 t2 => typeDenote t1 * typeDenote t2
  end%type.

The typeDenote function compiles types of our object language into "native" Coq types. It is deceptively easy to implement. The only new thing we see is the %type annotation, which tells Coq to parse the match expression using the notations associated with types. Without this annotation, the * would be interpreted as multiplication on naturals, rather than as the product type constructor. The token %type is one example of an identifier bound to a notation scope delimiter.

We can define a function expDenote that is typed in terms of typeDenote.

Fixpoint expDenote {t} (e : exp t) : typeDenote t :=
  match e in exp t return typeDenote t with
    | NConst n => n
    | Plus e1 e2 => expDenote e1 + expDenote e2
  | Eq e1 e2 =>
      if PeanoNat.Nat.eq_dec (expDenote e1) (expDenote e2)
      then true else false

    | BConst b => b
    | And e1 e2 => expDenote e1 && expDenote e2
    | If e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2

    | Pair e1 e2 => (expDenote e1, expDenote e2)
    | Fst e' => fst (expDenote e')
    | Snd e' => snd (expDenote e')
  end.

Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form if E then true else false in the Eq case. Remember that ==n has a rich dependent type, rather than a simple Boolean type. Coq's native if is overloaded to work on a test of any two-constructor type, so we can use if to build a simple Boolean from the sumbool that ==n returns.

We can implement our old favorite, a constant-folding function, and prove it correct. It will be useful to write a function pairOut that checks if an exp of Prod type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error.

Fail Definition pairOut t1 t2
     (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
  match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
    | Pair e1 e2 => Some (e1, e2)
    | _ => None
  end.The command has indeed failed with message:
In environment
t1 : type
t2 : type
e : exp (Prod t1 t2)
t : type
e0 : exp Bool
e1 : exp t
e2 : exp t
The term "None" has type "option ?A"
while it is expected to have type
 "match t as iV return (exp iV -> Type) with
  | Nat =>
      fun e3 : exp Nat =>
      option
        ?T@{e0:=e; iV:=t; e1:=If e0 e1 e2; e:=e3;
            e2:=e3}
  | Bool =>
      fun e3 : exp Bool =>
      option
        ?T0@{e0:=e; iV:=t; e1:=If e0 e1 e2; e:=e3;
             e2:=e3}
  | Prod t1 t2 =>
      fun _ : exp (Prod t1 t2) =>
      option (exp t1 * exp t2)
  end (If e0 e1 e2)".

We run again into the problem of not being able to specify non-variable arguments in in clauses (and this time Coq's avant-garde heuristics don't save us). The problem would just be hopeless without a use of an in clause, though, since the result type of the match depends on an argument to exp. Our solution will be to use a more general type, as we did for hd. First, we define a type-valued function to use in assigning a type to pairOut.

Definition pairOutType (t : type) :=
  option (match t with
          | Prod t1 t2 => exp t1 * exp t2
          | _ => unit
          end).

When passed a type that is a product, pairOutType returns our final desired type. On any other input type, pairOutType returns the harmless option unit, since we do not care about extracting components of non-pairs. Now pairOut is easy to write.

Definition pairOut {t} (e : exp t) :=
  match e in (exp t) return (pairOutType t) with
    | Pair e1 e2 => Some (e1, e2)
    | _ => None
  end.

With pairOut available, we can write cfold in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden.

Fixpoint cfold {t} (e : exp t) : exp t :=
  match e with
  | NConst n => NConst n
  | Plus e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
      match e1', e2' with
      | NConst n1, NConst n2 => NConst (n1 + n2)
      | _, _ => Plus e1' e2'
      end
  | Eq e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
      match e1', e2' with
      | NConst n1, NConst n2 =>
          BConst (if PeanoNat.Nat.eq_dec n1 n2 then true else false)
      | _, _ => Eq e1' e2'
      end

  | BConst b => BConst b
  | And e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
      match e1', e2' with
      | BConst b1, BConst b2 => BConst (b1 && b2)
      | _, _ => And e1' e2'
      end
  | If e e1 e2 =>
      let e' := cfold e in
      match e' with
      | BConst true => cfold e1
      | BConst false => cfold e2
      | _ => If e' (cfold e1) (cfold e2)
      end

  | Pair e1 e2 => Pair (cfold e1) (cfold e2)
  | Fst e =>
      let e' := cfold e in
      match pairOut e' with
      | Some p => fst p
      | None => Fst e'
      end
  | Snd e =>
      let e' := cfold e in
      match pairOut e' with
      | Some p => snd p
      | None => Snd e'
      end
  end.

The correctness theorem for cfold turns out to be easy to prove, once we get over one serious hurdle.

Require Import Coq.Program.Equality.

Ltac dep_cases E :=
  let x := fresh "x" in
  remember E as x; simpl in x; dependent destruction x;
  try match goal with
      | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
      end.

Theorem cfold_correct :
  forall t (e : exp t), expDenote e = expDenote (cfold e).forall (t : type) (e : exp t),
expDenote e = expDenote (cfold e)
Proof.forall (t : type) (e : exp t),
expDenote e = expDenote (cfold e)
  induction e; simpl; try congruence.e1, e2: exp Nat
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote
  match cfold e1 with
  | NConst n1 =>
      match cfold e2 with
      | NConst n2 => NConst (n1 + n2)
      | _ => Plus (cfold e1) (cfold e2)
      end
  | _ => Plus (cfold e1) (cfold e2)
  end
e1, e2: exp Nat
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
(if PeanoNat.Nat.eq_dec (expDenote e1) (expDenote e2)
 then true
 else false) =
expDenote
  match cfold e1 with
  | NConst n1 =>
      match cfold e2 with
      | NConst n2 =>
          BConst
            (if PeanoNat.Nat.eq_dec n1 n2
             then true
             else false)
      | _ => Eq (cfold e1) (cfold e2)
      end
  | _ => Eq (cfold e1) (cfold e2)
  end
e1, e2: exp Bool
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 && expDenote e2 =
expDenote
  match cfold e1 with
  | BConst b1 =>
      match cfold e2 with
      | BConst b2 => BConst (b1 && b2)
      | _ => And (cfold e1) (cfold e2)
      end
  | _ => And (cfold e1) (cfold e2)
  end
t: type
e1: exp Bool
e2, e3: exp t
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
IHe3: expDenote e3 = expDenote (cfold e3)
(if expDenote e1 then expDenote e2 else expDenote e3) =
expDenote
  match cfold e1 with
  | BConst true => cfold e2
  | BConst false => cfold e3
  | _ => If (cfold e1) (cfold e2) (cfold e3)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
fst (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => fst p
  | None => Fst (cfold e)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
snd (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => snd p
  | None => Snd (cfold e)
  end

We would like to do a case analysis on cfold e1, and we attempt to do so in the way that has worked so far.

  Fail destruct (cfold e1).The command has indeed failed with message:
Abstracting over the terms "t" and "e" leads to a term
fun (t0 : type) (e0 : exp t0) =>
forall e3 e4 : exp t0,
expDenote e3 = expDenote e0 ->
expDenote e4 = expDenote (cfold e4) ->
expDenote e3 + expDenote e4 =
expDenote
  match e0 with
  | NConst n1 =>
      match cfold e4 with
      | NConst n2 => NConst (n1 + n2)
      | _ => Plus e0 (cfold e4)
      end
  | _ => Plus e0 (cfold e4)
  end
which is ill-typed.
Reason is: Illegal application: 
The term "Nat.add" of type "nat -> nat -> nat"
cannot be applied to the terms
 "expDenote e3" : "typeDenote t0"
 "expDenote e4" : "typeDenote t0"
The 1st term has type "typeDenote t0"
which should be a subtype of "nat".
e1, e2: exp Nat
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote
  match cfold e1 with
  | NConst n1 =>
      match cfold e2 with
      | NConst n2 => NConst (n1 + n2)
      | _ => Plus (cfold e1) (cfold e2)
      end
  | _ => Plus (cfold e1) (cfold e2)
  end
e1, e2: exp Nat
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
(if PeanoNat.Nat.eq_dec (expDenote e1) (expDenote e2)
 then true
 else false) =
expDenote
  match cfold e1 with
  | NConst n1 =>
      match cfold e2 with
      | NConst n2 =>
          BConst
            (if PeanoNat.Nat.eq_dec n1 n2
             then true
             else false)
      | _ => Eq (cfold e1) (cfold e2)
      end
  | _ => Eq (cfold e1) (cfold e2)
  end
e1, e2: exp Bool
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 && expDenote e2 =
expDenote
  match cfold e1 with
  | BConst b1 =>
      match cfold e2 with
      | BConst b2 => BConst (b1 && b2)
      | _ => And (cfold e1) (cfold e2)
      end
  | _ => And (cfold e1) (cfold e2)
  end
t: type
e1: exp Bool
e2, e3: exp t
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
IHe3: expDenote e3 = expDenote (cfold e3)
(if expDenote e1 then expDenote e2 else expDenote e3) =
expDenote
  match cfold e1 with
  | BConst true => cfold e2
  | BConst false => cfold e3
  | _ => If (cfold e1) (cfold e2) (cfold e3)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
fst (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => fst p
  | None => Fst (cfold e)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
snd (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => snd p
  | None => Snd (cfold e)
  end

A nasty error message greets us!

  dep_cases (cfold e1).e1, e2: exp Nat
n: nat
IHe1: expDenote e1 = expDenote (NConst n)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote
  match cfold e2 with
  | NConst n2 => NConst (n + n2)
  | _ => Plus (NConst n) (cfold e2)
  end
e1, e2, x1, x2: exp Nat
IHe1: expDenote e1 = expDenote (Plus x1 x2)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote (Plus (Plus x1 x2) (cfold e2))
e1, e2: exp Nat
x1: exp Bool
x2, x3: exp Nat
IHe1: expDenote e1 = expDenote (If x1 x2 x3)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote (Plus (If x1 x2 x3) (cfold e2))
e1, e2: exp Nat
t2: type
x: exp (Prod Nat t2)
IHe1: expDenote e1 = expDenote (Fst x)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote (Plus (Fst x) (cfold e2))
e1, e2: exp Nat
t1: type
x: exp (Prod t1 Nat)
IHe1: expDenote e1 = expDenote (Snd x)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 + expDenote e2 =
expDenote (Plus (Snd x) (cfold e2))
e1, e2: exp Nat
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
(if PeanoNat.Nat.eq_dec (expDenote e1) (expDenote e2)
 then true
 else false) =
expDenote
  match cfold e1 with
  | NConst n1 =>
      match cfold e2 with
      | NConst n2 =>
          BConst
            (if PeanoNat.Nat.eq_dec n1 n2
             then true
             else false)
      | _ => Eq (cfold e1) (cfold e2)
      end
  | _ => Eq (cfold e1) (cfold e2)
  end
e1, e2: exp Bool
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
expDenote e1 && expDenote e2 =
expDenote
  match cfold e1 with
  | BConst b1 =>
      match cfold e2 with
      | BConst b2 => BConst (b1 && b2)
      | _ => And (cfold e1) (cfold e2)
      end
  | _ => And (cfold e1) (cfold e2)
  end
t: type
e1: exp Bool
e2, e3: exp t
IHe1: expDenote e1 = expDenote (cfold e1)
IHe2: expDenote e2 = expDenote (cfold e2)
IHe3: expDenote e3 = expDenote (cfold e3)
(if expDenote e1 then expDenote e2 else expDenote e3) =
expDenote
  match cfold e1 with
  | BConst true => cfold e2
  | BConst false => cfold e3
  | _ => If (cfold e1) (cfold e2) (cfold e3)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
fst (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => fst p
  | None => Fst (cfold e)
  end
t1, t2: type
e: exp (Prod t1 t2)
IHe: expDenote e = expDenote (cfold e)
snd (expDenote e) =
expDenote
  match pairOut (cfold e) with
  | Some p => snd p
  | None => Snd (cfold e)
  end

Incidentally, general and fully precise case analysis on dependently typed variables is undecidable, as witnessed by a simple reduction from the known-undecidable problem of higher-order unification, which has come up a few times already. The tactic dep_cases makes a best effort to handle some common cases.

This successfully breaks the subgoal into 5 new subgoals, one for each constructor of exp that could produce an exp Nat. Note that dep_cases is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like hd and pairOut.

This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof.

  Restart.forall (t : type) (e : exp t),
expDenote e = expDenote (cfold e)

  induction e; simpl;
    repeat
      (match goal with
       | [ |- context[match cfold ?E
                     with NConst _ => _ | _ => _ end] ] =>
           dep_cases (cfold E)
       | [ |- context[match pairOut (cfold ?E) with
                     | Some _ => _
                     | None => _ end] ] =>
           dep_cases (cfold E)
       | [ |- context[if ?E then _ else _] ] => destruct E
       | [ H : _ = _ |- _ ] => rewrite H
       end; simpl in *); congruence.
Qed.

Interlude: The Convoy Pattern

Here are some examples, contemplation of which may provoke enlightenment. See more discussion later of the idea behind the examples.

Module MoreIlist.
  Import ilist.

  Fail Definition firstElements
       {n A B}
       (ls1 : ilist A n)
       (ls2 : ilist B n) : option (A * B) :=
    match ls1 with
    | Cons v1 _ =>
        Some (v1,
               match ls2 in ilist _ N
                     return match N with
                            | O => unit
                            | S _ => B end with
               | Cons v2 _ => v2
               | Nil => tt
               end)
    | Nil => None
    end.The command has indeed failed with message:
In environment
n : nat
A : Set
B : Set
ls1 : ilist A n
ls2 : ilist B n
n0 : nat
v1 : A
i : ilist A n0
The term
 "Some
    (v1,
     match
       ls2 in (ilist _ N)
       return match N with
              | 0 => unit
              | S _ => B
              end
     with
     | Nil => tt
     | Cons v2 _ => v2
     end)" has type
 "option (A * match n with
              | 0 => unit
              | S _ => B
              end)" while it is expected to have type
 "option (A * B)".

  Definition firstElements
             {n A B} (ls1 : ilist A n) (ls2 : ilist B n)
    : option (A * B) :=
    match ls1 in ilist _ N return ilist B N -> option (A * B) with
    | Cons v1 _ =>
        fun ls2 =>
          Some (v1,
                 match ls2 in ilist _ N
                       return match N with
                              | O => unit
                              | S _ => B end with
                 | Cons v2 _ => v2
                 | Nil => tt
                 end)
    | Nil => fun _ => None
    end ls2.

Note use of a struct annotation to tell Coq which argument should decrease across recursive calls. It's an artificial choice here, since usually those annotations are inferred. Here we are making an effort to demonstrate a decently common problem!

  Fail Fixpoint zip
       {n A B} (ls1 : ilist A n) (ls2 : ilist B n)
       {struct ls1} : ilist (A * B) n :=
    match ls1 in ilist _ N return ilist B N -> ilist (A * B) N with
    | Cons v1 ls1' =>
        fun ls2 =>
          match ls2 in ilist _ N return
                match N with
                | O => unit
                | S N' => ilist A N' -> ilist (A * B) N
                end with
          | Cons v2 ls2' =>
              fun ls1' => Cons (v1, v2) (zip ls1' ls2')
          | Nil => tt
          end ls1'
    | Nil => fun _ => Nil
    end ls2.The command has indeed failed with message:
Recursive definition of zip is ill-formed.
In environment
zip :
  forall (n : nat) (A B : Set),
  ilist A n -> ilist B n -> ilist (A * B) n
n : nat
A : Set
B : Set
ls1 : ilist A n
ls2 : ilist B n
n0 : nat
v1 : A
ls1' : ilist A n0
ls0 : ilist B (S n0)
n1 : nat
v2 : B
ls2' : ilist B n1
ls1'0 : ilist A n1
Recursive call to zip has principal argument equal to
"ls1'0" instead of "ls1'".
Recursive definition is:
"fun (n : nat) (A B : Set) (ls1 : ilist A n)
   (ls2 : ilist B n) =>
 match
   ls1 in (ilist _ N)
   return (ilist B N -> ilist (A * B) N)
 with
 | Nil => fun _ : ilist B 0 => Nil
 | @Cons _ n0 v1 ls1' =>
     fun ls3 : ilist B (S n0) =>
     match
       ls3 in (ilist _ N)
       return
         match N with
         | 0 => unit
         | S N' => ilist A N' -> ilist (A * B) N
         end
     with
     | Nil => tt
     | @Cons _ n1 v2 ls2' =>
         fun ls1'0 : ilist A n1 =>
         Cons (v1, v2) (zip n1 A B ls1'0 ls2')
     end ls1'
 end ls2".

  Fixpoint zip {n A B} (ls1 : ilist A n) (ls2 : ilist B n)
           {struct ls1} : ilist (A * B) n :=
    match ls1 in ilist _ N return ilist B N -> ilist (A * B) N with
    | Cons v1 ls1' =>
        fun ls2 =>
          match ls2 in ilist _ N
                return match N with
                       | O => unit
                       | S N' => (ilist B N' ->
                                  ilist (A * B) N') ->
                                  ilist (A * B) N
                       end with
          | Cons v2 ls2' =>
              fun zip_ls1' => Cons (v1, v2) (zip_ls1' ls2')
          | Nil => tt
          end (zip ls1')
    | Nil => fun _ => Nil
    end ls2.
End MoreIlist.

A different take on length-indexed lists

Module fixlist.
  Section fixlist.
    Context {A : Type}.

    Fixpoint fixlist n: Type :=
      match n with
      | 0 => unit
      | S n => A * fixlist n
      end.

    Definition hd {n} (v: fixlist (S n)) :=
      fst v.

    Fixpoint app {n0} (v0: fixlist n0) {n1} (v1: fixlist n1):
      fixlist (n0 + n1) :=
      match n0 return fixlist n0 -> fixlist (n0 + n1) with
      | 0 => fun _ => v1
      | S n => fun v0 => (fst v0, app (snd v0) v1)
      end v0.

    Fixpoint inject (ls : list A): fixlist (length ls) :=
      match ls return fixlist (length ls) with
      | [] => tt
      | hd :: tl => (hd, inject tl)
      end.

    Fixpoint unject {n} (v : fixlist n): list A :=
      match n return fixlist n -> list A with
      | 0 => fun _ => []
      | S n => fun v => fst v :: unject (snd v)
      end v.
  End fixlist.

  Arguments fixlist A n : clear implicits.

Exercise: More fixlist functions

Define the functions zip, map, and map2.

Solution

  Fixpoint zip {A B n} (va: fixlist A n) (vb: fixlist B n)
    : fixlist (A * B) n :=

    match n return fixlist A n -> fixlist B n -> fixlist (A * B) n with
    | 0 => fun _ _ => tt
    | S n => fun va vb => ((fst va, fst vb), zip (snd va) (snd vb))
    end va vb.

  Fixpoint map {A B n} (f: A -> B) :=
    match n return fixlist A n ->
                   fixlist B n with
    | 0 => fun _ => tt
    | S n =>
        fun fl => (f (fst fl), map f (snd fl))
    end.

  Fixpoint map2 {A B C n} (f: A -> B -> C) :=
    match n return fixlist A n ->
                   fixlist B n ->
                   fixlist C n with
    | 0 => fun _ _ => tt
    | S n =>
        fun fla flb =>
          (f (fst fla) (fst flb),
            map2 f (snd fla) (snd flb))
    end.

End fixlist.

Exercises

Exercise: Circuits again

Redefine the circuit interpreter to use fixlists.

Solution

Fixpoint fixnat_to_nat {n} :=
  match n return fixnat n -> nat with
  | 0 => fun f => False_rect _ f
  | S n => fun f =>
            match f with
            | None => 0
            | Some f => S (fixnat_to_nat f)
            end
  end.

Module DependentTypes2.
  Module fixlist.
    Include fixlist.

    Fixpoint firstn {A n} :=
      match n return forall f: fixnat (S n),
          fixlist A n ->
          fixlist A (@fixnat_to_nat (S n) f) with
      | 0 =>
          fun f fl =>
            match f with
            | None => fl
            | Some f => False_rect _ f
            end
      | S n =>
          fun f fl =>
            match f with
            | None => tt
            | Some f => (fst fl, firstn f (snd fl))
            end
      end.

    Fixpoint skipn {A n} :=
      match n return forall f: fixnat (S n),
          fixlist A n ->
          fixlist A (n - (@fixnat_to_nat (S n) f)) with
      | 0 => fun _ fl => fl
      | S n =>
          fun f fl =>
            match f with
            | None => fl
            | Some f => skipn f (snd fl)
            end
      end.

    Fixpoint append {A n0 n1} :=
      match n0 return fixlist A n0 -> fixlist A n1 ->
                      fixlist A (n0 + n1) with
      | 0 => fun _ fl1 => fl1
      | S n => fun fl0 fl1 => (fst fl0, append (snd fl0) fl1)
      end.
  End fixlist.

  Import fixlist.
  Print Module fixlist.Module
fixlist
:= Struct
     Definition fixlist : Type -> nat -> Type.
     Definition hd :
       forall (A : Type) (n : nat),
       fixlist A (S n) -> A.
     Definition app :
       forall (A : Type) (n0 : nat),
       fixlist A n0 ->
       forall n1 : nat,
       fixlist A n1 -> fixlist A (n0 + n1).
     Definition inject :
       forall (A : Type) (ls : list A),
       fixlist A (Datatypes.length ls).
     Definition unject :
       forall (A : Type) (n : nat),
       fixlist A n -> list A.
     Definition zip :
       forall (A B : Type) (n : nat),
       fixlist A n -> fixlist B n -> fixlist (A * B) n.
     Definition map :
       forall (A B : Type) (n : nat),
       (A -> B) ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (A * fixlist n1)%type
          end) n ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (B * fixlist n1)%type
          end) n.
     Definition map2 :
       forall (A B C : Type) (n : nat),
       (A -> B -> C) ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (A * fixlist n1)%type
          end) n ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (B * fixlist n1)%type
          end) n ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (C * fixlist n1)%type
          end) n.
     Definition firstn :
       forall (A : Type) (n : nat)
         (x : option
                ((fix fixnat (n0 : nat) : Set :=
                    match n0 with
                    | 0 => False
                    | S n1 => option (fixnat n1)
                    end) n)),
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (A * fixlist n1)%type
          end) n ->
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (A * fixlist n1)%type
          end)
         match x with
         | Some f =>
             S
               ((fix fixnat_to_nat (n0 : nat) :
                     (fix fixnat (n1 : nat) : Set :=
                        match n1 with
                        | 0 => False
                        | S n2 => option (fixnat n2)
                        end) n0 -> nat :=
                   match
                     n0 as n1
                     return (fixnat n1 -> nat)
                   with
                   | 0 =>
                       fun f0 : fixnat 0 =>
                       False_rect nat f0
                   | S n1 =>
                       fun f0 : fixnat (S n1) =>
                       match f0 with
                       | Some f1 =>
                           S (fixnat_to_nat n1 f1)
                       | None => 0
                       end
                   end) n f)
         | None => 0
         end.
     Definition skipn :
       forall (A : Type) (n : nat)
         (x : option
                ((fix fixnat (n0 : nat) : Set :=
                    match n0 with
                    | 0 => False
                    | S n1 => option (fixnat n1)
                    end) n)),
       (fix fixlist (n0 : nat) : Type :=
          match n0 with
          | 0 => unit
          | S n1 => (A * fixlist n1)%type
          end) n ->
       fixlist A (S n - fixnat_to_nat (Some x)).
     Definition append :
       forall (A : Type) (n0 n1 : nat),
       (fix fixlist (n : nat) : Type :=
          match n with
          | 0 => unit
          | S n2 => (A * fixlist n2)%type
          end) n0 ->
       fixlist A n1 ->
       (fix fixlist (n : nat) : Type :=
          match n with
          | 0 => unit
          | S n2 => (A * fixlist n2)%type
          end)
         ((fix add (n m : nat) {struct n} : nat :=
             match n with
             | 0 => m
             | S p => S (add p m)
             end) n0 n1).
   End

  Section DependentTypes2.
    Context {nregs: nat} {reg_widths: fixlist nat nregs}.

    Inductive circuit : forall w: nat, Type :=
    | ReadRegister (idx: fixnat nregs)
      : circuit (fixlist_nth reg_widths idx)
    | Constant {w} (bs: fixlist bool w)
      : circuit w
    | And {w} (c0 c1: circuit w)
      : circuit w
    | Not {w} (c: circuit w)
      : circuit w
    | Firstn {w} (c: circuit w) (len: fixnat (S w))
      : circuit (@fixnat_to_nat (S w) len)
    | Skipn {w} (c: circuit w) (idx: fixnat (S w))
      : circuit (w - (@fixnat_to_nat (S w) idx))
    | Append {w0 w1} (c0: circuit w0) (c1: circuit w1)
      : circuit (w0 + w1)
    | Mux {w} (c: circuit 1) (c0 c1: circuit w) : circuit w.

    Fixpoint simulate
             {w}
             (regs: forall idx: fixnat nregs,
                 fixlist bool (fixlist_nth reg_widths idx))
             (c: circuit w) : fixlist bool w :=
    match c with
    | ReadRegister idx => regs idx
    | Constant bs => bs
    | And c0 c1 =>
        map2 (fun b0 b1 => andb b0 b1)
          (simulate regs c0) (simulate regs c1)
    | Not c =>
        map negb (simulate regs c)
    | Firstn c len =>
        firstn len (simulate regs c)
    | Skipn c idx =>
        skipn idx (simulate regs c)
    | Append c0 c1 =>
        app (simulate regs c0) (simulate regs c1)
    | Mux c c0 c1 =>
        simulate regs (if fst (simulate regs c) then c0 else c1)
    end.
  End DependentTypes2.
End DependentTypes2.

Exercise: Feeling challenged?

Try the challenge above with fixnat and fixlist.

Definition register_sizes: fixlist nat 2 := (3, (4, tt)).

Definition renv (idx: fixnat 2)
  : fixlist bool (fixlist_nth register_sizes idx).idx: fixnat 2
fixlist bool (fixlist_nth register_sizes idx)
Abort.

Solution

Definition renv (idx: fixnat 2)
  : fixlist bool (fixlist_nth register_sizes idx) :=
  match idx return fixlist bool (fixlist_nth register_sizes idx) with
  | None => (false, (false, (true, tt)))
  | Some None => (false, (true, (false, (true, tt))))
  | Some (Some fl) => False_rect _ fl
  end.

It computes just fine:

Compute renv None.= (false, (false, (true, tt)))
: fixlist bool (fixlist_nth register_sizes None)

And it extracts beautifully:

Extraction renv.(** val renv : fixnat -> bool Coq_fixlist.fixlist **)

let renv idx =
  match Obj.magic idx with
  | Some f ->
    (match f with
     | Some _ -> assert false (* absurd case *)
     | None ->
       Obj.magic (Pair (False, (Pair (True, (Pair
         (False, (Pair (True, Tt)))))))))
  | None ->
    Obj.magic (Pair (False, (Pair (False, (Pair (True,
      Tt))))))

Systems and
Formalisms Lab

Week 12: Dependent inductives

A motivating example

Length-Indexed Lists

The One Rule of Dependent Pattern Matching in Coq

A Tagless Interpreter

Interlude: The Convoy Pattern

A different take on length-indexed lists

A hard exercise

Exercises