r/programminghorror • u/swagnation77 • 2d ago

Lean4 Finally solved Two Sum!

Somehow my code is so horrifying, Lean4 is able to evaluate it, the LSP says it works and the compiler gives an error. It is theoretically correct and the kernel accepts it, but the compiler isn't able to produce anything out of it. My awful code discovered a bug in Lean's compiler.

143 Upvotes

95% Upvoted

15 comments sorted by

98

u/MistakeIndividual690 2d ago

I don’t know what Lean is but what for the love of god is this…

TwoSum is like eight lines in Python

But this is clearly the perfect post for this sub

81

u/swagnation77 2d ago

Thanks! I tried to make the code as ugly as possible for this sub.

Explanation (boring alert):
Lean4 is a theorem checker, meaning you can prove things in code, and the compiler checks whether its a valid proof or not.
What I did was essentially a proof by exhaustion of a naive implementation of TwoSum.
Since the algorithm checks all possible pairs of numbers, meaning that if the algorithm finds a pair, that pair is the solution, otherwise there is no solution at all.
The algorithm then (if successful) returns a pair and a proof that the pair is the solution.
Somehow, whilst trying to make this code uglier I discovered a bug in the Lean compiler that allowed me to have a well-typed expression without the compiler knowing how to produce code for it. It allows me to evaluate expressions, but not compile them.

8

u/TLJGame 2d ago

The what I’m assuming are variable names just makes this 10x worse

7

u/swagnation77 2d ago

I'm sorry.

1

u/GoddammitDontShootMe [ $[ $RANDOM % 6 ] == 0 ] && rm -rf / || echo “You live” 1d ago

I never heard of either TwoSum or Lean4.

3

u/MistakeIndividual690 1d ago

https://leetcode.com/problems/two-sum/

1

u/GoddammitDontShootMe [ $[ $RANDOM % 6 ] == 0 ] && rm -rf / || echo “You live” 1d ago

I've never done leetcode before, so that would explain why.

33

u/JAMIEISSLEEPWOKEN 2d ago

……you want a hashmap…?

14

u/swagnation77 2d ago

lmao yeah if I did a hashmap the solution would've been better, but the proofs would've taken me 10x as long. (I spent two days on a single algorithm)

6

u/NooneAtAll3 1d ago

am I reading Lean problem statement correctly? when you return some(), you are not guaranteeing that it's the returned indexes that sum to the target, only that some such indexes exist?

3

u/swagnation77 1d ago

Damn good catch, such a dumb mistake on my end. I will update it to match the correct specification, thanks!

2

u/swagnation77 1d ago

Yeah so some _ => (∃ p : Fin n × Fin n, v[p.1] + v[p.2] = target ∧ p.1 ≠ p.2) becomes: some p => (v[p.1] + v[p.2] = target ∧ p.1 ≠ p.2)

and matching on pairs in the some case returns a different constructor:
in the base case:
⟨some p, hsol⟩ => ⟨some (⟨0, h0⟩, p.2), hsol⟩
In the inductive case:
⟨some p, hsol⟩ => ⟨some (⟨i + 1, hip⟩, p.2), hsol⟩

which actually simplified my proof because I don't need to turn an already valid pair into a proof that a valid pair exists, I just have to propagate it.

2

u/NooneAtAll3 1d ago

by the way, have you tried experimenting with cpp-based syntax?

lean supports many styles, you don't have to only use python-esk whitespace-based nesting

1

u/swagnation77 1d ago

Never tried it but seems interesting. I'm still learning Lean so I have just been following convention. I don't really like Lean's default syntax so thanks for the tip!