Grace/Cumulus/List/Range.g17

Open in Workbench Download source

Imports

Sorted

Declarations

Source

1-- The list of the first n natural numbers in order: length, entries,2-- support, sortedness, counts, and prefixes3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.List.Range9import Sorted1011def listRange (n : Nat) → Set12  | zero => []13  | succ(k) => append{ℕ}(k :: [], listRange(k))1415theorem listRange.zero16  shows listRange(0) = []17proof18  simp [listRange]1920theorem listRange.succ (n : Nat)21  shows listRange(succ(n)) = append{ℕ}(n :: [], listRange(n))22proof23  simp [listRange]2425theorem listRange.closed (n : Nat)26  shows List(ℕ, listRange(n))27proof28  induction n29  | zero =>30    rw listRange.zero31    typecheck32  | succ(k) using ih =>33    have kIn : k ∈ ℕ := nat.omega.forward with *34    have single : List(ℕ, k :: []) by typecheck35    rw listRange.succ36    typecheck3738theorem listRange.length (n : Nat)39  shows length{ℕ}(listRange(n)) = n40proof41  induction n42  | zero =>43    rw [listRange.zero, length.nil]44    rfl45  | succ(k) using ih =>46    have kIn : k ∈ ℕ := nat.omega.forward with *47    have single : List(ℕ, k :: []) by typecheck48    have list := listRange.closed at k with *49    rw [listRange.succ, length.append, ih, length.singleton, add.right_one]50    rfl5152theorem listRange.coefficient (n i : Nat)53  requires bound : i < n54  shows listCoefficient{ℕ}(0, listRange(n), i) = i55proof56  induction n57  | zero =>58    intro bound59    exfalso60    arith61  | succ(k) using ih =>62    intro bound63    have kIn : k ∈ ℕ := nat.omega.forward with *64    have list := listRange.closed at k with *65    have length := listRange.length at k with *66    rw listRange.succ67    have alternatives : i < k ∨ ¬(i < k) by tauto68    cases alternatives with below | notBelow69    . have inside : i < length{ℕ}(listRange(k)) by rwa length70      have step := listCoefficient.snoc_below at ℕ, 0, k, listRange(k), i with kIn, inside71      rw step72      exact ih with below73    . have atLeast := LessEqual.of_not_Less at i, k with notBelow74      have same : i = k75        have upper := Less.successor_upper with bound76        exact LessEqual.antisymmetric with upper, atLeast77      have last := listCoefficient.snoc_last at ℕ, 0, k, listRange(k) with kIn78      rw length at last79      rw same80      exact last8182theorem listRange.mem_support (n : Nat)83  shows ∀ y, y ∈ listSupport{ℕ}(listRange(n)) ↔ y ∈ n84proof85  induction n86  | zero =>87    intro y88    rw [listRange.zero, listSupport.nil]89    constructor90    . intro member91      exfalso92      exact set.empty with member93    . intro member94      have zero : y ∈ ∅ by rwa ← nat.zero95      exfalso96      exact set.empty with zero97  | succ(k) using ih =>98    intro y99    have kIn : k ∈ ℕ := nat.omega.forward with *100    have single : List(ℕ, k :: []) by typecheck101    have list := listRange.closed at k with *102    have successor := natural.successor_as_insert at k with *103    have inner := ih with y104    rw [listRange.succ, listSupport.append, listSupport.singleton, successor]105    have union := union2.membership at y, listSupport{ℕ}(listRange(k)), {k}106    have insertion := insert.membership at y, k, k107    have singleton := singleton.membership at y, k108    tauto109110theorem listRange.support (n : Nat)111  shows listSupport{ℕ}(listRange(n)) = n112proof113  have members := listRange.mem_support at n with *114  ext y115  exact members with y116117theorem listRange.mem_support_iff (n : Nat) (y : Set)118  shows y ∈ listSupport{ℕ}(listRange(n)) ↔ (Nat(y) ∧ y < n)119proof120  rw listRange.support121  constructor122  . intro member123    have natural := natural.member at n with *124    have yNat := natural with y, member125    have below := Less.of_membership at y, n with *, member126    exact ⟨yNat, below⟩127  . intro both128    obtain ⟨yNat, below⟩ := both129    exact membership.of_Less at y, n with *, below130131theorem listRange.sorted (n : Nat)132  shows ListSorted(listRange(n))133proof134  have list := listRange.closed at n with *135  have length := listRange.length at n with *136  unfold ListSorted137  intros i j iNat jNat below bound138  rw length at bound139  have smaller : i < n by arith140  have left := listRange.coefficient at n, i with smaller141  have right := listRange.coefficient at n, j with bound142  rw [left, right]143  exact Less.implies_LessEqual with below144145theorem listRange.count_below (n i : Nat)146  requires bound : i < n147  shows listCount{ℕ}(i, listRange(n)) = 1148proof149  induction n150  | zero =>151    intro bound152    exfalso153    arith154  | succ(k) using ih =>155    intro bound156    have kIn : k ∈ ℕ := nat.omega.forward with *157    have single : List(ℕ, k :: []) by typecheck158    have list := listRange.closed at k with *159    rw [listRange.succ, listCount.append]160    have alternatives : i < k ∨ ¬(i < k) by tauto161    cases alternatives with below | notBelow162    . have inner := ih with below163      have different : i ≠ k164        intro same165        rw same at below166        exact Less.irreflexive with *, below167      have other := listCount.singleton_other at ℕ, i, k with kIn, different168      rw [inner, other, add.right_unit]169      rfl170    . have atLeast := LessEqual.of_not_Less at i, k with notBelow171      have same : i = k172        have upper := Less.successor_upper with bound173        exact LessEqual.antisymmetric with upper, atLeast174      have absent : ¬(i ∈ listSupport{ℕ}(listRange(k)))175        intro member176        have both := listRange.mem_support_iff.forward at k, i with member177        rw same at both178        have strict := both.right179        exact Less.irreflexive at k with *, strict180      have zero := listCount.zero_of_absent with absent181      rw [zero, same, listCount.singleton_self, add.left_unit]182      rfl183184theorem listRange.count_above (n i : Nat)185  requires bound : n ≤ i186  shows listCount{ℕ}(i, listRange(n)) = 0187proof188  have list := listRange.closed at n with *189  have absent : ¬(i ∈ listSupport{ℕ}(listRange(n)))190    intro member191    have both := listRange.mem_support_iff.forward at n, i with member192    have below := both.right193    have strict : i < i by arith194    exact Less.irreflexive at i with *, strict195  exact listCount.zero_of_absent with absent196197theorem listRange.prefix (m n : Nat)198  requires bound : m ≤ n199  shows ListPrefix(ℕ, listRange(m), listRange(n))200proof201  induction n202  | zero =>203    intro bound204    have zero : m = 0205      have lower : 0 ≤ m by arith206      exact LessEqual.antisymmetric with bound, lower207    rw [zero, listRange.zero]208    have nilList : List(ℕ, []) by typecheck209    exact ListPrefix.reflexive at ℕ, [] with *210  | succ(k) using ih =>211    intro bound212    have kIn : k ∈ ℕ := nat.omega.forward with *213    have single : List(ℕ, k :: []) by typecheck214    have list := listRange.closed at k with *215    have listM := listRange.closed at m with *216    have alternatives : m ≤ k ∨ ¬(m ≤ k) by tauto217    cases alternatives with below | notBelow218    . have inner := ih with below219      have extend := ListPrefix.append at ℕ, listRange(k), k :: [] with *220      rw listRange.succ221      exact ListPrefix.transitive with inner, extend222    . have above := Less.of_not_LessEqual at m, k with notBelow223      have same : m = succ(k)224        have upper : m ≤ succ(k) := bound225        have lower : succ(k) ≤ m by arith226        exact LessEqual.antisymmetric with upper, lower227      rw same228      have listSucc := listRange.closed at succ(k) with *229      exact ListPrefix.reflexive at ℕ, listRange(succ(k)) with *230231theorem listRange.take (m n : Nat)232  requires bound : m ≤ n233  shows listTake{ℕ}(m, listRange(n)) = listRange(m)234proof235  have prefix := listRange.prefix with bound236  have listM := listRange.closed at m with *237  have listN := listRange.closed at n with *238  have taken := ListPrefix.eq_take with prefix239  rw listRange.length at taken240  symm241  exact taken242