Grace/Cumulus/List/Replicate.g17

Open in Workbench Download source

Imports

Basic

Declarations

Source

1-- Constant lists: n copies of one element, their length, support, and2-- interaction with concatenation, mapping, reversal, and indexing3-- 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.Replicate9import Basic1011def listReplicate (n : Nat, x : Set) → Set12  | zero, x => []13  | succ(k), x => x :: listReplicate(k, x)1415theorem listReplicate.zero (x : Set)16  shows listReplicate(0, x) = []17proof18  simp [listReplicate]1920theorem listReplicate.succ (n : Nat) (x : Set)21  shows listReplicate(succ(n), x) = x :: listReplicate(n, x)22proof23  simp [listReplicate]2425theorem listReplicate.closed (A x : Set) (n : Nat)26  requires element : x ∈ A27  shows List(A, listReplicate(n, x))28proof29  induction n30  | zero =>31    rw listReplicate.zero32    typecheck33  | succ(k) using ih =>34    rw listReplicate.succ35    typecheck3637theorem listReplicate.length (A x : Set) (n : Nat)38  requires element : x ∈ A39  shows length{A}(listReplicate(n, x)) = n40proof41  induction n42  | zero =>43    rw [listReplicate.zero, length.nil]44    rfl45  | succ(k) using ih =>46    have list := listReplicate.closed at A, x, k with element47    rw [listReplicate.succ, length.cons, ih]48    rfl4950theorem listReplicate.one (x : Set)51  shows listReplicate(1, x) = x :: []52proof53  simp [listReplicate]5455theorem listReplicate.support_subset (A x : Set) (n : Nat)56  requires element : x ∈ A57  shows listSupport{A}(listReplicate(n, x)) ⊆ {x}58proof59  induction n60  | zero =>61    rw [listReplicate.zero, listSupport.nil]62    exact empty.subset63  | succ(k) using ih =>64    have list := listReplicate.closed at A, x, k with element65    rw [listReplicate.succ, listSupport.cons]66    intros y hy67    have alternatives := insert.membership.forward with hy68    cases alternatives with head | rest69    . rw head70      exact singleton.self at x71    . exact ih with y, rest7273theorem listReplicate.support_succ (A x : Set) (n : Nat)74  requires element : x ∈ A75  shows listSupport{A}(listReplicate(succ(n), x)) = {x}76proof77  have list := listReplicate.closed at A, x, n with element78  have subset := listReplicate.support_subset at A, x, succ(n) with element79  apply Subset.antisymmetric with subset80  intros y hy81  have equal := singleton.membership.forward with hy82  rw [equal, listReplicate.succ]83  exact listSupport.mem_cons_self with element8485theorem listReplicate.mem_support (A x y : Set) (n : Nat)86  requires element : x ∈ A87  requires member : y ∈ listSupport{A}(listReplicate(n, x))88  shows y = x89proof90  have subset := listReplicate.support_subset at A, x, n with element91  have single := subset with y, member92  exact singleton.membership.forward with single9394theorem listReplicate.mem_support_iff (A x y : Set) (n : Nat)95  requires element : x ∈ A96  shows y ∈ listSupport{A}(listReplicate(n, x)) ↔ 0 < n ∧ y = x97proof98  constructor99  . intro member100    have equal := listReplicate.mem_support with element, member101    have nonempty : listReplicate(n, x) ≠ []102      intro empty103      rw [empty, listSupport.nil] at member104      exact set.empty with member105    have shape := natural.zero_or_successor with *106    cases shape with zero | successor107    . rw [zero, listReplicate.zero] at nonempty108      exfalso109      have same : [] = [] by rfl110      exact nonempty with same111    . obtain ⟨k, kNat, equal2⟩ := successor112      rw equal2113      constructor114      . arith115      . exact equal116  . intro both117    obtain ⟨positive, equal⟩ := both118    have shape := natural.zero_or_successor with *119    cases shape with zero | successor120    . rw zero at positive121      exfalso122      exact Less.irreflexive with Naturals.constructor.zero, positive123    . obtain ⟨k, kNat, equal2⟩ := successor124      rw [equal2, listReplicate.support_succ, equal]125      exact singleton.self at x126127theorem listReplicate.append (A x : Set) (m n : Nat)128  requires element : x ∈ A129  shows append{A}(listReplicate(m, x), listReplicate(n, x)) = listReplicate(n + m, x)130proof131  induction n132  | zero =>133    have list := listReplicate.closed at A, x, m with element134    rw [listReplicate.zero, add.left_unit]135    simp [append]136  | succ(k) using ih =>137    have list := listReplicate.closed at A, x, k with element138    have other := listReplicate.closed at A, x, m with element139    rw [listReplicate.succ, append.cons, ih]140    have shift : succ(k) + m = succ(k + m) by simp [add, add.succ_right]141    rw [shift, listReplicate.succ]142    rfl143144theorem listReplicate.map (A B f x : Set) (n : Nat)145  requires function : f : A → B146  requires element : x ∈ A147  shows listMap{A}(f, listReplicate(n, x)) = listReplicate(n, f(x))148proof149  induction n150  | zero =>151    rw [listReplicate.zero, listMap.nil, listReplicate.zero]152    rfl153  | succ(k) using ih =>154    have list := listReplicate.closed at A, x, k with element155    rw [listReplicate.succ, listMap.cons, ih, listReplicate.succ]156    rfl157158theorem listReplicate.reverse (A x : Set) (n : Nat)159  requires element : x ∈ A160  shows reverse{A}(listReplicate(n, x)) = listReplicate(n, x)161proof162  induction n163  | zero =>164    rw listReplicate.zero165    simp [reverse]166  | succ(k) using ih =>167    have list := listReplicate.closed at A, x, k with element168    have reversed : List(A, reverse(listReplicate(k, x))) by typecheck169    have single : List(A, x :: []) by typecheck170    rw [listReplicate.succ, reverse.cons, ih]171    have one := listReplicate.one at x172    rw [← one, listReplicate.append, add.right_one]173    exact listReplicate.succ at k, x174175theorem listReplicate.tail (A x : Set) (n : Nat)176  requires element : x ∈ A177  shows listTail{A}(listReplicate(succ(n), x)) = listReplicate(n, x)178proof179  have list := listReplicate.closed at A, x, n with element180  rw [listReplicate.succ, listTail.cons]181  rfl182183theorem listReplicate.coefficient (A z x : Set) (n k : Nat)184  requires element : x ∈ A185  requires bound : k < n186  shows listCoefficient{A}(z, listReplicate(n, x), k) = x187proof188  induction n generalizing k189  | zero =>190    intros k kNat bound191    exfalso192    arith193  | succ(j) using ih =>194    intros k kNat bound195    have list := listReplicate.closed at A, x, j with element196    have shape := natural.zero_or_successor at k with *197    rw listReplicate.succ198    cases shape with zero | successor199    . rw [zero, listCoefficient.zero]200      rfl201    . obtain ⟨r, rNat, equal⟩ := successor202      rw equal at bound203      have smaller : r < j by arith204      rw [equal, listCoefficient.succ]205      exact ih with r, rNat, smaller206207-- A list whose support lies in a singleton is constant.208theorem List.constant_of_support (A x : Set) (xs : List(A))209  requires element : x ∈ A210  requires support : listSupport{A}(xs) ⊆ {x}211  shows xs = listReplicate(length{A}(xs), x)212proof213  induction xs214  | List.nil =>215    intro support216    rw [length.nil, listReplicate.zero]217    rfl218  | List.cons(a, tail) using ih =>219    intro support220    have headA : a ∈ A by assumption221    have headIn := listSupport.mem_cons_self with headA222    have headSingle := support with a, headIn223    have head := singleton.membership.forward with headSingle224    have rest : listSupport{A}(tail) ⊆ {x}225      intros y hy226      have member := listSupport.mem_cons_of_mem with headA, hy227      exact support with y, member228    have tails := ih with rest229    rw [length.cons, listReplicate.succ, head]230    rw ← tails231    rfl232233theorem listReplicate.injective_length (A x : Set) (m n : Nat)234  requires element : x ∈ A235  requires equal : listReplicate(m, x) = listReplicate(n, x)236  shows m = n237proof238  have lengths : length{A}(listReplicate(m, x)) = length{A}(listReplicate(n, x))239    rw equal240    rfl241  rw [listReplicate.length, listReplicate.length] at lengths242  exact lengths243