refactor(builtin/Nat): cleanup all proofs using calculational proof style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
e714bd7982
commit
307099b1cb
2 changed files with 65 additions and 83 deletions
|
|
@ -41,135 +41,117 @@ Theorem ZeroNeOne : 0 ≠ 1 := Trivial.
|
||||||
Theorem ZeroPlus (a : Nat) : 0 + a = a
|
Theorem ZeroPlus (a : Nat) : 0 + a = a
|
||||||
:= Induction (show 0 + 0 = 0, Trivial)
|
:= Induction (show 0 + 0 = 0, Trivial)
|
||||||
(λ (n : Nat) (Hi : 0 + n = n),
|
(λ (n : Nat) (Hi : 0 + n = n),
|
||||||
let L1 : 0 + (n + 1) = (0 + n) + 1 := PlusSucc 0 n
|
calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n
|
||||||
in show 0 + (n + 1) = n + 1, Subst L1 Hi)
|
... = n + 1 : { Hi })
|
||||||
a.
|
a.
|
||||||
|
|
||||||
Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
|
Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
|
||||||
:= Induction (show (a + 1) + 0 = (a + 0) + 1,
|
:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1)
|
||||||
(Subst (PlusZero (a + 1)) (Symm (PlusZero a))))
|
... = (a + 0) + 1 : { Symm (PlusZero a) })
|
||||||
(λ (n : Nat) (Hi : (a + 1) + n = (a + n) + 1),
|
(λ (n : Nat) (Hi : (a + 1) + n = (a + n) + 1),
|
||||||
let L1 : (a + 1) + (n + 1) = ((a + 1) + n) + 1 := PlusSucc (a + 1) n,
|
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n
|
||||||
L2 : (a + 1) + (n + 1) = ((a + n) + 1) + 1 := Subst L1 Hi,
|
... = ((a + n) + 1) + 1 : { Hi }
|
||||||
L3 : (a + n) + 1 = a + (n + 1) := Symm (PlusSucc a n)
|
... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) })
|
||||||
in show (a + 1) + (n + 1) = (a + (n + 1)) + 1, Subst L2 L3)
|
|
||||||
b.
|
b.
|
||||||
|
|
||||||
Theorem PlusComm (a b : Nat) : a + b = b + a
|
Theorem PlusComm (a b : Nat) : a + b = b + a
|
||||||
:= Induction (show a + 0 = 0 + a,
|
:= Induction (calc a + 0 = a : PlusZero a
|
||||||
let L1 : a + 0 = a := PlusZero a,
|
... = 0 + a : Symm (ZeroPlus a))
|
||||||
L2 : a = 0 + a := Symm (ZeroPlus a)
|
|
||||||
in Trans L1 L2)
|
|
||||||
(λ (n : Nat) (Hi : a + n = n + a),
|
(λ (n : Nat) (Hi : a + n = n + a),
|
||||||
let L1 : a + (n + 1) = (a + n) + 1 := PlusSucc a n,
|
calc a + (n + 1) = (a + n) + 1 : PlusSucc a n
|
||||||
L2 : a + (n + 1) = (n + a) + 1 := Subst L1 Hi,
|
... = (n + a) + 1 : { Hi }
|
||||||
L3 : (n + a) + 1 = (n + 1) + a := Symm (SuccPlus n a)
|
... = (n + 1) + a : Symm (SuccPlus n a))
|
||||||
in show a + (n + 1) = (n + 1) + a, Trans L2 L3)
|
|
||||||
b.
|
b.
|
||||||
|
|
||||||
Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c
|
Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c
|
||||||
:= Induction (show 0 + (b + c) = (0 + b) + c,
|
:= Induction (calc 0 + (b + c) = b + c : ZeroPlus (b + c)
|
||||||
Subst (ZeroPlus (b + c)) (Symm (ZeroPlus b)))
|
... = (0 + b) + c : { Symm (ZeroPlus b) })
|
||||||
(λ (n : Nat) (Hi : n + (b + c) = (n + b) + c),
|
(λ (n : Nat) (Hi : n + (b + c) = (n + b) + c),
|
||||||
let L1 : (n + 1) + (b + c) = (n + (b + c)) + 1 := SuccPlus n (b + c),
|
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c)
|
||||||
L2 : (n + 1) + (b + c) = ((n + b) + c) + 1 := Subst L1 Hi,
|
... = ((n + b) + c) + 1 : { Hi }
|
||||||
L3 : ((n + b) + 1) + c = ((n + b) + c) + 1 := SuccPlus (n + b) c,
|
... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c)
|
||||||
L4 : (n + b) + 1 = (n + 1) + b := Symm (SuccPlus n b),
|
... = ((n + 1) + b) + c : { show (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.
|
a.
|
||||||
|
|
||||||
Theorem ZeroMul (a : Nat) : 0 * a = 0
|
Theorem ZeroMul (a : Nat) : 0 * a = 0
|
||||||
:= Induction (show 0 * 0 = 0, Trivial)
|
:= Induction (show 0 * 0 = 0, Trivial)
|
||||||
(λ (n : Nat) (Hi : 0 * n = 0),
|
(λ (n : Nat) (Hi : 0 * n = 0),
|
||||||
let L1 : 0 * (n + 1) = (0 * n) + 0 := MulSucc 0 n,
|
calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n
|
||||||
L2 : 0 * (n + 1) = 0 + 0 := Subst L1 Hi
|
... = 0 + 0 : { Hi }
|
||||||
in show 0 * (n + 1) = 0, L2)
|
... = 0 : Trivial)
|
||||||
a.
|
a.
|
||||||
|
|
||||||
Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
|
Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
|
||||||
:= Induction (show (a + 1) * 0 = a * 0 + 0,
|
:= Induction (calc (a + 1) * 0 = 0 : MulZero (a + 1)
|
||||||
Trans (MulZero (a + 1)) (Symm (Subst (PlusZero (a * 0)) (MulZero a))))
|
... = a * 0 : Symm (MulZero a)
|
||||||
|
... = a * 0 + 0 : Symm (PlusZero (a * 0)))
|
||||||
(λ (n : Nat) (Hi : (a + 1) * n = a * n + n),
|
(λ (n : Nat) (Hi : (a + 1) * n = a * n + n),
|
||||||
let L1 : (a + 1) * (n + 1) = (a + 1) * n + (a + 1) := MulSucc (a + 1) n,
|
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n
|
||||||
L2 : (a + 1) * (n + 1) = a * n + n + (a + 1) := Subst L1 Hi,
|
... = a * n + n + (a + 1) : { Hi }
|
||||||
L3 : a * n + n + (a + 1) = a * n + n + a + 1 := PlusAssoc (a * n + n) a 1,
|
... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1
|
||||||
L4 : a * n + n + a = a * n + (n + a) := Symm (PlusAssoc (a * n) n a),
|
... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) }
|
||||||
L5 : a * n + n + (a + 1) = a * n + (n + a) + 1 := Subst L3 L4,
|
... = a * n + (a + n) + 1 : { PlusComm n a }
|
||||||
L6 : a * n + n + (a + 1) = a * n + (a + n) + 1 := Subst L5 (PlusComm n a),
|
... = a * n + a + n + 1 : { PlusAssoc (a * n) a n }
|
||||||
L7 : a * n + (a + n) = a * n + a + n := PlusAssoc (a * n) a n,
|
... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) }
|
||||||
L8 : a * n + n + (a + 1) = a * n + a + n + 1 := Subst L6 L7,
|
... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1))
|
||||||
L9 : a * n + a = a * (n + 1) := Symm (MulSucc a n),
|
|
||||||
L10 : a * n + n + (a + 1) = a * (n + 1) + n + 1 := Subst L8 L9,
|
|
||||||
L11 : a * (n + 1) + n + 1 = a * (n + 1) + (n + 1) := Symm (PlusAssoc (a * (n + 1)) n 1)
|
|
||||||
in show (a + 1) * (n + 1) = a * (n + 1) + (n + 1),
|
|
||||||
Trans (Trans L2 L10) L11)
|
|
||||||
b.
|
b.
|
||||||
|
|
||||||
Theorem OneMul (a : Nat) : 1 * a = a
|
Theorem OneMul (a : Nat) : 1 * a = a
|
||||||
:= Induction (show 1 * 0 = 0, Trivial)
|
:= Induction (show 1 * 0 = 0, Trivial)
|
||||||
(λ (n : Nat) (Hi : 1 * n = n),
|
(λ (n : Nat) (Hi : 1 * n = n),
|
||||||
let L1 : 1 * (n + 1) = 1 * n + 1 := MulSucc 1 n
|
calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n
|
||||||
in show 1 * (n + 1) = n + 1, Subst L1 Hi)
|
... = n + 1 : { Hi })
|
||||||
a.
|
a.
|
||||||
|
|
||||||
Theorem MulOne (a : Nat) : a * 1 = a
|
Theorem MulOne (a : Nat) : a * 1 = a
|
||||||
:= Induction (show 0 * 1 = 0, Trivial)
|
:= Induction (show 0 * 1 = 0, Trivial)
|
||||||
(λ (n : Nat) (Hi : n * 1 = n),
|
(λ (n : Nat) (Hi : n * 1 = n),
|
||||||
let L1 : (n + 1) * 1 = n * 1 + 1 := SuccMul n 1
|
calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1
|
||||||
in show (n + 1) * 1 = n + 1, Subst L1 Hi)
|
... = n + 1 : { Hi })
|
||||||
a.
|
a.
|
||||||
|
|
||||||
Theorem MulComm (a b : Nat) : a * b = b * a
|
Theorem MulComm (a b : Nat) : a * b = b * a
|
||||||
:= Induction (show a * 0 = 0 * a, Trans (MulZero a) (Symm (ZeroMul a)))
|
:= Induction (calc a * 0 = 0 : MulZero a
|
||||||
|
... = 0 * a : Symm (ZeroMul a))
|
||||||
(λ (n : Nat) (Hi : a * n = n * a),
|
(λ (n : Nat) (Hi : a * n = n * a),
|
||||||
let L1 : a * (n + 1) = a * n + a := MulSucc a n,
|
calc a * (n + 1) = a * n + a : MulSucc a n
|
||||||
L2 : (n + 1) * a = n * a + a := SuccMul n a,
|
... = n * a + a : { Hi }
|
||||||
L3 : (n + 1) * a = a * n + a := Subst L2 (Symm Hi)
|
... = (n + 1) * a : Symm (SuccMul n a))
|
||||||
in show a * (n + 1) = (n + 1) * a, Trans L1 (Symm L3))
|
|
||||||
b.
|
b.
|
||||||
|
|
||||||
|
|
||||||
Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c
|
Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c
|
||||||
:= Induction (let L1 : 0 * (b + c) = 0 := ZeroMul (b + c),
|
:= Induction (calc 0 * (b + c) = 0 : ZeroMul (b + c)
|
||||||
L2 : 0 * b + 0 * c = 0 + 0 := Subst (Subst (Refl (0 * b + 0 * c)) (ZeroMul b)) (ZeroMul c),
|
... = 0 + 0 : Trivial
|
||||||
L3 : 0 + 0 = 0 := Trivial
|
... = 0 * b + 0 : { Symm (ZeroMul b) }
|
||||||
in show 0 * (b + c) = 0 * b + 0 * c, Trans L1 (Symm (Trans L2 L3)))
|
... = 0 * b + 0 * c : { Symm (ZeroMul c) })
|
||||||
(λ (n : Nat) (Hi : n * (b + c) = n * b + n * c),
|
(λ (n : Nat) (Hi : n * (b + c) = n * b + n * c),
|
||||||
let L1 : (n + 1) * (b + c) = n * (b + c) + (b + c) := SuccMul n (b + c),
|
calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c)
|
||||||
L2 : (n + 1) * (b + c) = n * b + n * c + (b + c) := Subst L1 Hi,
|
... = n * b + n * c + (b + c) : { Hi }
|
||||||
L3 : n * b + n * c + (b + c) = n * b + n * c + b + c := PlusAssoc (n * b + n * c) b c,
|
... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c
|
||||||
L4 : n * b + n * c + b = n * b + (n * c + b) := Symm (PlusAssoc (n * b) (n * c) b),
|
... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) }
|
||||||
L5 : n * b + n * c + b = n * b + (b + n * c) := Subst L4 (PlusComm (n * c) b),
|
... = n * b + (b + n * c) + c : { PlusComm (n * c) b }
|
||||||
L6 : n * b + (b + n * c) = n * b + b + n * c := PlusAssoc (n * b) b (n * c),
|
... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) }
|
||||||
L7 : n * b + (b + n * c) = (n + 1) * b + n * c := Subst L6 (Symm (SuccMul n b)),
|
... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) }
|
||||||
L8 : n * b + n * c + b = (n + 1) * b + n * c := Trans L5 L7,
|
... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c)
|
||||||
L9 : n * b + n * c + (b + c) = (n + 1) * b + n * c + c := Subst L3 L8,
|
... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) })
|
||||||
L10 : (n + 1) * b + n * c + c = (n + 1) * b + (n * c + c) := Symm (PlusAssoc ((n + 1) * b) (n * c) c),
|
|
||||||
L11 : (n + 1) * b + n * c + c = (n + 1) * b + (n + 1) * c := Subst L10 (Symm (SuccMul n c)),
|
|
||||||
L12 : n * b + n * c + (b + c) = (n + 1) * b + (n + 1) * c := Trans L9 L11
|
|
||||||
in show (n + 1) * (b + c) = (n + 1) * b + (n + 1) * c,
|
|
||||||
Trans L2 L12)
|
|
||||||
a.
|
a.
|
||||||
|
|
||||||
Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
|
Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
|
||||||
:= let L1 : (a + b) * c = c * (a + b) := MulComm (a + b) c,
|
:= calc (a + b) * c = c * (a + b) : MulComm (a + b) c
|
||||||
L2 : c * (a + b) = c * a + c * b := Distribute c a b,
|
... = c * a + c * b : Distribute c a b
|
||||||
L3 : (a + b) * c = c * a + c * b := Trans L1 L2
|
... = a * c + c * b : { MulComm c a }
|
||||||
in Subst (Subst L3 (MulComm c a)) (MulComm c b).
|
... = a * c + b * c : { MulComm c b }.
|
||||||
|
|
||||||
Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c
|
Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c
|
||||||
:= Induction (let L1 : 0 * (b * c) = 0 := ZeroMul (b * c),
|
:= Induction (calc 0 * (b * c) = 0 : ZeroMul (b * c)
|
||||||
L2 : 0 * b * c = 0 * c := Subst (Refl (0 * b * c)) (ZeroMul b),
|
... = 0 * c : Symm (ZeroMul c)
|
||||||
L3 : 0 * c = 0 := ZeroMul c
|
... = (0 * b) * c : { Symm (ZeroMul b) })
|
||||||
in show 0 * (b * c) = 0 * b * c, Trans L1 (Symm (Trans L2 L3)))
|
|
||||||
(λ (n : Nat) (Hi : n * (b * c) = n * b * c),
|
(λ (n : Nat) (Hi : n * (b * c) = n * b * c),
|
||||||
let L1 : (n + 1) * (b * c) = n * (b * c) + (b * c) := SuccMul n (b * c),
|
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c)
|
||||||
L2 : (n + 1) * (b * c) = n * b * c + (b * c) := Subst L1 Hi,
|
... = n * b * c + (b * c) : { Hi }
|
||||||
L3 : n * b * c + (b * c) = (n * b + b) * c := Symm (Distribute2 (n * b) b c),
|
... = (n * b + b) * c : Symm (Distribute2 (n * b) b c)
|
||||||
L4 : n * b * c + (b * c) = (n + 1) * b * c := Subst L3 (Symm (SuccMul n b))
|
... = (n + 1) * b * c : { Symm (SuccMul n b) })
|
||||||
in show (n + 1) * (b * c) = (n + 1) * b * c, Trans L2 L4)
|
|
||||||
a.
|
a.
|
||||||
|
|
||||||
SetOpaque ge true.
|
SetOpaque ge true.
|
||||||
|
|
|
||||||
Binary file not shown.
Loading…
Reference in a new issue