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