From aa009b6b05b26279bdbac8efd1c032e51785054f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2014 15:53:53 -0800
Subject: [PATCH] feat(builtin/Nat): add basic axioms and theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/Nat.lean      |  38 ++++++++++++++++++++++++++++++++++++--
 src/builtin/obj/Nat.olean | Bin 742 -> 4135 bytes
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index e4959bd42..9f7c1ba2d 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -4,7 +4,6 @@ Variable Nat : Type.
 Alias ℕ : Nat.
 
 Namespace Nat.
-
 Builtin numeral.
 
 Builtin add : Nat → Nat → Nat.
@@ -30,9 +29,44 @@ Infix 50 >  : gt.
 Definition id (a : Nat) := a.
 Notation 55 | _ | : id.
 
+Axiom PlusZero (a : Nat)   : a + 0 = a.
+Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1.
+Axiom Induction {P : Nat -> Bool} (Hb : P 0) (Hi : Pi (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a.
+
+Theorem ZeroPlus (a : Nat) : 0 + a = a
+:= Induction (show 0 + 0 = 0, Trivial)
+             (fun (n : Nat) (H : 0 + n = n),
+                  (show 0 + (n + 1) = n + 1,
+                       let L1 : 0 + (n + 1) = (0 + n) + 1 := PlusSucc 0 n
+                       in Subst L1 H))
+             a.
+
+Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
+:= Induction (show (a + 1) + 0 = (a + 0) + 1,
+                   (Subst (PlusZero (a + 1)) (Symm (PlusZero a))))
+             (fun (n : Nat) (H : (a + 1) + n = (a + n) + 1),
+                  (show (a + 1) + (n + 1) = (a + (n + 1)) + 1,
+                        let L1 : (a + 1) + (n + 1) = ((a + 1) + n) + 1 := PlusSucc (a + 1) n,
+                            L2 : (a + 1) + (n + 1) = ((a + n) + 1) + 1 := Subst L1 H,
+                            L3 : (a + n) + 1 = a + (n + 1)             := Symm (PlusSucc a n)
+                         in Subst L2 L3))
+             b.
+
+Theorem PlusComm (a b : Nat) : a + b = b + a
+:= Induction (show a + 0 = 0 + a,
+                   let L1 : a + 0 = a  := PlusZero a,
+                       L2 : a = 0 + a  := Symm (ZeroPlus a)
+                   in Trans L1 L2)
+             (fun (n : Nat) (H : a + n = n + a),
+                  (show a + (n + 1) = (n + 1) + a,
+                        let L1 : a + (n + 1) = (a + n) + 1 := PlusSucc a n,
+                            L2 : a + (n + 1) = (n + a) + 1 := Subst L1 H,
+                            L3 : (n + a) + 1 = (n + 1) + a := Symm (SuccPlus n a)
+                        in Trans L2 L3))
+             b.
+
 SetOpaque ge true.
 SetOpaque lt true.
 SetOpaque gt true.
 SetOpaque id true.
-
 EndNamespace.
\ No newline at end of file
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index 81772f9907cbd6a3000453f4020d7a4600e08f10..8bdb60f0563a030b69f3ed7217cb46ae50f6be6d 100644
GIT binary patch
literal 4135
zcmbtYU2j!I6rGv-WqH67Fq%MOLTy9D8(Ksf3=mtCl*AxO8z0n!oc12z<er{W?gy5H
z#F!WiFTNQ6LG_Iv0^xzbV4qBU^ba^|&CH!SAGcn$q0>FH_pH5U&))l-L!QP_b}va|
zVSnVU-MxG;68(6P#i{r*8VGee8i|e+YC9i^wKR!_LLL6_i%@3E`Z!5PNwyh}L?hFd
z%fha3dN=Cz#O-_(jgmaW2C2?-=NcxBg6Zx!Et$Sg)0;4D7ECqaBIwm?LTamvFl`l8
zhtCcI-KX(A(d3ct$D*wwcZ{~$#$LUo*7H2oD45N0iQ+Me?_q4g6)|Pe)pg5)p?RZ3
z@$lKNhKJRX34l83sE)}A>gfATh$kq{Q(RCg)3+f=XC8DUITh(#4g4J!-rxONe`kQ)
zp_5Y(&rp1e;sVA~{_u6)t_R*u2Huihcsc+r5&0d871~NY5&B<8YgZYmx5e7NXu`O2
zCmj#JiU)ZJxTsY8Pzc34H34Z5)Mg{)0>b8aXD38(SAS^{PCmfU<xz<vy=W4A#X9lp
zCK~j&;>q61dgC3YeOuiL{kaTltBq~35OUQkiMGsqQf?RnMJw7i0>9Q}kjBP@*1D2$
z6meGnO1bsG#t`vC979HxgNLyr7;lWB`Fe@Ba#pm|KJmMi-B|vH+c?ar;e-6!ZoI!Y
zh=)V;0a@8%9Txv6wKYf{C6TU1L&8U<r8dMgkpJYl8rAB`oceraI`^u*SutY}QAt^+
z5d-<IYnz}g&ndMz-X7}G#?PMF3-KY;OasNc=wh)x^xt_V4Oo5e=a`BgCjl~v%jqOP
zP#xv`a20Y;3Au-Mry`nJ4wPKA=O+KlU~)ilmEt6=Fq?8Z56IB{R_n{u3Q(TUl6fA}
zoxomI<qUS+p5h!ST!J6b1rggQFn@vJ!cq6+y(){xEq)nO@oIriP6us`M}D=W)8z5)
zE{((i{=CHS!r7A#O<Vs^Gv1>k!fj?bP;%8${dZw)*j*mX1-k5{rnOBx)>fW}oXttq
zo`G@%Z9Pu0($#;lruw~g)8XJM`0Q{YH8$Z0zfBCz#O^I*Rb>N!f9I}>imTB7F<aWf
zO3oV?>_w-LC;ePcg**)nd#}`||M1Au^QEYI4J{Apl%~?J06KiohL%vRmd{AapFnlZ
zwNCIej*kpn8+J|oD=&LGZ7)*w@oa&^i%A$bvZ@VS&|MkFNsC2$y^-tk4IbRK#mfGo
z#;?AF5Wo{QcS6Ez;M1qLPH~n-3OLgzOPFew+Qx2E!^^faF?*LMnNs(Z3^!3O^r}*E
z$vznxasjvsa!2-!T9Ywv8z^7-vw=NNE=oU6w+2x*giRsYnC?&E#5Nr*$)7kUISho*
zuQ`*~vD%joSpL6I*0eoyGJiL&W0K&M*AVKeTgp&uOb#!sBcmu?L|C9r5AM2F8JvM|
zeXyn^!O^t60E>%E;3<!N7?iq$eCYwSR>;>dnk3-St%@gY6}q)Yb6tu~gLHF|2rS`|
z?;w_3Q6>L^{<#V9N2F#Po4D|+)`7xVxgXgRdQb+gtu5tivlytb`X^B^lsnHCdy#$n
c*B`yo&-909Fw>uf!AyU)$<MOhP5kG;-(=ui+W-In

delta 11
ScmZ3k@QiiCGN#GT`5gcr(*)E2