The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 11/19/2013 08:27 PM, David MENTRÉ wrote:
>   * Curry-Howard isomorphism: a very simple Coq theorem (on Boolean or
> integers) with associated proof, from which I could also generate OCaml
> code and show the Coq type.
What about something simple like:

Lemma minus : forall x y : nat, y <= x -> { z | x = y + z }.
Proof.
  induction x as [|x IH].
  { exists 0. omega. }
  intros [|y] ?.
  { exists (S x). omega. }
  destruct (IH y) as [z Hz]. omega. exists z. omega.
Defined.

Extraction minus.
(*
(** val minus : nat -> nat -> nat **)

let rec minus n y =
  match n with
  | O -> O
  | S n0 ->
    (match y with
     | O -> S n0
     | S y0 -> minus n0 y0)
*)