Grace/Cumulus/List/Sum.g17

Open in Workbench Download source

Imports

Permutation

Declarations

• listSum def
• listSum.nil theorem derivation
• listSum.cons theorem derivation
• listSum.natural theorem derivation
• listSum.singleton theorem derivation
• listSum.append theorem derivation
• listSum.reverse theorem derivation
• listSum.replicate theorem derivation
• listSum.cons_le theorem derivation
• listSum.head_le theorem derivation
• listSum.le_of_mem theorem derivation
• listSum.eq_zero theorem derivation
• listSum.zero_of_all theorem derivation
• listSum.zero_iff theorem derivation
• listSum.take_add_drop theorem derivation
• listSum.filter_add_complement theorem derivation
• listSum.filter_le theorem derivation
• listSum.append_le_left theorem derivation
• listSum.append_le_right theorem derivation
• listSum.take_le theorem derivation
• listSum.drop_le theorem derivation
• listSum.of_permutation theorem derivation
• listSum.length_le_of_positive theorem derivation
• listSum.le_length_mul theorem derivation

Source

1-- Sums of lists of natural numbers: the equation lemmas, concatenation,2-- reversal, constant lists, bounds by the entries, splitting by take and3-- drop or by a filter, and invariance under permutation4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.List.Sum10import Permutation1112def listSum (xs : List(ℕ)) → Nat13  | [] => 014  | x :: rest => add(x, listSum(rest))1516theorem listSum.nil17  shows listSum([]) = 018proof19  simp [listSum]2021theorem listSum.cons (x : Nat) (rest : List(ℕ))22  shows listSum(x :: rest) = x + listSum(rest)23proof24  simp [listSum]2526theorem listSum.natural (xs : List(ℕ))27  shows Nat(listSum(xs))28proof29  typecheck3031theorem listSum.singleton (x : Nat)32  shows listSum(x :: []) = x33proof34  simp [listSum, add.right_unit]3536theorem listSum.append (xs ys : List(ℕ))37  shows listSum(append(ys, xs)) = listSum(xs) + listSum(ys)38proof39  induction xs40  | List.nil =>41    rw [append.nil, listSum.nil, add.left_unit]42    rfl43  | List.cons(x, tail) using ih =>44    have xIn : x ∈ ℕ by assumption45    have xNat := nat.omega.backward with xIn46    have appended := append.closed at ℕ, tail, ys with *47    rw [append.cons, listSum.cons, ih, listSum.cons, add.associative]48    rfl4950theorem listSum.reverse (xs : List(ℕ))51  shows listSum(reverse(xs)) = listSum(xs)52proof53  induction xs54  | List.nil =>55    rw reverse.nil56    rfl57  | List.cons(x, tail) using ih =>58    have xIn : x ∈ ℕ by assumption59    have xNat := nat.omega.backward with xIn60    have single : List(ℕ, x :: []) by typecheck61    have reversed : List(ℕ, reverse{ℕ}(tail)) by typecheck62    rw [reverse.cons, listSum.append, ih, listSum.singleton, listSum.cons]63    rw add.commutative64    rfl6566theorem listSum.replicate (x : Nat) (n : Nat)67  shows listSum(listReplicate(n, x)) = n * x68proof69  induction n70  | zero =>71    rw [listReplicate.zero, listSum.nil, mul.left_zero]72    rfl73  | succ(k) using ih =>74    have xIn : x ∈ ℕ := nat.omega.forward with *75    have list := listReplicate.closed at ℕ, x, k with xIn76    rw [listReplicate.succ, listSum.cons, ih, mul.succ_left]77    rfl7879theorem listSum.cons_le (x : Nat) (rest : List(ℕ))80  shows listSum(rest) ≤ listSum(x :: rest)81proof82  rw listSum.cons83  arith8485theorem listSum.head_le (x : Nat) (rest : List(ℕ))86  shows x ≤ listSum(x :: rest)87proof88  rw listSum.cons89  arith9091theorem listSum.le_of_mem (x : Set) (xs : List(ℕ))92  requires member : x ∈ listSupport{ℕ}(xs)93  shows x ≤ listSum(xs)94proof95  induction xs96  | List.nil =>97    intro member98    rw listSupport.nil at member99    exfalso100    exact set.empty with member101  | List.cons(y, tail) using ih =>102    intro member103    have yIn : y ∈ ℕ by assumption104    have yNat := nat.omega.backward with yIn105    have split := listSupport.mem_cons_iff.forward with yIn, member106    rw listSum.cons107    cases split with head | rest108    . rw head109      arith110    . have inner := ih with rest111      have subset := listSupport.subset at ℕ, tail with *112      have xIn := subset with x, rest113      have xNat := nat.omega.backward with xIn114      arith115116theorem listSum.eq_zero (xs : List(ℕ))117  requires zero : listSum(xs) = 0118  shows ∀ x ∈ listSupport{ℕ}(xs), x = 0119proof120  intros x hx121  have bound := listSum.le_of_mem with hx122  rw zero at bound123  have subset := listSupport.subset at ℕ, xs with *124  have xIn := subset with x, hx125  have xNat := nat.omega.backward with xIn126  have lower : 0 ≤ x by arith127  exact LessEqual.antisymmetric with bound, lower128129theorem listSum.zero_of_all (xs : List(ℕ))130  requires zeros : ∀ x ∈ listSupport{ℕ}(xs), x = 0131  shows listSum(xs) = 0132proof133  induction xs134  | List.nil =>135    intro zeros136    exact listSum.nil137  | List.cons(y, tail) using ih =>138    intro zeros139    have yIn : y ∈ ℕ by assumption140    have headIn := listSupport.mem_cons_self at ℕ, y, tail with yIn141    have head := zeros with y, headIn142    have rest : ∀ x ∈ listSupport{ℕ}(tail), x = 0143      intros x hx144      have outer := listSupport.mem_cons_of_mem with yIn, hx145      exact zeros with x, outer146    have inner := ih with rest147    rw [listSum.cons, head, inner, add.right_unit]148    rfl149150theorem listSum.zero_iff (xs : List(ℕ))151  shows listSum(xs) = 0 ↔ ∀ x ∈ listSupport{ℕ}(xs), x = 0152proof153  constructor154  . intro zero155    exact listSum.eq_zero with zero156  . intro zeros157    exact listSum.zero_of_all with zeros158159theorem listSum.take_add_drop (xs : List(ℕ)) (n : Nat)160  shows listSum(listTake{ℕ}(n, xs)) + listSum(listDrop{ℕ}(n, xs)) = listSum(xs)161proof162  have split := listTake.append_drop at ℕ, xs, n with *163  have taken := listTake.closed at ℕ, xs, n with *164  have dropped := listDrop.closed at ℕ, xs, n with *165  have sums := listSum.append at listTake{ℕ}(n, xs), listDrop{ℕ}(n, xs) with *166  rw split at sums167  symm168  exact sums169170theorem listSum.filter_add_complement (S : Set) (xs : List(ℕ))171  shows listSum(listFilter{ℕ}(S, xs)) + listSum(listFilter{ℕ}(ℕ ∖ S, xs)) = listSum(xs)172proof173  induction xs174  | List.nil =>175    rw [listFilter.nil, listFilter.nil, listSum.nil, add.right_unit]176    rfl177  | List.cons(x, tail) using ih =>178    have xIn : x ∈ ℕ by assumption179    have xNat := nat.omega.backward with xIn180    have kept := listFilter.closed at ℕ, S, tail with *181    have discarded := listFilter.closed at ℕ, ℕ ∖ S, tail with *182    have keptNat := listSum.natural at listFilter{ℕ}(S, tail) with *183    have discardedNat := listSum.natural at listFilter{ℕ}(ℕ ∖ S, tail) with *184    have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto185    rw listSum.cons186    cases alternatives with member | absent187    . have notDifference : ¬(x ∈ ℕ ∖ S) by simp188      rw [listFilter.cons_member, listFilter.cons_other, listSum.cons, add.associative, ih]189      rfl190    . have inDifference : x ∈ ℕ ∖ S by simp191      rw [listFilter.cons_other, listFilter.cons_member, listSum.cons]192      rw [add.swap, ih]193      rfl194195theorem listSum.filter_le (S : Set) (xs : List(ℕ))196  shows listSum(listFilter{ℕ}(S, xs)) ≤ listSum(xs)197proof198  have total := listSum.filter_add_complement at S, xs with *199  have kept := listFilter.closed at ℕ, S, xs with *200  have discarded := listFilter.closed at ℕ, ℕ ∖ S, xs with *201  have keptNat := listSum.natural at listFilter{ℕ}(S, xs) with *202  have discardedNat := listSum.natural at listFilter{ℕ}(ℕ ∖ S, xs) with *203  rw ← total204  arith205206theorem listSum.append_le_left (xs ys : List(ℕ))207  shows listSum(xs) ≤ listSum(append(ys, xs))208proof209  have xsNat := listSum.natural at xs with *210  have ysNat := listSum.natural at ys with *211  rw listSum.append212  arith213214theorem listSum.append_le_right (xs ys : List(ℕ))215  shows listSum(ys) ≤ listSum(append(ys, xs))216proof217  have xsNat := listSum.natural at xs with *218  have ysNat := listSum.natural at ys with *219  rw listSum.append220  arith221222theorem listSum.take_le (xs : List(ℕ)) (n : Nat)223  shows listSum(listTake{ℕ}(n, xs)) ≤ listSum(xs)224proof225  have total := listSum.take_add_drop at xs, n with *226  have taken := listTake.closed at ℕ, xs, n with *227  have dropped := listDrop.closed at ℕ, xs, n with *228  have takenNat := listSum.natural at listTake{ℕ}(n, xs) with *229  have droppedNat := listSum.natural at listDrop{ℕ}(n, xs) with *230  rw ← total231  arith232233theorem listSum.drop_le (xs : List(ℕ)) (n : Nat)234  shows listSum(listDrop{ℕ}(n, xs)) ≤ listSum(xs)235proof236  have total := listSum.take_add_drop at xs, n with *237  have taken := listTake.closed at ℕ, xs, n with *238  have dropped := listDrop.closed at ℕ, xs, n with *239  have takenNat := listSum.natural at listTake{ℕ}(n, xs) with *240  have droppedNat := listSum.natural at listDrop{ℕ}(n, xs) with *241  rw ← total242  arith243244-- The sum does not depend on the order of the entries.245theorem listSum.of_permutation (xs ys : List(ℕ))246  requires permutation : ListPermutation(ℕ, xs, ys)247  shows listSum(xs) = listSum(ys)248proof249  induction xs generalizing ys250  | List.nil =>251    intros ys ysList permutation252    have back := ListPermutation.symmetric with permutation253    have empty := ListPermutation.nil with back254    rw empty255    rfl256  | List.cons(x, tail) using ih =>257    intros ys ysList permutation258    have xIn : x ∈ ℕ by assumption259    have xNat := nat.omega.backward with xIn260    obtain ⟨front, frontList, back, backList, equal, rest⟩ :=261      ListPermutation.cons_split with xIn, permutation262    have appended := append.closed at ℕ, front, back with *263    have inner := ih with append{ℕ}(back, front), appended, rest264    have backCons : List(ℕ, x :: back) by typecheck265    have frontNat := listSum.natural at front with *266    have backNat := listSum.natural at back with *267    rw [equal, listSum.cons, inner, listSum.append, listSum.append, listSum.cons]268    exact add.swap at listSum(front), listSum(back), x with *269270theorem listSum.length_le_of_positive (xs : List(ℕ))271  requires positive : ∀ x ∈ listSupport{ℕ}(xs), 0 < x272  shows length{ℕ}(xs) ≤ listSum(xs)273proof274  induction xs275  | List.nil =>276    intro positive277    rw [length.nil, listSum.nil]278    arith279  | List.cons(y, tail) using ih =>280    intro positive281    have yIn : y ∈ ℕ by assumption282    have yNat := nat.omega.backward with yIn283    have headIn := listSupport.mem_cons_self at ℕ, y, tail with yIn284    have head := positive with y, headIn285    have rest : ∀ x ∈ listSupport{ℕ}(tail), 0 < x286      intros x hx287      have outer := listSupport.mem_cons_of_mem with yIn, hx288      exact positive with x, outer289    have inner := ih with rest290    have tailNat := listSum.natural at tail with *291    rw [length.cons, listSum.cons]292    arith293294theorem listSum.le_length_mul (xs : List(ℕ)) (bound : Nat)295  requires bounded : ∀ x ∈ listSupport{ℕ}(xs), x ≤ bound296  shows listSum(xs) ≤ length{ℕ}(xs) * bound297proof298  induction xs299  | List.nil =>300    intro bounded301    rw [length.nil, listSum.nil, mul.left_zero]302    arith303  | List.cons(y, tail) using ih =>304    intro bounded305    have yIn : y ∈ ℕ by assumption306    have yNat := nat.omega.backward with yIn307    have headIn := listSupport.mem_cons_self at ℕ, y, tail with yIn308    have head := bounded with y, headIn309    have rest : ∀ x ∈ listSupport{ℕ}(tail), x ≤ bound310      intros x hx311      have outer := listSupport.mem_cons_of_mem with yIn, hx312      exact bounded with x, outer313    have inner := ih with rest314    have tailNat := listSum.natural at tail with *315    have product : Nat(length{ℕ}(tail) * bound) by typecheck316    rw [length.cons, listSum.cons, mul.succ_left]317    arith318