Grace/Cumulus/Algebra/IndexedLists.g17

Open in Workbench Download source

Imports

CoefficientLists · Cardinal.ListSupport

Declarations

Source

1-- Lists as functions on their finite ordinal of positions (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.IndexedLists8import CoefficientLists9import Cardinal.ListSupport1011theorem listCoefficient.mem_support (A z : Set) (xs : List(A)) (n : Nat)12  requires bound : n < length{A}(xs)13  shows listCoefficient{A}(z, xs, n) ∈ listSupport{A}(xs)14proof15  induction xs generalizing n16  | List.nil =>17    intros n natural bound18    rw length.nil at bound19    have impossible : 0 < 0 by arith20    exfalso21    exact Less.irreflexive with Naturals.constructor.zero, impossible22  | List.cons(a, tail) using ih =>23    intros n natural 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, listSupport]29      exact insert.self30    . obtain ⟨k, kNat, equal⟩ := successor31      have smaller : k < length{A}(tail) by arith32      have previous := ih with k, kNat, smaller33      rw [equal, listCoefficient.succ, listSupport]34      exact insert.contains with previous3536theorem listCoefficient.closed (A z : Set) (xs : List(A)) (n : Nat)37  requires default : z ∈ A38  shows listCoefficient{A}(z, xs, n) ∈ A39proof40  have casesN : n < length{A}(xs) ∨ ¬(n < length{A}(xs)) by tauto41  cases casesN with inside | outside42  . have supported := listCoefficient.mem_support at A, z, xs, n with *43    have subset := listSupport.subset with *44    exact subset with listCoefficient{A}(z, xs, n), supported45  . have bound : length{A}(xs) ≤ n46      exact LessEqual.of_not_Less with *47    rwa listCoefficient.outside4849-- No default-element hypothesis is needed: every index is in range.50defgraph listEntries (A z xs : Set) (i ∈ length{A}(xs)) : listSupport{A}(xs) := listCoefficient{A}(z, xs, i)51requires list : List(A, xs)52proof53  have size : Nat(length{A}(xs)) by typecheck54  have positions := natural.member with size55  have index := positions with i56  have bound := Less.of_membership with *57  exact listCoefficient.mem_support with *5859theorem listCoefficient.ext (A z : Set) (xs ys : List(A))60  requires sameLength : length{A}(xs) = length{A}(ys)61  requires entries : ∀ n, Nat(n) → n < length{A}(xs) → listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)62  shows xs = ys63proof64  induction xs generalizing ys65  | List.nil =>66    intros ys ysList sameLength entries67    have shape := List.cases with ysList68    cases shape with empty | nonempty69    . rw empty70      rfl71    . obtain ⟨b, hb, tail, tailList, equal⟩ := nonempty72      rw [equal, length.nil, length.cons] at sameLength73      have impossible : 0 < 0 by arith74      exfalso75      exact Less.irreflexive with Naturals.constructor.zero, impossible76  | List.cons(a, tail) using ih =>77    intros ys ysList sameLength entries78    have headIn : a ∈ A by assumption79    have shape := List.cases with ysList80    cases shape with empty | nonempty81    . rw [empty, length.cons, length.nil] at sameLength82      have impossible : 0 < 0 by arith83      exfalso84      exact Less.irreflexive with Naturals.constructor.zero, impossible85    . obtain ⟨b, hb, rest, restList, equal⟩ := nonempty86      rw [equal, length.cons, length.cons] at sameLength87      have lengths := Naturals.injective.succ with sameLength88      have firstBound : 0 < length{A}(a :: tail)89        rw length.cons90        arith91      have heads := entries with 0, Naturals.constructor.zero, firstBound92      rw [equal, listCoefficient.zero, listCoefficient.zero] at heads93      have restEntries : ∀ n, Nat(n) → n < length{A}(tail) → listCoefficient{A}(z, tail, n) = listCoefficient{A}(z, rest, n)94        intros n nNat bound95        have nextBound : succ(n) < length{A}(a :: tail)96          rw length.cons97          arith98        have values := entries with succ(n), nextBound99        rwa [equal, listCoefficient.succ, listCoefficient.succ] at values100      have tails := ih with rest, restList, lengths, restEntries101      rw equal102      cc103104theorem listSupport.exists_index (A z : Set) (xs : List(A))105  shows ∀ a ∈ listSupport{A}(xs), ∃ n, Nat(n) ∧ n < length{A}(xs) ∧ listCoefficient{A}(z, xs, n) = a106proof107  induction xs108  | List.nil =>109    intros a ha110    rw listSupport at ha111    exfalso112    exact set.empty with ha113  | List.cons(b, tail) using ih =>114    intros a ha115    have headIn : b ∈ A by assumption116    rw listSupport at ha117    have alternatives := insert.membership.forward with ha118    cases alternatives with head | rest119    . have bound : 0 < length{A}(b :: tail)120        rw length.cons121        arith122      refine ⟨0, Naturals.constructor.zero, bound, ?_⟩123      rw listCoefficient.zero124      cc125    . obtain ⟨n, nNat, bound, value⟩ := ih with a, rest126      have next : Nat(succ(n)) by typecheck127      have nextBound : succ(n) < length{A}(b :: tail)128        rw length.cons129        arith130      refine ⟨succ(n), next, nextBound, ?_⟩131      rwa listCoefficient.succ132133theorem listEntries.surjective (A z : Set) (xs : List(A))134  shows SurjectiveBetween(listEntries(A, z, xs), length{A}(xs), listSupport{A}(xs))135proof136  have function := listEntries.function at A, z, xs with *137  have cover := listSupport.exists_index at A, z, xs with *138  unfold SurjectiveBetween139  refine ⟨function, ?_⟩140  intros a ha141  obtain ⟨n, nNat, bound, value⟩ := cover with a, ha142  have position : n ∈ length{A}(xs) by exact membership.of_Less at n, length{A}(xs) with nNat, bound143  have entry := listEntries.value at A, z, xs, n with *144  have graph := FunctionBetween.relates_apply with *145  refine ⟨n, position, ?_⟩146  rwa [entry, value] at graph147