1
$\begingroup$

I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma containing a cast with an explicit proof, I want to able to rewrite a statement that is equivalent. Is there someway I could either do this manually or automatically?

$\endgroup$

1 Answer 1

1
$\begingroup$

It is indeed possible, but not so easy to build infrastructure to do.

I'd suggest you have a look at MathComp's subType class, and how it organizes the set of irrelevant proofs.

To work with Vector.t effectively though, you'll need to master ssreflect rewrite, IMHO regular rewrite is not powerful enough as to properly be used as you'll have to perform complex subterm selection.

Note that we don't recommend using Vector.t anymore, see this PR for more info upstream: https://github.com/coq/coq/pull/18032

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.