Grace/Cumulus/Combinatorics/Derangements.g17

Open in Workbench Download source

Imports

FallingBounds

Declarations

Source

1-- The derangement numbers 1, 0, 1, 2, 9, 44, …: the recurrence2-- d(n + 2) = (n + 1)(d(n + 1) + d(n)), the one-step recurrences3-- d(2n + 1) + 1 = (2n + 1) d(2n) and d(2n + 2) = (2n + 2) d(2n + 1) + 1,4-- positivity, monotonicity, and the comparison with n!5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.Derangements11import FallingBounds1213-- derangementAux(n, i, a, b) is the term n places after index i of a14-- sequence t with t(i) = a, t(i + 1) = b, and15-- t(k + 2) = (k + 1)(t(k + 1) + t(k)).16def derangementAux (n i a b : Nat) → Nat17  | zero, i, a, b => a18  | succ(k), i, a, b => derangementAux(k, i + 1, b, (i + 1) * (a + b))19  descends n2021def derangement (n : Nat) : Nat := derangementAux(n, 0, 1, 0)2223theorem derangementAux.zero (i a b : Nat)24  shows derangementAux(0, i, a, b) = a25proof26  simp [derangementAux]2728theorem derangementAux.succ (k i a b : Nat)29  shows derangementAux(k + 1, i, a, b) =30    derangementAux(k, i + 1, b, (i + 1) * (a + b))31proof32  have one : k + 1 = succ(k) := add.right_one with *33  rw one34  simp [derangementAux]3536theorem derangementAux.one (i a b : Nat)37  shows derangementAux(1, i, a, b) = b38proof39  simp [derangementAux]4041theorem derangementAux.two (i a b : Nat)42  shows derangementAux(2, i, a, b) = (i + 1) * (a + b)43proof44  simp [derangementAux]4546theorem derangementAux.closed (n : Nat)47  shows ∀ i, Nat(i) → ∀ a, Nat(a) → ∀ b, Nat(b) →48    Nat(derangementAux(n, i, a, b))49proof50  induction n51  | zero =>52    intros i iNat a aNat b bNat53    rw derangementAux.zero54    exact aNat55  | k + 1 using ih =>56    intros i iNat a aNat b bNat57    rw derangementAux.succ58    have nextNat : Nat(i + 1) by typecheck59    have productNat : Nat((i + 1) * (a + b)) by typecheck60    exact ih with i + 1, nextNat, b, bNat, (i + 1) * (a + b), productNat6162-- Every such sequence obeys the derangement recurrence.63theorem derangementAux.shift (n : Nat)64  shows ∀ i, Nat(i) → ∀ a, Nat(a) → ∀ b, Nat(b) →65    derangementAux(n + 2, i, a, b) =66    (i + n + 1) * (derangementAux(n + 1, i, a, b) + derangementAux(n, i, a, b))67proof68  induction n69  | zero =>70    intros i iNat a aNat b bNat71    have two : 0 + 2 = 2 by compute72    have one : 0 + 1 = 1 by compute73    rw [two, one, derangementAux.two, derangementAux.one, derangementAux.zero]74    have shape : i + 0 + 1 = i + 1 by ring75    rw shape76    ring77  | k + 1 using ih =>78    intros i iNat a aNat b bNat79    have shape : k + 1 + 2 = (k + 2) + 1 by ring80    have shape2 : k + 1 + 1 = k + 2 by ring81    rw [shape, shape2]82    have top := derangementAux.succ at k + 2, i, a, b83    have middle := derangementAux.succ at k + 1, i, a, b84    have last := derangementAux.succ at k, i, a, b85    rw shape2 at middle86    rw [top, middle, last]87    have iNat1 : Nat(i + 1) by typecheck88    have cNat : Nat((i + 1) * (a + b)) by typecheck89    have inner := ih with i + 1, iNat1, b, bNat, (i + 1) * (a + b), cNat90    rw inner91    have aux1 := derangementAux.closed at k + 192    have bNat1 := aux1 with i + 1, iNat1, b, bNat, (i + 1) * (a + b), cNat93    have aux0 := derangementAux.closed at k94    have bNat0 := aux0 with i + 1, iNat1, b, bNat, (i + 1) * (a + b), cNat95    ring9697theorem derangement.zero98  shows derangement(0) = 199proof100  compute101102theorem derangement.one103  shows derangement(1) = 0104proof105  compute106107theorem derangement.two108  shows derangement(2) = 1109proof110  compute111112theorem derangement.three113  shows derangement(3) = 2114proof115  compute116117theorem derangement.four118  shows derangement(4) = 9119proof120  compute121122theorem derangement.five123  shows derangement(5) = 44124proof125  compute126127theorem derangement.natural (n : Nat)128  shows Nat(derangement(n))129proof130  unfold derangement131  have zeroNat : Nat(0) by typecheck132  have oneNat : Nat(1) by typecheck133  exact derangementAux.closed at n with 0, zeroNat, 1, oneNat, 0, zeroNat134135theorem derangement.recurrence (n : Nat)136  shows derangement(n + 2) = (n + 1) * (derangement(n + 1) + derangement(n))137proof138  unfold derangement139  have zeroNat : Nat(0) by typecheck140  have oneNat : Nat(1) by typecheck141  have shift := derangementAux.shift at n with 0, zeroNat, 1, oneNat, 0, zeroNat142  have shape : 0 + n + 1 = n + 1 by ring143  rw shape at shift144  exact shift145146-- The one-step recurrences d(n + 1) = (n + 1) d(n) + (−1)^(n + 1), split by147-- the parity of n so that both sides stay natural.148theorem derangement.alternating_pair (n : Nat)149  shows derangement(2 * n + 1) + 1 = (2 * n + 1) * derangement(2 * n) ∧150    derangement(2 * n + 2) = (2 * n + 2) * derangement(2 * n + 1) + 1151proof152  induction n153  | zero =>154    constructor155    . compute156    . compute157  | k + 1 using ih =>158    have odd := ih.left159    have even := ih.right160    have shapeA : 2 * (k + 1) + 1 = 2 * k + 3 by ring161    have shapeB : 2 * (k + 1) = 2 * k + 2 by ring162    have shapeC : 2 * (k + 1) + 2 = 2 * k + 4 by ring163    rw [shapeA, shapeC, shapeB]164    have natA := derangement.natural at 2 * k165    have natB := derangement.natural at 2 * k + 1166    have natC := derangement.natural at 2 * k + 2167    have natD := derangement.natural at 2 * k + 3168    have stepOdd : derangement(2 * k + 3) + 1 =169        (2 * k + 3) * derangement(2 * k + 2)170      have step := derangement.recurrence at 2 * k + 1171      have three : 2 * k + 1 + 2 = 2 * k + 3 by ring172      have two : 2 * k + 1 + 1 = 2 * k + 2 by ring173      rw [three, two] at step174      rw [step, even]175      ring176    constructor177    . exact stepOdd178    . have step := derangement.recurrence at 2 * k + 2179      have four : 2 * k + 2 + 2 = 2 * k + 4 by ring180      have three : 2 * k + 2 + 1 = 2 * k + 3 by ring181      rw [four, three] at step182      rw step183      have reversed : (2 * k + 3) * derangement(2 * k + 2) =184          derangement(2 * k + 3) + 1185        symm186        exact stepOdd187      ring [reversed]188189theorem derangement.odd_succ (n : Nat)190  shows derangement(2 * n + 1) + 1 = (2 * n + 1) * derangement(2 * n)191proof192  have pair := derangement.alternating_pair at n193  exact pair.left194195theorem derangement.even_succ (n : Nat)196  shows derangement(2 * n + 2) = (2 * n + 2) * derangement(2 * n + 1) + 1197proof198  have pair := derangement.alternating_pair at n199  exact pair.right200201-- d(n + 1) ≤ (n + 1) d(n) + 1 and (n + 1) d(n) ≤ d(n + 1) + 1 for every n.202theorem derangement.succ_le (n : Nat)203  shows derangement(n + 1) ≤ (n + 1) * derangement(n) + 1204proof205  have alternatives := parity.exhaustive at n206  cases alternatives with even | odd207  . have iff := Even.iff_two_mul at n208    obtain ⟨k, kNat, shape⟩ := iff.forward with even209    rw shape210    have step := derangement.odd_succ at k211    have natA := derangement.natural at 2 * k212    have natB := derangement.natural at 2 * k + 1213    arith214  . have iff := Odd.iff_two_mul_add_one at n215    obtain ⟨k, kNat, shape⟩ := iff.forward with odd216    rw shape217    have step := derangement.even_succ at k218    have two : 2 * k + 1 + 1 = 2 * k + 2 by ring219    rw two220    have natB := derangement.natural at 2 * k + 1221    have natC := derangement.natural at 2 * k + 2222    arith223224theorem derangement.succ_ge (n : Nat)225  shows (n + 1) * derangement(n) ≤ derangement(n + 1) + 1226proof227  have alternatives := parity.exhaustive at n228  cases alternatives with even | odd229  . have iff := Even.iff_two_mul at n230    obtain ⟨k, kNat, shape⟩ := iff.forward with even231    rw shape232    have step := derangement.odd_succ at k233    have natA := derangement.natural at 2 * k234    have natB := derangement.natural at 2 * k + 1235    arith236  . have iff := Odd.iff_two_mul_add_one at n237    obtain ⟨k, kNat, shape⟩ := iff.forward with odd238    rw shape239    have step := derangement.even_succ at k240    have two : 2 * k + 1 + 1 = 2 * k + 2 by ring241    rw two242    have natB := derangement.natural at 2 * k + 1243    have natC := derangement.natural at 2 * k + 2244    arith245246theorem derangement.positive (n : Nat)247  shows 0 < derangement(n + 2)248proof249  induction n250  | zero =>251    have two : 0 + 2 = 2 by compute252    rw [two, derangement.two]253    arith254  | k + 1 using ih =>255    rw derangement.recurrence256    have shape : k + 1 + 1 = k + 2 by ring257    rw shape258    have natA := derangement.natural at k + 1259    have natC := derangement.natural at k + 2260    have coefficient : 0 < k + 2 by arith261    have sum : 0 < derangement(k + 2) + derangement(k + 1) by arith262    exact Less.mul_positive with coefficient, sum263264theorem derangement.ge_one (n : Nat)265  shows 1 ≤ derangement(n + 2)266proof267  have positive := derangement.positive at n268  have natural := derangement.natural at n + 2269  arith270271theorem derangement.monotone (n : Nat)272  shows derangement(n + 2) ≤ derangement(n + 3)273proof274  have step := derangement.recurrence at n + 1275  have shape : n + 1 + 2 = n + 3 by ring276  have shape2 : n + 1 + 1 = n + 2 by ring277  rw [shape, shape2] at step278  rw step279  have natA := derangement.natural at n + 1280  have natB := derangement.natural at n + 2281  have expand : (n + 2) * (derangement(n + 2) + derangement(n + 1)) =282    derangement(n + 2) + (n + 1) * derangement(n + 2) +283    (n + 2) * derangement(n + 1)284    ring285  rw expand286  have productA : Nat((n + 1) * derangement(n + 2)) by typecheck287  have productB : Nat((n + 2) * derangement(n + 1)) by typecheck288  arith289290-- d(n) ≤ n!, proved together with its successor.291theorem derangement.le_factorial_pair (n : Nat)292  shows derangement(n) ≤ n! ∧ derangement(n + 1) ≤ (n + 1)!293proof294  induction n295  | zero =>296    have one : 0 + 1 = 1 by compute297    have zeroFactorial : 0! = 1 by compute298    rw [one, derangement.zero, derangement.one, zeroFactorial, factorial.one]299    constructor300    . arith301    . arith302  | k + 1 using ih =>303    have first := ih.left304    have second := ih.right305    constructor306    . exact second307    . have shape : k + 1 + 1 = k + 2 by ring308      rw [shape, derangement.recurrence]309      have natA := derangement.natural at k310      have natB := derangement.natural at k + 1311      have closedK := factorial.closed at k312      have closedK1 := factorial.closed at k + 1313      have sum := LessEqual.add with second, first314      have scaled := LessEqual.mul_left at derangement(k + 1) + derangement(k),315        (k + 1)! + k!, k + 1 with sum316      have expand : (k + 2)! = (k + 1) * ((k + 1)! + k!)317        have shape2 : k + 2 = k + 1 + 1 by ring318        rw [shape2, factorial.succ, factorial.succ]319        ring320      rw expand321      exact scaled322323theorem derangement.le_factorial (n : Nat)324  shows derangement(n) ≤ n!325proof326  have pair := derangement.le_factorial_pair at n327  exact pair.left328329-- d(n + 1) < (n + 1)!, proved together with its successor.330theorem derangement.lt_factorial_pair (n : Nat)331  shows derangement(n + 1) < (n + 1)! ∧ derangement(n + 2) < (n + 2)!332proof333  induction n334  | zero =>335    have one : 0 + 1 = 1 by compute336    have two : 0 + 2 = 2 by compute337    rw [one, two, derangement.one, derangement.two]338    rw [factorial.one, factorial.two]339    constructor340    . arith341    . arith342  | k + 1 using ih =>343    have first := ih.left344    have second := ih.right345    have shape : k + 1 + 1 = k + 2 by ring346    rw shape347    constructor348    . exact second349    . have step := derangement.recurrence at k + 1350      have shape2 : k + 1 + 2 = k + 3 by ring351      rw [shape2, shape] at step352      rw [shape2, step]353      have natA := derangement.natural at k + 1354      have natB := derangement.natural at k + 2355      have closedK1 := factorial.closed at k + 1356      have closedK2 := factorial.closed at k + 2357      have firstLe := derangement.le_factorial at k + 1358      have sum := Less.add_LessEqual with second, firstLe359      have coefficient : 0 < k + 2 by arith360      have nonzero := Less.ne_zero_of_positive with coefficient361      have scaled := Less.mul_left at derangement(k + 2) + derangement(k + 1),362        (k + 2)! + (k + 1)!, k + 2 with nonzero, sum363      have expand : (k + 3)! = (k + 2) * ((k + 2)! + (k + 1)!)364        have shape3 : k + 3 = k + 2 + 1 by ring365        rw [shape3, factorial.succ]366        have inner := factorial.succ at k + 1367        rw shape at inner368        rw inner369        ring370      rw expand371      exact scaled372373theorem derangement.lt_factorial (n : Nat)374  shows derangement(n + 1) < (n + 1)!375proof376  have pair := derangement.lt_factorial_pair at n377  exact pair.left378