The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 28/01/2016 17:15, Jonathan Leivent wrote:

> If the output of extraction
> from two extensionally-equivalent functions would behave differently in
> OCaml, then I would prefer that they are not treated within Coq as
> substitutionally identical.

But that is already the case, even without any functional extensionality!

Axiom g : nat -> nat -> nat.
Fixpoint f1 (n : nat) :=
  match n with S n => g (f1 n) (f1 n) | O => g O O end.
Fixpoint f2 (n : nat) :=
  match n with S n => let v := f2 n in g v v | O => g O O end.
Goal f1 = f2. reflexivity. Qed.

While f1 and f2 are convertible, their behavior is entirely different
when extracted to Ocaml. One performs an exponential number of calls to
g, the other one is only linear. Sure, you could devise an Ocaml
optimization so that f1 also has linear complexity once compiled. But
where do you set the limit of what a compiler is allowed to?

Best regards,

Guillaume