The Coq mailing list

[Andrew Rodriguez <amr1 AT andrew.cmu.edu>]

In the course of defining a simple reverse vector function I defined a function: 

Require Import VectorDef.

Definition vec := VectorDef.t.

Definition vnil := VectorDef.nil.

Definition vcons := VectorDef.cons.

Lemma plus_0_doesn't_matter {m} (va : prod (vec A 0) (vec A m)) : prod (vec A 0) (vec A (m + 0)).

assert (vec A m = vec A (m + 0)).

f_equal. auto.

rewrite <-H.

trivial.

Defined.

Eval compute in plus_0_doesn't_matter (vnil A, vnil A).

>   = match

         match

           match

             plus_n_O 0 in (_ = y) return (VectorDef.t A 0 = VectorDef.t A y)

           with

           | eq_refl => eq_refl

           end in (_ = y) return (VectorDef.t A 0 = y)

         with

         | eq_refl => eq_refl

         end in (_ = y) return (VectorDef.t A 0 * y)

       with

       | eq_refl => (VectorDef.nil A, VectorDef.nil A)

       end

     : vec A 0 * vec A (0 + 0)

As you can see, when I try to evaluate it gets stuck on plus_n_O because it's defined opaque. I end up building on this function like so: 

Lemma S_equal_vectors {l n m} : (prod (vec A l) (vec A (S m + n))) = prod (vec A l) (vec A (m + S n)).

f_equal. f_equal.

unfold plus. auto.

Defined.

Hint Immediate S_equal_vectors.

Lemma S_generate_eq {l n m} (va : prod (vec A l) (vec A (S m + n))) : prod (vec A l) (vec A (m + S n)).

replace (vec A l * vec A (m + S n))%type with (vec A l * vec A (S m + n))%type.

trivial.

auto.

Defined.

Definition one_step {n m} (input : vec A (S n)) (acc : vec A m) 

  : prod (vec A n) (vec A (S m)) :=

  match input in VectorDef.t _ n' return 

    match n' return Type with

      | O => unit

      | S n'' => prod (vec A n'') (vec A (S m)) 

    end with

    | vnil => tt

    | vcons x _ rest => (rest, vcons x acc)

  end.

Fixpoint vrev' {n m} (input : vec A n) (acc : vec A m) : prod (vec A 0) (vec A (m + n)) :=

  match n return vec A n -> prod (vec A 0) (vec A (m + n)) with

    | O => fun _ => plus_0_doesn't_matter (vnil A, acc)

    | S n' => fun input' : vec A (S n') =>

      let (i, a) := one_step input' acc in

        S_generate_eq (vrev' i a)

  end input.

End vrev.

Eval compute in vrev' (vcons 3 (vcons 2 (vcons 1 (vnil _)))) (vnil _).

> this has the same problem as the previous lemma, but there are many more matches.

The main question is how to define my helper lemmas so they don't try to match on a proof object. I also suspect that maybe my definition of vrev' is making things more complicated than they need to be. If there were a way to use an equality of types in the typechecking of vrev', I wouldn't have to apply the function that matches on the proof object -- but I don't know if that's possible.

Thanks,

Andrew