Grace/Cumulus/List/Index.g17

Open in Workbench Download source

Imports

Sum

Declarations

Source

1-- Reading a list by position: the default is invisible inside the list,2-- positions mirror under reversal, the last entry of a snoc, and3-- extensionality by positions in both directions4-- 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.Index10import Sum1112theorem listCoefficient.congr_default (A z w : Set) (xs : List(A)) (n : Nat)13  requires bound : n < length{A}(xs)14  shows listCoefficient{A}(z, xs, n) = listCoefficient{A}(w, xs, n)15proof16  induction xs generalizing n17  | List.nil =>18    intros n nNat bound19    rw length.nil at bound20    exfalso21    arith22  | List.cons(a, tail) using ih =>23    intros n nNat bound24    have element : a ∈ A by assumption25    rw length.cons at bound26    have shape := natural.zero_or_successor with *27    cases shape with zero | successor28    . rw [zero, listCoefficient.zero, listCoefficient.zero]29      rfl30    . obtain ⟨k, kNat, equal⟩ := successor31      rw equal at bound32      have smaller : k < length{A}(tail) by arith33      have inner := ih with k, kNat, smaller34      rw [equal, listCoefficient.succ, listCoefficient.succ]35      exact inner3637theorem listCoefficient.singleton (A z a : Set)38  requires element : a ∈ A39  shows listCoefficient{A}(z, a :: [], 0) = a40proof41  simp [listCoefficient, listHeadOr]4243theorem listCoefficient.lt_length_of_ne_default (A z : Set) (xs : List(A)) (n : Nat)44  requires different : listCoefficient{A}(z, xs, n) ≠ z45  shows n < length{A}(xs)46proof47  have alternatives : n < length{A}(xs) ∨ ¬(n < length{A}(xs)) by tauto48  cases alternatives with inside | outside49  . exact inside50  . have bound := LessEqual.of_not_Less at n, length{A}(xs) with outside51    have equal := listCoefficient.outside at A, z, xs, n with bound52    exfalso53    exact different with equal5455theorem listCoefficient.count_positive (A z : Set) (xs : List(A)) (n : Nat)56  requires bound : n < length{A}(xs)57  shows 0 < listCount{A}(listCoefficient{A}(z, xs, n), xs)58proof59  have member := listCoefficient.mem_support at A, z, xs, n with bound60  exact listCount.positive_of_mem with member6162theorem listSupport.mem_iff_index (A z y : Set) (xs : List(A))63  shows y ∈ listSupport{A}(xs) ↔64    ∃ n, Nat(n) ∧ n < length{A}(xs) ∧ listCoefficient{A}(z, xs, n) = y65proof66  constructor67  . intro member68    have cover := listSupport.exists_index at A, z, xs with *69    exact cover with y, member70  . intro witness71    obtain ⟨n, nNat, bound, value⟩ := witness72    have member := listCoefficient.mem_support at A, z, xs, n with *73    rwa value at member7475-- The last entry of a list extended by a, and reading the reversal.76theorem listCoefficient.snoc_last (A z a : Set) (xs : List(A))77  requires element : a ∈ A78  shows listCoefficient{A}(z, append(a :: [], xs), length{A}(xs)) = a79proof80  have single : List(A, a :: []) by typecheck81  have step := listCoefficient.append_right at A, z, xs, a :: [], 0 with *82  rw [add.left_unit, listCoefficient.singleton] at step83  exact step8485theorem listCoefficient.snoc_below (A z a : Set) (xs : List(A)) (n : Nat)86  requires element : a ∈ A87  requires bound : n < length{A}(xs)88  shows listCoefficient{A}(z, append(a :: [], xs), n) = listCoefficient{A}(z, xs, n)89proof90  have single : List(A, a :: []) by typecheck91  exact listCoefficient.append_left with bound9293theorem listCoefficient.reverse (A z : Set) (xs : List(A)) (n m : Nat)94  requires split : n + m + 1 = length{A}(xs)95  shows listCoefficient{A}(z, reverse(xs), n) = listCoefficient{A}(z, xs, m)96proof97  induction xs generalizing n m98  | List.nil =>99    intros n m nNat mNat split100    rw [length.nil] at split101    have sum : Nat(n + m) by typecheck102    have distinct := Naturals.disjoint.zero.succ at n + m103    rw add.right_one at split104    exfalso105    symm at split106    exact distinct with split107  | List.cons(a, tail) using ih =>108    intros n m nNat mNat split109    have element : a ∈ A by assumption110    have single : List(A, a :: []) by typecheck111    have reversed : List(A, reverse(tail)) by typecheck112    have reversedLength := reverse.length at A, tail with *113    rw [length.cons, add.right_one] at split114    have sum := Naturals.injective.succ with split115    rw reverse.cons116    have shape := natural.zero_or_successor at m with mNat117    cases shape with zero | successor118    . rw [zero, add.right_unit] at sum119      rw [zero, listCoefficient.zero, sum, ← reversedLength]120      exact listCoefficient.snoc_last with element121    . obtain ⟨k, kNat, equal⟩ := successor122      rw [equal, add.succ_right] at sum123      have smaller : n < length{A}(reverse(tail))124        rw reversedLength125        rw ← sum126        arith127      have inner : n + k + 1 = length{A}(tail)128        rw add.right_one129        exact sum130      have recursive := ih with n, k, nNat, kNat, inner131      rw [equal, listCoefficient.succ, listCoefficient.snoc_below, recursive]132      rfl133134theorem listCoefficient.reverse_head (A z : Set) (xs : List(A)) (n : Nat)135  requires split : n + 1 = length{A}(xs)136  shows listCoefficient{A}(z, reverse(xs), 0) = listCoefficient{A}(z, xs, n)137proof138  have shifted : 0 + n + 1 = length{A}(xs)139    rw add.left_unit140    exact split141  exact listCoefficient.reverse with shifted142143theorem listCoefficient.reverse_last (A z : Set) (xs : List(A)) (n : Nat)144  requires split : n + 1 = length{A}(xs)145  shows listCoefficient{A}(z, reverse(xs), n) = listCoefficient{A}(z, xs, 0)146proof147  have shifted : n + 0 + 1 = length{A}(xs)148    rw add.right_unit149    exact split150  exact listCoefficient.reverse with shifted151152-- Extensionality by positions, in both directions and with every position.153theorem listCoefficient.ext_iff (A z : Set) (xs ys : List(A))154  shows xs = ys ↔ (length{A}(xs) = length{A}(ys) ∧ (∀ n, Nat(n) → n < length{A}(xs) →155    listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)))156proof157  constructor158  . intro equal159    constructor160    . rw equal161      rfl162    . intros n nNat bound163      rw equal164      rfl165  . intro both166    obtain ⟨sameLength, entries⟩ := both167    exact listCoefficient.ext with sameLength, entries168169theorem listCoefficient.ext_all (A z : Set) (xs ys : List(A))170  requires sameLength : length{A}(xs) = length{A}(ys)171  requires entries : ∀ n, Nat(n) → listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)172  shows xs = ys173proof174  have bounded : ∀ n, Nat(n) → n < length{A}(xs) →175      listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)176    intros n nNat bound177    exact entries with n, nNat178  exact listCoefficient.ext with sameLength, bounded179180theorem listCoefficient.eq_of_entries (A z : Set) (xs ys : List(A))181  requires entries : ∀ n, Nat(n) → listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)182  requires default : ¬(z ∈ A)183  shows xs = ys184proof185  have sameLength : length{A}(xs) = length{A}(ys)186    have xsNat : Nat(length{A}(xs)) by typecheck187    have ysNat : Nat(length{A}(ys)) by typecheck188    have trichotomy := Less.trichotomy at length{A}(xs), length{A}(ys) with *189    rcases trichotomy with less | equal | greater190    . have bound : length{A}(xs) ≤ length{A}(xs) by arith191      have outside := listCoefficient.outside at A, z, xs, length{A}(xs) with bound192      have inside := listCoefficient.mem_support at A, z, ys, length{A}(xs) with less193      have value := entries with length{A}(xs), xsNat194      rw [← value, outside] at inside195      have subset := listSupport.subset at A, ys with *196      have inA := subset with z, inside197      exfalso198      exact default with inA199    . exact equal200    . have bound : length{A}(ys) ≤ length{A}(ys) by arith201      have outside := listCoefficient.outside at A, z, ys, length{A}(ys) with bound202      have inside := listCoefficient.mem_support at A, z, xs, length{A}(ys) with greater203      have value := entries with length{A}(ys), ysNat204      rw [value, outside] at inside205      have subset := listSupport.subset at A, xs with *206      have inA := subset with z, inside207      exfalso208      exact default with inA209  exact listCoefficient.ext_all with sameLength, entries210211theorem listCoefficient.take_ext (A z : Set) (xs ys : List(A)) (n : Nat)212  requires boundXs : n ≤ length{A}(xs)213  requires boundYs : n ≤ length{A}(ys)214  requires entries : ∀ k, Nat(k) → k < n →215    listCoefficient{A}(z, xs, k) = listCoefficient{A}(z, ys, k)216  shows listTake{A}(n, xs) = listTake{A}(n, ys)217proof218  have takenXs := listTake.closed at A, xs, n with *219  have takenYs := listTake.closed at A, ys, n with *220  have lengthXs := listTake.length with boundXs221  have lengthYs := listTake.length with boundYs222  have sameLength : length{A}(listTake{A}(n, xs)) = length{A}(listTake{A}(n, ys))223    rw [lengthXs, lengthYs]224    rfl225  have positions : ∀ k, Nat(k) → k < length{A}(listTake{A}(n, xs)) →226      listCoefficient{A}(z, listTake{A}(n, xs), k) = listCoefficient{A}(z, listTake{A}(n, ys), k)227    intros k kNat bound228    rw lengthXs at bound229    have left := listTake.coefficient at A, z, xs, n, k with bound230    have right := listTake.coefficient at A, z, ys, n, k with bound231    rw [left, right]232    exact entries with k, kNat, bound233  exact listCoefficient.ext with sameLength, positions234235theorem listCoefficient.drop_ext (A z : Set) (xs ys : List(A)) (n : Nat)236  requires sameLength : length{A}(xs) = length{A}(ys)237  requires entries : ∀ k, Nat(k) → n ≤ k →238    listCoefficient{A}(z, xs, k) = listCoefficient{A}(z, ys, k)239  shows listDrop{A}(n, xs) = listDrop{A}(n, ys)240proof241  have droppedXs := listDrop.closed at A, xs, n with *242  have droppedYs := listDrop.closed at A, ys, n with *243  have positions : ∀ k, Nat(k) →244      listCoefficient{A}(z, listDrop{A}(n, xs), k) = listCoefficient{A}(z, listDrop{A}(n, ys), k)245    intros k kNat246    have left := listDrop.coefficient at A, z, xs, n, k with *247    have right := listDrop.coefficient at A, z, ys, n, k with *248    have shifted : Nat(n + k) by typecheck249    have above : n ≤ n + k by arith250    rw [left, right]251    exact entries with n + k, shifted, above252  have lengths : length{A}(listDrop{A}(n, xs)) = length{A}(listDrop{A}(n, ys))253    have alternatives : n ≤ length{A}(xs) ∨ ¬(n ≤ length{A}(xs)) by tauto254    cases alternatives with inside | outside255    . have insideYs : n ≤ length{A}(ys) by rwa ← sameLength256      have left := listDrop.length with inside257      have right := listDrop.length with insideYs258      rw sameLength at left259      rw ← right at left260      exact add.right_cancel with left261    . have beyond := Less.of_not_LessEqual at n, length{A}(xs) with outside262      have boundXs : length{A}(xs) ≤ n by arith263      have boundYs : length{A}(ys) ≤ n by rwa ← sameLength264      have left := listDrop.all with boundXs265      have right := listDrop.all with boundYs266      rw [left, right]267      rfl268  exact listCoefficient.ext_all with lengths, positions269