Lean4

40. Longest increasing subsequence

MediumProgramAcademy Pass20 points

A subsequence keeps some elements of a list in their original order, not necessarily next to each other. Write lengthOfLIS nums, the length of the longest subsequence of nums that is strictly increasing.

Examples

  1. InputlengthOfLIS [10, 9, 2, 5, 3, 7, 101, 18]Output4
  2. InputlengthOfLIS [0, 1, 0, 3, 2, 3]Output4
  3. InputlengthOfLIS [7, 7, 7, 7]Output1

Submitting also runs 9 hidden tests.

Constraints

  • Hidden tests include 2,000 numbers. O(n²) and faster methods pass; trying every subsequence does not.
dynamic programminglistsarrays

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Learn the ideas

Similar problems

Solution.lean
Loading…
Loading editor…
3#guard (lengthOfLIS [10, 9, 2, 5, 3, 7, 101, 18]) = (4)
4#guard (lengthOfLIS [0, 1, 0, 3, 2, 3]) = (4)
5#guard (lengthOfLIS [7, 7, 7, 7]) = (1)
examples

Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.

ReadyLn 1, Col 1Lean 4
Draft saved in this browser