From d72b165db402d98cb47284d9531a4a0124f5f7b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jan 2014 17:19:12 -0800 Subject: [PATCH] feat(builtin/Nat): cleanup and add PlusAssoc Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 47 ++++++++++++++++++++++++++++---------------- 1 file changed, 30 insertions(+), 17 deletions(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 9f7c1ba2d..deba26840 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -31,25 +31,24 @@ 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. +Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b +Axiom Induction {P : Nat → Bool} (Hb : P 0) (Hi : Π (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)) + (λ (n : Nat) (Hi : 0 + n = n), + let L1 : 0 + (n + 1) = (0 + n) + 1 := PlusSucc 0 n + in show 0 + (n + 1) = n + 1, Subst L1 Hi) 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)) + (λ (n : Nat) (Hi : (a + 1) + n = (a + n) + 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 Hi, + L3 : (a + n) + 1 = a + (n + 1) := Symm (PlusSucc a n) + in show (a + 1) + (n + 1) = (a + (n + 1)) + 1, Subst L2 L3) b. Theorem PlusComm (a b : Nat) : a + b = b + a @@ -57,14 +56,28 @@ Theorem PlusComm (a b : Nat) : a + b = b + 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)) + (λ (n : Nat) (Hi : a + n = n + a), + let L1 : a + (n + 1) = (a + n) + 1 := PlusSucc a n, + L2 : a + (n + 1) = (n + a) + 1 := Subst L1 Hi, + L3 : (n + a) + 1 = (n + 1) + a := Symm (SuccPlus n a) + in show a + (n + 1) = (n + 1) + a, Trans L2 L3) b. +Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c +:= Induction (show 0 + (b + c) = (0 + b) + c, + Subst (ZeroPlus (b + c)) (Symm (ZeroPlus b))) + (λ (n : Nat) (Hi : n + (b + c) = (n + b) + c), + let L1 : (n + 1) + (b + c) = (n + (b + c)) + 1 := SuccPlus n (b + c), + L2 : (n + 1) + (b + c) = ((n + b) + c) + 1 := Subst L1 Hi, + L3 : ((n + b) + 1) + c = ((n + b) + c) + 1 := SuccPlus (n + b) c, + L4 : (n + b) + 1 = (n + 1) + b := Symm (SuccPlus n b), + L5 : ((n + 1) + b) + c = ((n + b) + c) + 1 := Subst L3 L4, + L6 : ((n + b) + c) + 1 = ((n + 1) + b) + c := Symm L5 + in show (n + 1) + (b + c) = ((n + 1) + b) + c, Trans L2 L6) + a. + +Theorem ZeroNeOne : 0 ≠ 1 := Trivial. + SetOpaque ge true. SetOpaque lt true. SetOpaque gt true.