Grace/Cumulus/List/Reverse.g17

Imports

Declarations

reverse.length theorem derivation
reverse.append theorem derivation
reverse.singleton theorem derivation
reverse.involutive theorem derivation
listSupport.reverse theorem derivation
Source

1-- Reversal of lists: length, interaction with concatenation, involution,2-- and the support3-- 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.Reverse9import Algebra.IndexedLists1011theorem reverse.length (A : Set) (xs : List(A))12  shows length{A}(reverse(xs)) = length{A}(xs)13proof14  induction xs15  | List.nil =>16    rw reverse17    rfl18  | List.cons(a, tail) using ih =>19    have element : a ∈ A by assumption20    have single : List(A, a :: []) by typecheck21    have reversed : List(A, reverse(tail)) by typecheck22    rw [reverse, length.append, ih, length.cons]23    simp [length, add.succ_right, add.right_unit]2425theorem reverse.append (A : Set) (xs ys : List(A))26  shows reverse(append(ys, xs)) = append(reverse(xs), reverse(ys))27proof28  induction xs29  | List.nil =>30    have reversed : List(A, reverse(ys)) by typecheck31    rw [append, reverse, append.right_unit]32    rfl33  | List.cons(a, tail) using ih =>34    have element : a ∈ A by assumption35    have single : List(A, a :: []) by typecheck36    have reversedTail : List(A, reverse(tail)) by typecheck37    have reversedYs : List(A, reverse(ys)) by typecheck38    have appended : List(A, append(ys, tail)) by typecheck39    have reversedAppended : List(A, reverse(append(ys, tail))) by typecheck40    rw [append, reverse, ih, reverse, append.associative]41    rfl4243theorem reverse.singleton (A a : Set)44  requires element : a ∈ A45  shows reverse{A}(a :: []) = a :: []46proof47  rw [reverse, reverse, append]48  rfl4950theorem reverse.involutive (A : Set) (xs : List(A))51  shows reverse(reverse(xs)) = xs52proof53  induction xs54  | List.nil =>55    rw [reverse, reverse]56    rfl57  | List.cons(a, tail) using ih =>58    have element : a ∈ A by assumption59    have single : List(A, a :: []) by typecheck60    have reversed : List(A, reverse(tail)) by typecheck61    have doubled : List(A, reverse(reverse(tail))) by typecheck62    rw [reverse, reverse.append, ih, reverse.singleton, append, append.left_unit]63    rfl6465theorem listSupport.reverse (A : Set) (xs : List(A))66  shows listSupport{A}(reverse(xs)) = listSupport{A}(xs)67proof68  induction xs69  | List.nil =>70    rw reverse71    rfl72  | List.cons(a, tail) using ih =>73    have element : a ∈ A by assumption74    have single : List(A, a :: []) by typecheck75    have reversed : List(A, reverse(tail)) by typecheck76    rw [reverse, listSupport.append, ih, listSupport.cons]77    ext y78    simp [listSupport, insert.membership, union2.membership]79