Grace/Core/List.g17

Open in Workbench Download source

Imports

Grace.Core.Data

Declarations

• List.cases theorem derivation
• length.nil theorem derivation
• length.cons theorem derivation
• append.left_unit theorem derivation
• append.associative theorem derivation

Source

1-- Shared list facts. The sole List datatype and executable operations live in Data.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore. Apache License 2.0; see LICENSE.4-- Authors: Grant Passmore56module Grace.Core.List7import Grace.Core.Data8export open Grace.Core.Data910theorem List.cases (A : Set) (xs : List(A))11  shows xs = List.nil ∨ ∃ x ∈ A, ∃ tail, List(A, tail) ∧ xs = x :: tail12proof13  induction xs14  | List.nil =>15    left16    rfl17  | List.cons(x, tail) using ih =>18    right19    refine ⟨x, assumption, tail, assumption, rfl⟩202122theorem length.nil (A : Set)23  shows length{A}([]) = 024proof25  simp [length]2627theorem length.cons (A x : Set) (xs : List(A))28  requires element : x ∈ A29  shows length{A}(x :: xs) = succ(length{A}(xs))30proof31  simp [length]3233-- append(ys, xs) traverses xs and places ys after it (the existing API).34theorem append.left_unit {A : Set} (ys : List(A))35  shows append(ys, []) = ys36proof37  simp [append]3839theorem append.associative {A : Set} (zs ys xs : List(A))40  shows append(zs, append(ys, xs)) = append(append(zs, ys), xs)41proof42  induction xs43  | List.nil => simp [append]44  | List.cons(x, tail) using ih => simp [append, ih]45