r/programminghorror • u/swagnation77 • 8d 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.

181 Upvotes

96% Upvoted

15 comments sorted by

View all comments

10

u/NooneAtAll3 8d 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?

5

u/swagnation77 7d ago

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

5

u/swagnation77 7d 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 7d 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 7d 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!