-----Description-----
This task requires writing a Lean 4 function that computes the longest common subsequence (LCS) of two input strings.
A subsequence of a string is a sequence that can be derived from the original string by deleting zero or more characters (not necessarily contiguous) without changing the order of the remaining characters.
The function should return a string that is:
1) A subsequence of both input strings.
2) As long as possible among all such common subsequences.

If multiple LCS answers exist (with the same maximum length), returning any one of them is acceptable.

-----Input-----
s1: The first input string.
s2: The second input string.

-----Output-----
A string representing a longest common subsequence of s1 and s2.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def longestCommonSubsequence_precond (s1 : String) (s2 : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
partial def toCharList (s : String) : List Char :=
  s.data

partial def fromCharList (cs : List Char) : String :=
  cs.foldl (fun acc c => acc.push c) ""

partial def lcsAux (xs : List Char) (ys : List Char) : List Char :=
  match xs, ys with
  | [], _ => []
  | _, [] => []
  | x :: xs', y :: ys' =>
    if x == y then
      x :: lcsAux xs' ys'
    else
      let left  := lcsAux xs' (y :: ys')
      let right := lcsAux (x :: xs') ys'
      if left.length >= right.length then left else right
-- !benchmark @end code_aux


def longestCommonSubsequence (s1 : String) (s2 : String) (h_precond : longestCommonSubsequence_precond (s1) (s2)) : String :=
  -- !benchmark @start code
  let xs := toCharList s1
  let ys := toCharList s2
  let resultList := lcsAux xs ys
  fromCharList resultList
  -- !benchmark @end code


-- !benchmark @start postcond_aux
-- !benchmark @end postcond_aux


@[reducible]
def longestCommonSubsequence_postcond (s1 : String) (s2 : String) (result: String) (h_precond : longestCommonSubsequence_precond (s1) (s2)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq (arr : List Char) := (arr.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let subseqA := allSubseq s1.toList
  let subseqB := allSubseq s2.toList
  let commonSubseq := subseqA.filter (fun l => subseqB.contains l)
  commonSubseq.contains result.toList ∧ commonSubseq.all (fun l => l.length ≤ result.length)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem longestCommonSubsequence_spec_satisfied (s1: String) (s2: String) (h_precond : longestCommonSubsequence_precond (s1) (s2)) :
    longestCommonSubsequence_postcond (s1) (s2) (longestCommonSubsequence (s1) (s2) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s1: abcde
s2: ace
s1: aaaa
s2: bbaaa
s1: xyz
s2: abc
s1: axbxc
s2: abxc
s1: AGGTAB
s2: GXTXAYB
expected: ace
aaa
abxc
GTAB
unexpected: ab
abc
bce
aaaaa
b
aaab
x
y
a
abc
axc
abcx
GGTAB
AGGTA

Inputs rejected by the precondition: