Library rea

Require Import ssreflect ssrbool.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

This trick was explained to me by Marc Lasson. It goes back to Jean-Yves Girard and was later expanded by Parigot and others. Yes, I have to dig out the exact papers. Bear with me.

Inductive nat : Prop
    := O : nat
     | S : nat -> nat.
Remark: we're putting nat in Prop, weird heh?

Inductive isNat : nat -> Set
    := isNat_O : isNat O
     | isNat_S : forall n, isNat n -> isNat (S n).

Extraction isNat.
The extraction gives: 
    type isNat =
    | IsNat_O
    | IsNat_S of isNat
Wait, what, natural numbers?? W00t!

Definition LeibnizEqual {A : Set}(M N : A) : Type :=
  forall X : A -> Set, X N -> X M.

Notation "M =>= N" := (LeibnizEqual M N)
    (at level 100) : type_scope.

Now, let's implement plus.
Well, in fact, we are not going to implement plus. We are going to *specify* it with two axioms, plus_O and plus_S, and obtain plus as a realizer of the lemma stating that plus m n is a natural number, for m and n natural numbers.
The specification:
Axiom plus : nat -> nat -> nat.

Axiom plus_O : forall m, plus m O =>= m.
Axiom plus_S : forall m n, plus m (S n) =>= S (plus m n).

The realizers of plus_O and plus_S are trivial, because Leibniz equality is trivially realized by the identity function:
Extract Constant plus_O => "fun m -> m".
Extract Constant plus_S => "fun m -> m".

Look at the following lemma and think about its realizers: functions of type nat -> nat -> nat. Hmm, interesting.

Lemma plus_isNat :
  forall m n, isNat m -> isNat n -> isNat (plus m n).
Proof.
  move=> m n m_isNat n_isNat.
  elim: n_isNat=> [|n' n'_isNat m_plus_n'].
  *
    
    apply: plus_O.
    done.
  *
    
    apply: plus_S.
    apply: isNat_S.
    done.
Defined.
<- that's rather important
Remark: What is crucial here is the form of the lemma.
  • We are doing a \forall on m and n in Prop. Prop being contractible, this \forall is not your usual Pi-type: it's a (beautiful) System-F-ish intersection type!
  • We then pass the extra-arguments isNat m and isNat n, using an exponential: that's a (beautiful) System-F-ish implication!
In other words, we have (artificially) decluttered our Pi-type in terms of intersection and implication.

Extraction plus_isNat.
The extraction gives: 
    (* val plus_isNat : isNat -> isNat -> isNat *)

    let plus_isNat m_isNat n_isNat =
      let _evar_0_ = plus_O m_isNat in
      let _evar_0_0 = fun n'_isNat m_plus_n' ->
        let _evar_0_0 = IsNat_S m_plus_n' in plus_S _evar_0_0
      in
      let rec f = function
      | IsNat_O -> _evar_0_
      | IsNat_S i0 -> _evar_0_0 i0 (f i0)
      in f n_isNat
Or, after simplification: 
    let plus_isNat (m_isNat : nat)(n_isNat : nat) =
      let rec f = function
      | IsNat_0 -> m_isNat
      | IsNat_S n -> isNat_S (f n)
      in f n_isNat
Wait, but it's really the addition function?!
Remark: I've pedantically written the proof of plus_isNat because I'm a n00b. I suspect that, with some Coq magic, one could get a mixture of induction and eauto to prove the damned thing almost automatically. Yet, the extracted code would be the same: addition!