From 430b75f38f19db839baddfabb9204a64dc936ddf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 12:31:13 -0800 Subject: [PATCH] test(tests/lean): add version of the Nat library full of holes Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 46 +++++----- src/builtin/obj/Nat.olean | Bin 15338 -> 15338 bytes tests/lean/bare/NatHoles.lean | 165 ++++++++++++++++++++++++++++++++++ 3 files changed, 188 insertions(+), 23 deletions(-) create mode 100644 tests/lean/bare/NatHoles.lean diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 577019274..acd4c8ebf 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -34,50 +34,50 @@ Axiom PlusZero (a : Nat) : a + 0 = a. Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1. Axiom MulZero (a : Nat) : a * 0 = 0. Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. -Axiom Induction {P : Nat → Bool} (Hb : P 0) (Hi : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. +Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. Theorem ZeroNeOne : 0 ≠ 1 := Trivial. Theorem ZeroPlus (a : Nat) : 0 + a = a := Induction (show 0 + 0 = 0, Trivial) - (λ (n : Nat) (Hi : 0 + n = n), + (λ (n : Nat) (iH : 0 + n = n), calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n - ... = n + 1 : { Hi }) + ... = n + 1 : { iH }) a. Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 := Induction (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) ... = (a + 0) + 1 : { Symm (PlusZero a) }) - (λ (n : Nat) (Hi : (a + 1) + n = (a + n) + 1), + (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n - ... = ((a + n) + 1) + 1 : { Hi } + ... = ((a + n) + 1) + 1 : { iH } ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }) b. Theorem PlusComm (a b : Nat) : a + b = b + a := Induction (calc a + 0 = a : PlusZero a ... = 0 + a : Symm (ZeroPlus a)) - (λ (n : Nat) (Hi : a + n = n + a), + (λ (n : Nat) (iH : a + n = n + a), calc a + (n + 1) = (a + n) + 1 : PlusSucc a n - ... = (n + a) + 1 : { Hi } + ... = (n + a) + 1 : { iH } ... = (n + 1) + a : Symm (SuccPlus n a)) b. Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c := Induction (calc 0 + (b + c) = b + c : ZeroPlus (b + c) ... = (0 + b) + c : { Symm (ZeroPlus b) }) - (λ (n : Nat) (Hi : n + (b + c) = (n + b) + c), + (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) - ... = ((n + b) + c) + 1 : { Hi } + ... = ((n + b) + c) + 1 : { iH } ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }) a. Theorem ZeroMul (a : Nat) : 0 * a = 0 := Induction (show 0 * 0 = 0, Trivial) - (λ (n : Nat) (Hi : 0 * n = 0), + (λ (n : Nat) (iH : 0 * n = 0), calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n - ... = 0 + 0 : { Hi } + ... = 0 + 0 : { iH } ... = 0 : Trivial) a. @@ -85,9 +85,9 @@ Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b := Induction (calc (a + 1) * 0 = 0 : MulZero (a + 1) ... = a * 0 : Symm (MulZero a) ... = a * 0 + 0 : Symm (PlusZero (a * 0))) - (λ (n : Nat) (Hi : (a + 1) * n = a * n + n), + (λ (n : Nat) (iH : (a + 1) * n = a * n + n), calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n - ... = a * n + n + (a + 1) : { Hi } + ... = a * n + n + (a + 1) : { iH } ... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 ... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) } ... = a * n + (a + n) + 1 : { PlusComm n a } @@ -98,24 +98,24 @@ Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b Theorem OneMul (a : Nat) : 1 * a = a := Induction (show 1 * 0 = 0, Trivial) - (λ (n : Nat) (Hi : 1 * n = n), + (λ (n : Nat) (iH : 1 * n = n), calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n - ... = n + 1 : { Hi }) + ... = n + 1 : { iH }) a. Theorem MulOne (a : Nat) : a * 1 = a := Induction (show 0 * 1 = 0, Trivial) - (λ (n : Nat) (Hi : n * 1 = n), + (λ (n : Nat) (iH : n * 1 = n), calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 - ... = n + 1 : { Hi }) + ... = n + 1 : { iH }) a. Theorem MulComm (a b : Nat) : a * b = b * a := Induction (calc a * 0 = 0 : MulZero a ... = 0 * a : Symm (ZeroMul a)) - (λ (n : Nat) (Hi : a * n = n * a), + (λ (n : Nat) (iH : a * n = n * a), calc a * (n + 1) = a * n + a : MulSucc a n - ... = n * a + a : { Hi } + ... = n * a + a : { iH } ... = (n + 1) * a : Symm (SuccMul n a)) b. @@ -125,9 +125,9 @@ Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c ... = 0 + 0 : Trivial ... = 0 * b + 0 : { Symm (ZeroMul b) } ... = 0 * b + 0 * c : { Symm (ZeroMul c) }) - (λ (n : Nat) (Hi : n * (b + c) = n * b + n * c), + (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) - ... = n * b + n * c + (b + c) : { Hi } + ... = n * b + n * c + (b + c) : { iH } ... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c ... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } ... = n * b + (b + n * c) + c : { PlusComm (n * c) b } @@ -147,9 +147,9 @@ Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c := Induction (calc 0 * (b * c) = 0 : ZeroMul (b * c) ... = 0 * c : Symm (ZeroMul c) ... = (0 * b) * c : { Symm (ZeroMul b) }) - (λ (n : Nat) (Hi : n * (b * c) = n * b * c), + (λ (n : Nat) (iH : n * (b * c) = n * b * c), calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) - ... = n * b * c + (b * c) : { Hi } + ... = n * b * c + (b * c) : { iH } ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) ... = (n + 1) * b * c : { Symm (SuccMul n b) }) a. diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 44c6d2416cce9061c15c760f98fabaf7df387a19..78e095058851836d9dce7618c73e6b94f001e9bc 100644 GIT binary patch delta 168 zcmaD={;GV#Ru-mAkImazVi`fS7~35t=1dQU$!mnAHw$obgCr+AGK)>_;L+Y3$7{h1 z;frrxFOUnCOH>e_TqnY}*;(`&L}RX)^k#F3yBr{ei3-Y_Efv=?f=v`q5uL=sHrZc^ jeKWW6Pq^4-8PyUNn1adi7Hpf>Y0l(>32ctH=w=20;`=b7 delta 168 zcmaD={;GV#Ru(3Y%+1?bVi`fS7~35tW{*sU$!mnAHw$obgCr+AGK)>_;L+Y3$7{h1 z;frrxFOUnCOH>e_TqnY}*;(`&L}RX)^k#F3yBr{ei3-Y_Efv=?f=v`q5uL=sHrZc^ jeKWW6Pq^4-8PyUNn1adi7Hpf>Y0l(>32ctH=w=20;cqaa diff --git a/tests/lean/bare/NatHoles.lean b/tests/lean/bare/NatHoles.lean new file mode 100644 index 000000000..b0617a487 --- /dev/null +++ b/tests/lean/bare/NatHoles.lean @@ -0,0 +1,165 @@ +(* + Nat library full of "holes". + We provide only the proof skeletons, and let Lean infer the rest. +*) +Import kernel. + +Variable Nat : Type. +Alias ℕ : Nat. + +Namespace Nat. +Builtin numeral. + +Builtin add : Nat → Nat → Nat. +Infixl 65 + : add. + +Builtin mul : Nat → Nat → Nat. +Infixl 70 * : mul. + +Builtin le : Nat → Nat → Bool. +Infix 50 <= : le. +Infix 50 ≤ : le. + +Definition ge (a b : Nat) := b ≤ a. +Infix 50 >= : ge. +Infix 50 ≥ : ge. + +Definition lt (a b : Nat) := ¬ (a ≥ b). +Infix 50 < : lt. + +Definition gt (a b : Nat) := ¬ (a ≤ b). +Infix 50 > : gt. + +Definition id (a : Nat) := a. +Notation 55 | _ | : id. + +Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b +Axiom PlusZero (a : Nat) : a + 0 = a. +Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1. +Axiom MulZero (a : Nat) : a * 0 = 0. +Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. +Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. + +Theorem ZeroNeOne : 0 ≠ 1 := Trivial. + +Theorem ZeroPlus (a : Nat) : 0 + a = a +:= Induction (show 0 + 0 = 0, Trivial) + (λ (n : Nat) (iH : 0 + n = n), + calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc _ _ + ... = n + 1 : { iH }) + a. + +Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 +:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero _ + ... = (a + 0) + 1 : { Symm (PlusZero _) }) + (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc _ _ + ... = ((a + n) + 1) + 1 : { iH } + ... = (a + (n + 1)) + 1 : { Symm (PlusSucc _ _) }) + b. + +Theorem PlusComm (a b : Nat) : a + b = b + a +:= Induction (calc a + 0 = a : PlusZero a + ... = 0 + a : Symm (ZeroPlus a)) + (λ (n : Nat) (iH : a + n = n + a), + calc a + (n + 1) = (a + n) + 1 : PlusSucc _ _ + ... = (n + a) + 1 : { iH } + ... = (n + 1) + a : Symm (SuccPlus _ _)) + b. + +Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c +:= Induction (calc 0 + (b + c) = b + c : ZeroPlus _ + ... = (0 + b) + c : { Symm (ZeroPlus _) }) + (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus _ _ + ... = ((n + b) + c) + 1 : { iH } + ... = ((n + b) + 1) + c : Symm (SuccPlus _ _) + ... = ((n + 1) + b) + c : { Symm (SuccPlus _ _) }) + a. + +Theorem ZeroMul (a : Nat) : 0 * a = 0 +:= Induction (show 0 * 0 = 0, Trivial) + (λ (n : Nat) (iH : 0 * n = 0), + calc 0 * (n + 1) = (0 * n) + 0 : MulSucc _ _ + ... = 0 + 0 : { iH } + ... = 0 : Trivial) + a. + +Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b +:= Induction (calc (a + 1) * 0 = 0 : MulZero _ + ... = a * 0 : Symm (MulZero _) + ... = a * 0 + 0 : Symm (PlusZero _)) + (λ (n : Nat) (iH : (a + 1) * n = a * n + n), + calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc _ _ + ... = a * n + n + (a + 1) : { iH } + ... = a * n + n + a + 1 : PlusAssoc _ _ _ + ... = a * n + (n + a) + 1 : { Symm (PlusAssoc _ _ _) } + ... = a * n + (a + n) + 1 : { PlusComm _ _ } + ... = a * n + a + n + 1 : { PlusAssoc _ _ _ } + ... = a * (n + 1) + n + 1 : { Symm (MulSucc _ _) } + ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc _ _ _)) + b. + +Theorem OneMul (a : Nat) : 1 * a = a +:= Induction (show 1 * 0 = 0, Trivial) + (λ (n : Nat) (iH : 1 * n = n), + calc 1 * (n + 1) = 1 * n + 1 : MulSucc _ _ + ... = n + 1 : { iH }) + a. + +Theorem MulOne (a : Nat) : a * 1 = a +:= Induction (show 0 * 1 = 0, Trivial) + (λ (n : Nat) (iH : n * 1 = n), + calc (n + 1) * 1 = n * 1 + 1 : SuccMul _ _ + ... = n + 1 : { iH }) + a. + +Theorem MulComm (a b : Nat) : a * b = b * a +:= Induction (calc a * 0 = 0 : MulZero a + ... = 0 * a : Symm (ZeroMul a)) + (λ (n : Nat) (iH : a * n = n * a), + calc a * (n + 1) = a * n + a : MulSucc _ _ + ... = n * a + a : { iH } + ... = (n + 1) * a : Symm (SuccMul _ _)) + b. + + +Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c +:= Induction (calc 0 * (b + c) = 0 : ZeroMul _ + ... = 0 + 0 : Trivial + ... = 0 * b + 0 : { Symm (ZeroMul _) } + ... = 0 * b + 0 * c : { Symm (ZeroMul _) }) + (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), + calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul _ _ + ... = n * b + n * c + (b + c) : { iH } + ... = n * b + n * c + b + c : PlusAssoc _ _ _ + ... = n * b + (n * c + b) + c : { Symm (PlusAssoc _ _ _) } + ... = n * b + (b + n * c) + c : { PlusComm _ _ } + ... = n * b + b + n * c + c : { PlusAssoc _ _ _ } + ... = (n + 1) * b + n * c + c : { Symm (SuccMul _ _) } + ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc _ _ _) + ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul _ _) }) + a. + +Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c +:= calc (a + b) * c = c * (a + b) : MulComm _ _ + ... = c * a + c * b : Distribute _ _ _ + ... = a * c + c * b : { MulComm _ _ } + ... = a * c + b * c : { MulComm _ _}. + +Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c +:= Induction (calc 0 * (b * c) = 0 : ZeroMul _ + ... = 0 * c : Symm (ZeroMul _) + ... = (0 * b) * c : { Symm (ZeroMul _) }) + (λ (n : Nat) (iH : n * (b * c) = n * b * c), + calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul _ _ + ... = n * b * c + (b * c) : { iH } + ... = (n * b + b) * c : Symm (Distribute2 _ _ _) + ... = (n + 1) * b * c : { Symm (SuccMul _ _) }) + a. + +SetOpaque ge true. +SetOpaque lt true. +SetOpaque gt true. +SetOpaque id true. +EndNamespace. \ No newline at end of file