Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Evaluation with equality proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Evaluation with equality proofs


Chronological Thread 
  • From: Andrew Rodriguez <amr1 AT andrew.cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Evaluation with equality proofs
  • Date: Fri, 24 Jan 2014 09:28:03 -0800

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




Archive powered by MHonArc 2.6.18.

Top of Page