/-- A Caesar shift by `k` on letter numbers (A = 0, …, Z = 25): move `k` places on, wrappinground from 25 back to 0. -/def shift (k n : Nat) : Nat := (n + k) % 26
wrap_aroundtheoremProved here from basic factsNo axioms
wrap_aroundLean 4Proved here from basic factsFormally verified
/-- Shifting by 3 wraps round the end of the alphabet: X (23) → A (0), Y (24) → B (1),Z (25) → C (2). And M (12) → P (15) needs no wrapping. -/theorem wrap_around : shift 3 23 = 0 ∧ shift 3 24 = 1 ∧ shift 3 25 = 2 ∧ shift 3 12 = 15 := by decide
shift_ltLean 4Applies a library theoremFormally verified
/-- A shift always lands on one of the 26 letters: a remainder on division by 26 is lessthan 26. This applies core Lean's `Nat.mod_lt`. -/theorem shift_lt (k n : Nat) : shift k n < 26 := Nat.mod_lt _ (by decide)
shift_undotheoremProved here from basic factspropext, Quot.sound
shift_undoLean 4Proved here from basic factsFormally verified
/-- **A shift forward by `k` is undone by a shift forward by `26 − k`**: together they move26 places, once round the whole wheel. -/theorem shift_undo (k n : Nat) (hk : k ≤ 26) (hn : n < 26) : shift (26 - k) (shift k n) = n := by unfold shift omega
shift_shifttheoremProved here from basic factspropext, Quot.sound
shift_shiftLean 4Proved here from basic factsFormally verified
/-- Two shifts, one after the other, are one shift: by `a`, then by `b`, is the same as by`a + b`. (So the order of two shifts does not matter.) -/theorem shift_shift (a b n : Nat) : shift b (shift a n) = shift (a + b) n := by unfold shift omega
shift_twenty_sixtheoremProved here from basic factspropext, Quot.sound
shift_twenty_sixLean 4Proved here from basic factsFormally verified
/-- Shifting by 26 changes nothing: it goes once round the wheel. -/theorem shift_twenty_six (n : Nat) (hn : n < 26) : shift 26 n = n := by unfold shift omega
shift_add_twenty_sixtheoremProved here from basic factspropext, Quot.sound
shift_add_twenty_sixLean 4Proved here from basic factsFormally verified
/-- Shifting by `k + 26` is the same as shifting by `k`. So every shift is one of the shifts0, 1, …, 25: there are **at most** 26 different shifts. -/theorem shift_add_twenty_six (k n : Nat) : shift (k + 26) n = shift k n := by unfold shift omega
shifts_differtheoremProved here from basic factspropext, Quot.sound
shifts_differLean 4Proved here from basic factsFormally verified
/-- The shifts 0, 1, …, 25 are all different: shift `k` sends A (0) to letter number `k`. Sothere are **exactly** 26 shifts — and only 25 that change the message. -/theorem shifts_differ (k : Nat) (hk : k < 26) : shift k 0 = k := by unfold shift omega
shift_injectivetheoremProved here from basic factspropext, Quot.sound
shift_injectiveLean 4Proved here from basic factsFormally verified
/-- A shift never sends two different letters to the same letter. That is why a coded messagecan always be decoded. -/theorem shift_injective (k n m : Nat) (hn : n < 26) (hm : m < 26) (h : shift k n = shift k m) : n = m := by unfold shift at h omega
/-- Shift one character. Computers store `A` as the number 65, …, `Z` as 90. A capital letteris turned into its letter number (subtract 65), shifted, and turned back (add 65); spaces andother characters are left as they are. -/def shiftChar (k : Nat) (c : Char) : Char := if 65 ≤ c.toNat ∧ c.toNat ≤ 90 then Char.ofNat ((c.toNat - 65 + k) % 26 + 65) else c
/-- The Caesar cipher with key `k`: shift every letter of the message by `k`. -/def caesar (k : Nat) (message : String) : String := String.ofList (message.toList.map (shiftChar k))
try_every_shifttheoremProved here from basic factspropext, Classical.choice, Quot.sound
try_every_shiftLean 4Proved here from basic factsFormally verified
/-- Breaking a Caesar cipher by trying every key: among the 26 shifts of WKLV LV IXQ, onereads THIS IS FUN. -/theorem try_every_shift : "THIS IS FUN" ∈ (List.range 26).map (fun k => caesar k "WKLV LV IXQ") := by decide
toNat_ofNat_smalltheoremProved here from basic factspropext
toNat_ofNat_smallLean 4Proved here from basic factsFormally verified
/-- Turning a small number into a character and back gives the same number. -/theorem toNat_ofNat_small (m : Nat) (h : m < 55296) : (Char.ofNat m).toNat = m := by have hv : m.isValidChar := Or.inl h simp [Char.ofNat, hv, Char.ofNatAux, Char.toNat]
shiftChar_undotheoremProved here from basic factspropext, Classical.choice, Quot.sound
shiftChar_undoLean 4Proved here from basic factsFormally verified
/-- Shifting a character by `k` and then by `26 − k` gives it back: for a capital letter by`shift_undo`, and any other character was never changed. -/theorem shiftChar_undo (k : Nat) (hk : k ≤ 26) (c : Char) : shiftChar (26 - k) (shiftChar k c) = c := by unfold shiftChar by_cases h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 · have e := toNat_ofNat_small ((c.toNat - 65 + k) % 26 + 65) (by omega) rw [ite_eq_left h, ite_eq_left (by rw [e]; omega)] apply Char.toNat_inj.mp rw [toNat_ofNat_small _ (by omega), e] omega · rw [ite_eq_right h, ite_eq_right h]
caesar_undotheoremProved here from basic factspropext, Classical.choice, Quot.sound
caesar_undoLean 4Proved here from basic factsFormally verified
/-- **Decoding undoes encoding, for every message and every key**: the Caesar cipher with key`26 − k` decodes the Caesar cipher with key `k`. -/theorem caesar_undo (k : Nat) (hk : k ≤ 26) (message : String) : caesar (26 - k) (caesar k message) = message := by unfold caesar rw [String.toList_ofList, List.map_map] have : (shiftChar (26 - k) ∘ shiftChar k) = id := funext (shiftChar_undo k hk) rw [this, List.map_id, String.ofList_toList]
substitution_keystheoremProved here from basic factsNo axioms
substitution_keysLean 4Proved here from basic factsFormally verified
/-- A substitution key chooses a code letter for A (26 choices), then for B (25 left), and soon: 26 × 25 × ⋯ × 1 keys — more than 400 million million million million. -/theorem substitution_keys : factorial 26 = 403291461126605635584000000 := by decide
/-- Check that a shift of 3 wraps X, Y and Z round to A, B and C.Hint: Lean can work out these remainders itself — try `decide`. -/theorem wrap_around : shift 3 23 = 0 ∧ shift 3 24 = 1 ∧ shift 3 25 = 2 ∧ shift 3 12 = 15 := by sorry
Show the compiled solution
wrap_aroundLean 4Proved here from basic factsFormally verified
/-- Shifting by 3 wraps round the end of the alphabet: X (23) → A (0), Y (24) → B (1),Z (25) → C (2). And M (12) → P (15) needs no wrapping. -/theorem wrap_around : shift 3 23 = 0 ∧ shift 3 24 = 1 ∧ shift 3 25 = 2 ∧ shift 3 12 = 15 := by decide
/-- Show that two shifts make one shift.Hint: `unfold shift` turns the goal into a statement about remainders; then `omega` canfinish it. -/theorem shift_shift (a b n : Nat) : shift b (shift a n) = shift (a + b) n := by sorry
Show the compiled solution
shift_shiftLean 4Proved here from basic factsFormally verified
/-- Two shifts, one after the other, are one shift: by `a`, then by `b`, is the same as by`a + b`. (So the order of two shifts does not matter.) -/theorem shift_shift (a b n : Nat) : shift b (shift a n) = shift (a + b) n := by unfold shift omega