Can this be done with Coq? This can be done with any prover. Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1

Can this be done with Coq? This can be done with any prover. Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1 :: A -> B and f2 :: A -> B, say one slow and simple (f1), one fast and complicated (f2), then you can verify that f2 does what it is supposed to do in two steps: 1. Show that for all a in A we have f1 a == f2 a. 2. Show that f1 meets the specification. If you trust that f1 does what it is supposed to do, then you can skip (2).