# Library rea

Require Import ssreflect ssrbool.

Set Implicit Arguments.

Unset Strict Implicit.

Import Prenex Implicits.

Set Implicit Arguments.

Unset Strict Implicit.

Import Prenex Implicits.

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:
Wait, what, natural numbers?? W00t!

type isNat = | IsNat_O | IsNat_S of isNat

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.

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).

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".

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.
In other words, we have (artificially) decluttered our Pi-type in
terms of intersection and implication.

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

Extraction plus_isNat.

The extraction gives:
Or, after simplification:
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!

(* 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

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