want: good first issue for cslib

Stream: computer science

[TongKe Xue]

I've done some toy lean4 proof screencasts at https://www.youtube.com/@tongkexue ; am looking to start writing "serious" proofs; believe my interests match cslib better than mathlib and am looking for low hanging fruits at https://github.com/leanprover/cslib

Is there a list of

1. good first issue (did not find in superficial search)
2. things to prove (cloned repo, rg sorry brought up two comments)
3. roadmap of things to prove

At this point, I'm not sure what to hack on / what there is to contrib, since until a notion of running time is decided on, we can't really do things involve measuring time, so this eliminates things like

1. NP-completeness reductions (need to prove reduction is polynomial time)
2. crypto proofs of the form "suppose you can break our protocol in poly time, using it as a blackbox, we can build algorihm that breaks known-hard-problem in poly time" (again, need polytime proof)
3. much of CLRS (besides counting number of comparisons in sorting; almost everything else involves running time analysis)

Thanks!

Other things I have in mind that might be interesting, even in the absence of running time are:

1. Chris Okasaki's purely functional data structures books
2. Raft / Paxos protocols ?
3. Proving "durability" of leveldb / sstable design, even in the event of crashes, by showing that it can be terminated at any step, and the "recovery algorithm" does the right thing
4. Maybe proving write-ahead-log design (again, against crashes).

Anyway, if someone could point me at theorems in cslib that need proofs (and provable in < 1000 lines), that would be very helpful. Thanks!

[Shreyas Srinivas]

Try verified functional algorithms in Isabelle.

[TongKe Xue]

I can't find a "Verified Functional Algorithms in Isabelle" book. Are you referring to a course ? (There are quite a few verification courses in Isabelle, but not sure which one you are referring to.)

There is a "Verified Functional Algorithms" (in Coq) https://softwarefoundations.cis.upenn.edu/vfa-current/Perm.html part of the https://softwarefoundations.cis.upenn.edu/ series at upenn.

What do you have in mind for turning this into a cslib contrib, porting the proofs from Coq to Lean4 ?

[Shreyas Srinivas]

Here’s a link to the book : https://www21.in.tum.de/~eberlm/pdfs/algorithms_survey.pdf

I think functional algorithms are a valid paradigm of algorithms and have pedagogical value. In a way they are understudied on the Algorithms side but fairly relevant on the functional programming side.

[Shreyas Srinivas]

You could also port the Rocq version by Chauguerrard

[Shreyas Srinivas]

Sorry wrong link. I’ll find the right one when I have a proper machine in front of me

[Bolton Bailey]

I'll mention this because it seems related to the OP's question: I think that the theorem that polynomial time functions as defined by Turing.TM2ComputableInPolyTime compose is probably within reach from content already defined in Mathlib, so that could be a good first project in the direction of complexity theory (although I'm not sure whether the result would better go in Mathlib or CSLib)

[TongKe Xue]

It's entirely possible I'm misunderstand what you are proposing -- but under your model, do we need to express reductions in terms of turing machines ?

IIRC the classic for NP completeness reductions is https://www.amazon.com/Computers-Intractability-NP-Completeness-Mathematical-Sciences/dp/0716710455 ; where most of the reductions are expressed in 1-3 paragraphs; probably < 50 lines of OCaml/Haskell.

My concern here is that in the absence of a higher level language (that we can also reason about runtime in), we would have to express these reductions in Turing Machines ... which would be brutal. :-)

However, I'm new to lean. Entirely possible I misunderstood what you're suggesting. Let me know is I misinterpreted.

[Bolton Bailey]

TongKe Xue said:

It's entirely possible I'm misunderstand what you are proposing -- but under your model, do we need to express reductions in terms of turing machines ?

Yes, this is what I was proposing, I don't think CSLib has a model for polynomial time computations yet (other than the sense in which you can import TM2ComputableInPolyTime from Mathlib). If you think another model will be more convenient you will have to wait for someone to write one or make it yourself.

Certainly your concern is shared that expressing reductions in Turing machines would require a lot of work, I guess I don't understand what would be harder about Turing Machines than any other model of computation.

[TongKe Xue]

I have (with some LLM help, but manually verified it myself) translated the basic exercises (will do advanced ones later) of https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html from Coq to Lean4.

I intend to translate all of https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html

I'm wondering if someone could invest some time and tell me everything I'm doing wrong / need to fix in order to (hopefully) start contributing to CSLib. If the Appel / Coq "Software Foundations / Verified Functional Algorithms" is not a good content match, I'll do it in a separate github repo.

Thanks!

namespace InsertSort

def insert (t : Nat) (l : List Nat) : List Nat :=
  match l with
  | [] => [t]
  | x :: xs => if t <= x
               then t :: x ::xs
               else x :: insert t xs

def sort : List Nat -> List Nat
  | [] => []
  | x :: xs => insert x (sort xs)

inductive Sorted : List Nat → Prop where
  | nil   : Sorted []
  | single (x : Nat) : Sorted [x]
  | cons   (x y : Nat) (l : List Nat) :
      x ≤ y → Sorted (y :: l) → Sorted (x :: y :: l)

def is_a_sorting_algorithm (f : List Nat → List Nat) : Prop :=
  ∀ l, List.Perm (f l) l ∧ Sorted (f l)

theorem insert_sorted (t: Nat) (l : List Nat) (hl: Sorted l) : Sorted (insert t l) := by
  induction l generalizing t with
  | nil => exact Sorted.single t
  | cons x xs ih =>
      cases hl with
      |single x =>
        rw [insert]
        by_cases htx : t ≤ x
        .
          rw [if_pos htx]; exact Sorted.cons t x [] htx (Sorted.single x)
        .
          rw [if_neg htx]; exact Sorted.cons x t [] (Nat.le_of_not_le htx) (Sorted.single t)
      |cons _ y tl hxy htl =>
         rw [insert]
         by_cases htx : t ≤ x
         . -- t ≤ x
           rw [if_pos htx]; apply Sorted.cons t x (y :: tl) htx (Sorted.cons x y tl hxy htl)
         . -- t > x
           rw [if_neg htx, insert]
           have h4 := ih t htl
           by_cases hty : t ≤ y
           . -- t ≤ y
             rw [if_pos hty]
             apply Sorted.cons x t (y :: tl) (Nat.le_of_not_le htx) _
             apply Sorted.cons t y tl hty htl
           . -- t > y
             rw [if_neg hty]
             simp [insert, if_neg hty] at h4
             apply Sorted.cons x y (insert t tl) hxy h4

theorem sort_sorted (l : List Nat) : Sorted (sort l) := by
  induction l with
  | nil => exact Sorted.nil
  | cons x xs ih => exact insert_sorted x (sort xs) ih

theorem insert_perm (t : Nat) (l : List Nat) : List.Perm (t :: l) (insert t l) := by
  induction l with
  | nil => unfold insert; simp
  | cons x xs ih =>
      unfold insert;
      by_cases htx : t ≤ x
      .
        rw [if_pos htx]
      .
        rw [if_neg htx]
        apply List.Perm.trans (l₂ := x :: t :: xs )
          (List.Perm.swap x t xs)
          (List.Perm.cons x ih)

theorem sort_perm (l : List Nat) : List.Perm l (sort l) := by
  induction l with
  | nil => unfold sort; simp
  | cons x xs ih =>
      unfold sort;
      apply List.Perm.trans (l₂ := x :: (sort xs)) (List.Perm.cons x ih) (insert_perm _ _)

theorem insertion_sort_correct : is_a_sorting_algorithm sort := by
  intro lst
  apply And.intro (sort_perm lst).symm (sort_sorted lst)


end InsertSort