# 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!