LazyWeb to the rescue?

[winterkoninkje]

I've a question for any Coq users out there. How can you provide type equality constraints when doing case matching (ala GADT case matching in Haskell)? That is, assume we've defined something like:

Inductive Stack {A:Set} : nat -> nat -> Set :=
    | stack : (m:nat) -> (n:nat) -> vector A m -> vector A n -> Stack m n.

And now we want to do something like:

Definition
    foo {A:Set} {m n : nat} (s : stack (S m) n) (f : stack m (S n) -> (stack m (S n) *...)) ...
    := ...
        match s with
        | (stack (S m0) n0 (Vcons x0 _m0 xs0) ys0) =>
            let s' := stack m0 (S n0) xs0 (Vcons _ x0 n0 ys0)
            in match f s' with
               | (stack m1 (S n1) xs1 (Vcons y1 _n1 ys1), ...
               end
        end.

Where the type of f is constrained to accept and return stacks with the "right" indices with respect to the parameter s. I keep running into this problem where information about the length indices (i.e., what they're unified with) is getting lost by either one case match or the other. Hopefully I haven't simplified the example so much that you can't see why that would come up. I've tried playing around with different forms of match and moving around the arguments to Stack/stack to no avail. And my google-fu is failing me. Halp!

---

Edit (2010-04-06): For posterity, I've found two solutions to these sorts of problems. The first solution is less general, but more intelligible. Coq has an obscure syntax for dependent case matching which can be used to perform a case match at the type level in order to return different types based on the scrutinee:

Definition head {A:Set} {n:nat} : Vec A (S n) -> A :=
    fun v =>
        match v
            in Vec _ m
            return
                match m with
                | 0 => True (* Impossible *)
                | _ => A
                end
        with
        | VNil         => I (* Impossible *)
        | VCons n x xs => x
        end.

True : Prop is a singleton type with I as the only constructor. The in keyword gives the type of the scrutinee and introduces a new variable. The return keyword gives the type of all the branches of the case expression; in this case we use another case expression in order to analyze m and return either True or A (but namely always A since m = S n). In the outer case match we still need to provide a branch for the VNil case even though it'll never be called; but now we are able to fill out the body of that branch.

The second approach, also mentioned in the above link, is to use the same trick as the inversion tactic produces. This approach is more general and is necessary when doing complex nested case matching, e.g. for doing mutual induction on two parameters. In this version we use the match _ in _ return _ with form again. Except, rather than using a case match in the return, we instead declare that the case expression will return a function (m=S n -> A), that is: a function from proofs that m = S n into the type we wanted in the first place. We then apply the case expression to the obvious proof: (refl_equal (S n)). The tricky thing with this approach is that it's still not always clear what the body of the impossible branch should look like. In essence, we must prove a contradiction and then use the principle of explosion to generate an undefined value of the appropriate type. Doing this is much easier in tactic mode, but here's what the resulting code looks like, cleaned up for legibility:

Definition head {A:Set} {n:nat} : Vec A (S n) -> A :=
    fun v =>
        match v
            in Vec _ Sn
            return Sn = S n -> A
        with
        | VNil =>
            fun (H : 0 = S n) =>
                (* Use the principle of explosion to generate
                   an A from the proof of absurdity *)
                False_rec
                    A
                    (* Prove absurdity from H *)
                    (eq_ind
                        0
                        (fun (e:nat) =>
                            match e with
                            | 0   => True
                            | S _ => False
                            end)
                        I
                        (S n)
                        H)
        | VCons n' x xs =>
            fun (H : S n' = S n) =>
                (* Use the subst tactic, applying the
                   equality (sym_eq...) to rewrite n to n'
                   in (fun (x':A) (xs':Vec A n) => x') *)
                eq_rect
                    n
                    (fun (n'':nat) => A -> Vec A n'' -> A)
                    (fun (x':A) (xs':Vec A n) => x')
                    n'
                    (* Return the symmetry of (f_equal...) *)
                    (sym_eq
                        (f_equal
                            (fun (e:nat) =>
                                match e with
                                | 0    => n'
                                | S n1 => n1
                                end)
                            H))
                (* Apply the result of the above,
                   namely (fun (x':A) (xs':Vec A n') => x') *)
                x
                xs
        end (refl_equal (S n))

Comments

[antayla.livejournal.com]

If you don't get any answers here, I'd try asking at stackoverflow.com.