coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Daniel Schepler, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
Archive powered by MHonArc 2.6.18.