Grace/Cumulus/List/Basic.g17

Open in Workbench Download source

Imports

Append · Reverse

Declarations

Source

1-- Heads, tails, constructor laws, the equation lemmas of mapping,2-- reversal, and support that the remaining list modules rewrite with, and3-- the image of a set of lists under a fixed cons4-- 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.Basic10import Append11import Reverse1213-- A Boolean choice between two sets; list recursions branch through it.14def boolChoice (test : Bool, yes no : Set) → Set15  | Bool.false, yes, no => no16  | Bool.true, yes, no => yes1718theorem boolChoice.false (yes no : Set)19  shows boolChoice(Bool.false, yes, no) = no20proof21  simp [boolChoice]2223theorem boolChoice.true (yes no : Set)24  shows boolChoice(Bool.true, yes, no) = yes25proof26  simp [boolChoice]2728-- Constructor laws.29theorem List.cons_ne_nil (A a : Set) (xs : List(A))30  requires element : a ∈ A31  shows a :: xs ≠ []32proof33  intro equal34  symm at equal35  have distinct := List.inductive.disjoint.nil.cons at a, xs36  exact distinct with equal3738theorem List.nil_ne_cons (A a : Set) (xs : List(A))39  requires element : a ∈ A40  shows [] ≠ a :: xs41proof42  exact List.inductive.disjoint.nil.cons at a, xs4344theorem List.cons_injective (A a b : Set) (xs ys : List(A))45  requires element : a ∈ A46  requires other : b ∈ A47  requires equal : a :: xs = b :: ys48  shows a = b ∧ xs = ys49proof50  exact List.inductive.injective.cons with equal5152theorem List.cons_head (A a b : Set) (xs ys : List(A))53  requires element : a ∈ A54  requires other : b ∈ A55  requires equal : a :: xs = b :: ys56  shows a = b57proof58  have both := List.cons_injective with equal59  exact both.left6061theorem List.cons_tail (A a b : Set) (xs ys : List(A))62  requires element : a ∈ A63  requires other : b ∈ A64  requires equal : a :: xs = b :: ys65  shows xs = ys66proof67  have both := List.cons_injective with equal68  exact both.right6970theorem List.closed_cons (A a : Set) (xs : List(A))71  requires element : a ∈ A72  shows List(A, a :: xs)73proof74  typecheck7576-- Length.77theorem length.eq_zero (A : Set) (xs : List(A))78  requires zero : length{A}(xs) = 079  shows xs = []80proof81  have shape := List.cases with *82  cases shape with empty | nonempty83  . exact empty84  . obtain ⟨a, element, tail, tailList, equal⟩ := nonempty85    rw [equal, length.cons] at zero86    have distinct := Naturals.disjoint.zero.succ at length{A}(tail)87    exfalso88    symm at zero89    exact distinct with zero9091theorem length.nil_iff (A : Set) (xs : List(A))92  shows length{A}(xs) = 0 ↔ xs = []93proof94  constructor95  . intro zero96    exact length.eq_zero with zero97  . intro empty98    rw empty99    exact length.nil at A100101theorem length.cons_positive (A a : Set) (xs : List(A))102  requires element : a ∈ A103  shows 0 < length{A}(a :: xs)104proof105  rw length.cons106  arith107108theorem length.positive_of_ne_nil (A : Set) (xs : List(A))109  requires nonempty : xs ≠ []110  shows 0 < length{A}(xs)111proof112  have shape := List.cases with *113  cases shape with empty | cons114  . exfalso115    exact nonempty with empty116  . obtain ⟨a, element, tail, tailList, equal⟩ := cons117    rw equal118    exact length.cons_positive with element119120theorem List.ne_nil_of_length_positive (A : Set) (xs : List(A))121  requires positive : 0 < length{A}(xs)122  shows xs ≠ []123proof124  intro empty125  rw [empty, length.nil] at positive126  exact Less.irreflexive with Naturals.constructor.zero, positive127128theorem length.positive_iff (A : Set) (xs : List(A))129  shows 0 < length{A}(xs) ↔ xs ≠ []130proof131  constructor132  . intro positive133    exact List.ne_nil_of_length_positive with positive134  . intro nonempty135    exact length.positive_of_ne_nil with nonempty136137theorem length.singleton (A a : Set)138  requires element : a ∈ A139  shows length{A}(a :: []) = 1140proof141  simp [length]142143-- Heads and tails.144theorem listTail.nil (A : Set)145  shows listTail{A}([]) = []146proof147  simp [listTail]148149theorem listTail.cons (A a : Set) (xs : List(A))150  requires element : a ∈ A151  shows listTail{A}(a :: xs) = xs152proof153  simp [listTail]154155theorem listHeadOr.nil (A z : Set)156  shows listHeadOr{A}(z, []) = z157proof158  simp [listHeadOr]159160theorem listHeadOr.cons (A z a : Set) (xs : List(A))161  requires element : a ∈ A162  shows listHeadOr{A}(z, a :: xs) = a163proof164  simp [listHeadOr]165166theorem listHeadOr.mem_carrier (A z : Set) (xs : List(A))167  requires default : z ∈ A168  shows listHeadOr{A}(z, xs) ∈ A169proof170  have shape := List.cases with *171  cases shape with empty | cons172  . rw [empty, listHeadOr.nil]173    exact default174  . obtain ⟨a, element, tail, tailList, equal⟩ := cons175    rw [equal, listHeadOr.cons]176    exact element177178theorem listHeadOr.mem_support (A z : Set) (xs : List(A))179  requires nonempty : xs ≠ []180  shows listHeadOr{A}(z, xs) ∈ listSupport{A}(xs)181proof182  have shape := List.cases with *183  cases shape with empty | cons184  . exfalso185    exact nonempty with empty186  . obtain ⟨a, element, tail, tailList, equal⟩ := cons187    rw [equal, listHeadOr.cons, listSupport.cons]188    exact insert.self189190theorem List.head_tail (A z : Set) (xs : List(A))191  requires nonempty : xs ≠ []192  shows xs = listHeadOr{A}(z, xs) :: listTail{A}(xs)193proof194  have shape := List.cases with *195  cases shape with empty | cons196  . exfalso197    exact nonempty with empty198  . obtain ⟨a, element, tail, tailList, equal⟩ := cons199    rw [equal, listHeadOr.cons, listTail.cons]200    rfl201202theorem listTail.length (A : Set) (xs : List(A))203  requires nonempty : xs ≠ []204  shows succ(length{A}(listTail{A}(xs))) = length{A}(xs)205proof206  have shape := List.cases with *207  cases shape with empty | cons208  . exfalso209    exact nonempty with empty210  . obtain ⟨a, element, tail, tailList, equal⟩ := cons211    rw [equal, listTail.cons, length.cons]212    rfl213214theorem listTail.support_subset (A : Set) (xs : List(A))215  shows listSupport{A}(listTail{A}(xs)) ⊆ listSupport{A}(xs)216proof217  have shape := List.cases with *218  cases shape with empty | cons219  . rw [empty, listTail.nil]220    exact Subset.reflexive at listSupport{A}([])221  . obtain ⟨a, element, tail, tailList, equal⟩ := cons222    rw [equal, listTail.cons, listSupport.cons]223    intros y hy224    exact insert.contains with hy225226-- Append.227theorem append.closed (A : Set) (xs ys : List(A))228  shows List(A, append(ys, xs))229proof230  typecheck231232theorem append.nil (A : Set) (ys : List(A))233  shows append(ys, []) = ys234proof235  simp [append]236237theorem append.cons (A a : Set) (xs ys : List(A))238  requires element : a ∈ A239  shows append(ys, a :: xs) = a :: append(ys, xs)240proof241  simp [append]242243theorem append.singleton (A a : Set) (ys : List(A))244  requires element : a ∈ A245  shows append(ys, a :: []) = a :: ys246proof247  simp [append]248249theorem append.eq_nil (A : Set) (xs ys : List(A))250  requires empty : append(ys, xs) = []251  shows xs = [] ∧ ys = []252proof253  have lengths : length{A}(append(ys, xs)) = 0254    rw empty255    exact length.nil at A256  rw length.append at lengths257  have both := add.eq_zero with lengths258  obtain ⟨xsZero, ysZero⟩ := both259  constructor260  . exact length.eq_zero with xsZero261  . exact length.eq_zero with ysZero262263theorem append.nil_iff (A : Set) (xs ys : List(A))264  shows append(ys, xs) = [] ↔ xs = [] ∧ ys = []265proof266  constructor267  . intro empty268    exact append.eq_nil with empty269  . intro both270    obtain ⟨xsNil, ysNil⟩ := both271    rw [xsNil, ysNil]272    simp [append]273274theorem append.length_left_le (A : Set) (xs ys : List(A))275  shows length{A}(xs) ≤ length{A}(append(ys, xs))276proof277  rw length.append278  arith279280theorem append.length_right_le (A : Set) (xs ys : List(A))281  shows length{A}(ys) ≤ length{A}(append(ys, xs))282proof283  rw length.append284  arith285286theorem append.left_nil_of_eq (A : Set) (xs ys : List(A))287  requires equal : append(ys, xs) = xs288  shows ys = []289proof290  have lengths : length{A}(append(ys, xs)) = length{A}(xs)291    rw equal292    rfl293  rw length.append at lengths294  have padded : length{A}(xs) + length{A}(ys) = length{A}(xs) + 0295    rw add.right_unit296    exact lengths297  have zero := add.left_cancel with padded298  exact length.eq_zero with zero299300theorem append.right_nil_of_eq (A : Set) (xs ys : List(A))301  requires equal : append(ys, xs) = ys302  shows xs = []303proof304  have lengths : length{A}(append(ys, xs)) = length{A}(ys)305    rw equal306    rfl307  rw length.append at lengths308  have padded : length{A}(xs) + length{A}(ys) = 0 + length{A}(ys)309    rw add.left_unit310    exact lengths311  have zero := add.right_cancel with padded312  exact length.eq_zero with zero313314-- Support.315theorem listSupport.mem_cons_self (A a : Set) (xs : List(A))316  requires element : a ∈ A317  shows a ∈ listSupport{A}(a :: xs)318proof319  rw listSupport.cons320  exact insert.self321322theorem listSupport.mem_cons_of_mem (A a y : Set) (xs : List(A))323  requires element : a ∈ A324  requires member : y ∈ listSupport{A}(xs)325  shows y ∈ listSupport{A}(a :: xs)326proof327  rw listSupport.cons328  exact insert.contains with member329330theorem listSupport.mem_cons_iff (A a y : Set) (xs : List(A))331  requires element : a ∈ A332  shows y ∈ listSupport{A}(a :: xs) ↔ y = a ∨ y ∈ listSupport{A}(xs)333proof334  rw listSupport.cons335  exact insert.membership at y, a, listSupport{A}(xs)336337theorem listSupport.mem_append_iff (A y : Set) (xs ys : List(A))338  shows y ∈ listSupport{A}(append(ys, xs)) ↔339    y ∈ listSupport{A}(xs) ∨ y ∈ listSupport{A}(ys)340proof341  rw listSupport.append342  exact union2.membership at y, listSupport{A}(xs), listSupport{A}(ys)343344theorem listSupport.mem_append_left (A y : Set) (xs ys : List(A))345  requires member : y ∈ listSupport{A}(xs)346  shows y ∈ listSupport{A}(append(ys, xs))347proof348  rw listSupport.append349  simp350351theorem listSupport.mem_append_right (A y : Set) (xs ys : List(A))352  requires member : y ∈ listSupport{A}(ys)353  shows y ∈ listSupport{A}(append(ys, xs))354proof355  rw listSupport.append356  simp357358theorem listSupport.singleton (A a : Set)359  requires element : a ∈ A360  shows listSupport{A}(a :: []) = {a}361proof362  simp [listSupport]363  ext y364  simp365366theorem listSupport.eq_empty (A : Set) (xs : List(A))367  requires empty : listSupport{A}(xs) = ∅368  shows xs = []369proof370  have shape := List.cases with *371  cases shape with nil | cons372  . exact nil373  . obtain ⟨a, element, tail, tailList, equal⟩ := cons374    have member : a ∈ listSupport{A}(xs)375      rw equal376      exact listSupport.mem_cons_self with element377    rw empty at member378    exfalso379    exact set.empty with member380381theorem listSupport.empty_iff (A : Set) (xs : List(A))382  shows listSupport{A}(xs) = ∅ ↔ xs = []383proof384  constructor385  . intro empty386    exact listSupport.eq_empty with empty387  . intro nil388    rw nil389    exact listSupport.nil at A390391theorem listSupport.nonempty_of_ne_nil (A : Set) (xs : List(A))392  requires nonempty : xs ≠ []393  shows ∃ y, y ∈ listSupport{A}(xs)394proof395  have shape := List.cases with *396  cases shape with nil | cons397  . exfalso398    exact nonempty with nil399  . obtain ⟨a, element, tail, tailList, equal⟩ := cons400    witness a401    rw equal402    exact listSupport.mem_cons_self with element403404-- Reversal.405theorem reverse.nil (A : Set)406  shows reverse{A}([]) = []407proof408  simp [reverse]409410theorem reverse.cons (A a : Set) (xs : List(A))411  requires element : a ∈ A412  shows reverse(a :: xs) = append(a :: [], reverse(xs))413proof414  simp [reverse]415416theorem reverse.closed (A : Set) (xs : List(A))417  shows List(A, reverse(xs))418proof419  typecheck420421theorem reverse.snoc (A a : Set) (xs : List(A))422  requires element : a ∈ A423  shows reverse(append(a :: [], xs)) = a :: reverse(xs)424proof425  have single : List(A, a :: []) by typecheck426  have reversed : List(A, reverse(xs)) by typecheck427  rw [reverse.append, reverse.singleton, append.singleton]428  rfl429430theorem reverse.injective (A : Set) (xs ys : List(A))431  requires equal : reverse(xs) = reverse(ys)432  shows xs = ys433proof434  have doubled : reverse(reverse(xs)) = reverse(reverse(ys))435    rw equal436    rfl437  rw [reverse.involutive, reverse.involutive] at doubled438  exact doubled439440theorem reverse.eq_nil (A : Set) (xs : List(A))441  requires empty : reverse(xs) = []442  shows xs = []443proof444  have nilReversed : reverse{A}([]) = [] by simp [reverse]445  rw ← nilReversed at empty446  exact reverse.injective with empty447448theorem reverse.nil_iff (A : Set) (xs : List(A))449  shows reverse(xs) = [] ↔ xs = []450proof451  constructor452  . intro empty453    exact reverse.eq_nil with empty454  . intro nil455    rw nil456    simp [reverse]457458-- Every nonempty list ends with an element: the mirror image of List.cases.459theorem List.snoc_cases (A : Set) (xs : List(A))460  shows xs = [] ∨ ∃ a ∈ A, ∃ front, List(A, front) ∧ xs = append(a :: [], front)461proof462  have reversed : List(A, reverse(xs)) by typecheck463  have shape := List.cases with reversed464  cases shape with nil | cons465  . left466    exact reverse.eq_nil with nil467  . right468    obtain ⟨a, element, tail, tailList, equal⟩ := cons469    refine ⟨a, element, reverse(tail), ?_, ?_⟩470    . typecheck471    . have back : reverse(reverse(xs)) = reverse(a :: tail)472        rw equal473        rfl474      have single : List(A, a :: []) by typecheck475      rw [reverse.involutive, reverse.cons] at back476      rw back477      rfl478479-- Mapping.480theorem listMap.nil (A f : Set)481  shows listMap{A}(f, []) = []482proof483  simp [listMap]484485theorem listMap.cons (A f a : Set) (xs : List(A))486  requires element : a ∈ A487  shows listMap{A}(f, a :: xs) = f(a) :: listMap{A}(f, xs)488proof489  simp [listMap]490491theorem listMap.singleton (A f a : Set)492  requires element : a ∈ A493  shows listMap{A}(f, a :: []) = f(a) :: []494proof495  simp [listMap]496497theorem listMap.reverse (A B f : Set) (xs : List(A))498  requires function : f : A → B499  shows listMap{A}(f, reverse(xs)) = reverse{B}(listMap{A}(f, xs))500proof501  induction xs502  | List.nil =>503    rw [reverse.nil, listMap.nil, reverse.nil]504    rfl505  | List.cons(a, tail) using ih =>506    have element : a ∈ A by assumption507    have image := FunctionBetween.apply_closed with function, element508    have single : List(A, a :: []) by typecheck509    have reversed : List(A, reverse(tail)) by typecheck510    have mapped : List(B, listMap{A}(f, tail)) by exact listMap.closed with function511    have step := listMap.append at A, B, f, reverse(tail), a :: [] with function512    rw [reverse.cons, step, ih, listMap.singleton, listMap.cons, reverse.cons]513    rfl514515theorem listMap.identity (A : Set) (xs : List(A))516  shows listMap{A}(identity(A), xs) = xs517proof518  induction xs519  | List.nil => simp [listMap]520  | List.cons(a, tail) using ih =>521    have element : a ∈ A by assumption522    have value := identity.apply with element523    rw [listMap.cons, ih, value]524    rfl525526theorem listMap.congr (A f g : Set) (xs : List(A))527  requires agreement : ∀ x ∈ listSupport{A}(xs), f(x) = g(x)528  shows listMap{A}(f, xs) = listMap{A}(g, xs)529proof530  induction xs531  | List.nil =>532    intro agreement533    simp [listMap]534  | List.cons(a, tail) using ih =>535    intro agreement536    have element : a ∈ A by assumption537    have headIn := listSupport.mem_cons_self with element538    have head := agreement with a, headIn539    have rest : ∀ x ∈ listSupport{A}(tail), f(x) = g(x)540      intros x hx541      have member := listSupport.mem_cons_of_mem with element, hx542      exact agreement with x, member543    have tails := ih with rest544    rw [listMap.cons, listMap.cons, head, tails]545    rfl546547theorem listMap.eq_nil (A f : Set) (xs : List(A))548  requires empty : listMap{A}(f, xs) = []549  shows xs = []550proof551  have shape := List.cases with *552  cases shape with nil | cons553  . exact nil554  . obtain ⟨a, element, tail, tailList, equal⟩ := cons555    rw [equal, listMap.cons] at empty556    have distinct := List.inductive.disjoint.nil.cons at f(a), listMap{A}(f, tail)557    exfalso558    symm at empty559    exact distinct with empty560561theorem listMap.mem_support (A B f x : Set) (xs : List(A))562  requires function : f : A → B563  requires member : x ∈ listSupport{A}(xs)564  shows f(x) ∈ listSupport{B}(listMap{A}(f, xs))565proof566  induction xs567  | List.nil =>568    intro member569    rw listSupport.nil at member570    exfalso571    exact set.empty with member572  | List.cons(a, tail) using ih =>573    intro member574    have element : a ∈ A by assumption575    have image := FunctionBetween.apply_closed with function, element576    have mapped : List(B, listMap{A}(f, tail)) by exact listMap.closed with function577    have alternatives := listSupport.mem_cons_iff.forward with element, member578    rw [listMap.cons, listSupport.cons]579    cases alternatives with head | rest580    . rw head581      exact insert.self582    . have inner := ih with rest583      exact insert.contains with inner584585theorem listMap.support_subset (A B f : Set) (xs : List(A))586  requires function : f : A → B587  shows listSupport{B}(listMap{A}(f, xs)) ⊆ functionImage(f, listSupport{A}(xs), B)588proof589  induction xs590  | List.nil =>591    rw [listMap.nil, listSupport.nil]592    exact empty.subset593  | List.cons(a, tail) using ih =>594    have element : a ∈ A by assumption595    have image := FunctionBetween.apply_closed with function, element596    have mapped : List(B, listMap{A}(f, tail)) by exact listMap.closed with function597    rw [listMap.cons, listSupport.cons]598    intros y hy599    have alternatives := insert.membership.forward with hy600    cases alternatives with head | rest601    . rw head602      have headIn := listSupport.mem_cons_self with element603      exact functionImage.membership.backward with ⟨image, a, headIn, rfl⟩604    . have inner := ih with y, rest605      obtain ⟨yIn, x, hx, equal⟩ := functionImage.membership.forward with inner606      have member := listSupport.mem_cons_of_mem with element, hx607      exact functionImage.membership.backward with ⟨yIn, x, member, equal⟩608609theorem listMap.support (A B f : Set) (xs : List(A))610  requires function : f : A → B611  shows listSupport{B}(listMap{A}(f, xs)) = functionImage(f, listSupport{A}(xs), B)612proof613  have forward := listMap.support_subset with function614  apply Subset.antisymmetric with forward615  intros y hy616  obtain ⟨yIn, x, hx, equal⟩ := functionImage.membership.forward with hy617  rw equal618  exact listMap.mem_support with function, hx619620-- The head and tail of a list over A.621theorem List.cons_parts (A x xs : Set)622  requires list : List(A, x :: xs)623  shows x ∈ A ∧ List(A, xs)624proof625  have shape := List.cases at A, x :: xs with list626  cases shape with isNil | isCons627  . exfalso628    have distinct := List.inductive.disjoint.nil.cons at x, xs629    symm at isNil630    exact distinct with isNil631  . obtain ⟨y, hy, tail, tailList, equal⟩ := isCons632    obtain ⟨headEqual, tailEqual⟩ :=633      List.inductive.injective.cons with equal634    rw [headEqual, tailEqual]635    exact ⟨hy, tailList⟩636637-- The lists of a set S with a fixed entry prepended.638def consImage (x S : Set) : Set := { x :: ys | ys ∈ S }639