Grace/Cumulus/List/Append.g17

Open in Workbench Download source

Imports

Algebra.IndexedLists

Declarations

Source

1-- Concatenation of lists: how indexing reads through it, cancellation on2-- either side, and mapping over it3-- 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.Append9import Algebra.IndexedLists1011-- append(ys, xs) is xs followed by ys. Positions below the length of xs12-- read xs; later positions read ys, shifted by that length.13theorem listCoefficient.append_left (A z : Set) (xs ys : List(A)) (n : Nat)14  requires bound : n < length{A}(xs)15  shows listCoefficient{A}(z, append(ys, xs), n) = listCoefficient{A}(z, xs, n)16proof17  induction xs generalizing n18  | List.nil =>19    intros n nNat bound20    rw length.nil at bound21    arith22  | List.cons(a, tail) using ih =>23    intros n nNat bound24    have element : a ∈ A by assumption25    have appended : List(A, append(ys, tail)) by typecheck26    rw append27    have shape := natural.zero_or_successor with *28    cases shape with zero | successor29    . rw [zero, listCoefficient.zero, listCoefficient.zero]30      rfl31    . obtain ⟨r, rNat, equal⟩ := successor32      rw [equal, length.cons] at bound33      have smaller : r < length{A}(tail) by arith34      rw [equal, listCoefficient.succ, listCoefficient.succ]35      exact ih with r, rNat, smaller3637theorem listCoefficient.append_right (A z : Set) (xs ys : List(A)) (n : Nat)38  shows listCoefficient{A}(z, append(ys, xs), n + length{A}(xs)) = listCoefficient{A}(z, ys, n)39proof40  induction xs41  | List.nil =>42    rw [append, length.nil, add.right_unit]43    rfl44  | List.cons(a, tail) using ih =>45    have element : a ∈ A by assumption46    have appended : List(A, append(ys, tail)) by typecheck47    rwa [append, length.cons, add.succ_right, listCoefficient.succ]4849-- Cancellation: a common first part, or a common last part, can be dropped.50theorem append.cancel_first (A : Set) (xs ys zs : List(A))51  requires equal : append(ys, xs) = append(zs, xs)52  shows ys = zs53proof54  have lengths : length{A}(append(ys, xs)) = length{A}(append(zs, xs))55    rw equal56    rfl57  rw [length.append, length.append] at lengths58  have sameLength := add.left_cancel with lengths59  apply listCoefficient.ext at A, ∅, ys, zs with sameLength60  intros n nNat bound61  have left := listCoefficient.append_right at A, ∅, xs, ys, n with *62  have right := listCoefficient.append_right at A, ∅, xs, zs, n with *63  rw equal at left64  rwa ← left6566theorem append.cancel_last (A : Set) (xs ys zs : List(A))67  requires equal : append(xs, ys) = append(xs, zs)68  shows ys = zs69proof70  have lengths : length{A}(append(xs, ys)) = length{A}(append(xs, zs))71    rw equal72    rfl73  rw [length.append, length.append] at lengths74  have sameLength := add.right_cancel with lengths75  apply listCoefficient.ext at A, ∅, ys, zs with sameLength76  intros n nNat bound77  have boundZs : n < length{A}(zs) by rwa ← sameLength78  have left := listCoefficient.append_left at A, ∅, ys, xs, n with *79  have right := listCoefficient.append_left at A, ∅, zs, xs, n with boundZs, *80  rw equal at left81  rwa ← left8283theorem listMap.append (A B f : Set) (xs ys : List(A))84  requires function : f : A → B85  shows listMap{A}(f, append(ys, xs)) = append{B}(listMap{A}(f, ys), listMap{A}(f, xs))86proof87  induction xs88  | List.nil =>89    rw [append, listMap, append]90    rfl91  | List.cons(a, tail) using ih =>92    have element : a ∈ A by assumption93    have image := FunctionBetween.apply_closed with function, element94    rw [append, listMap, listMap, ih, append]95    rfl96