Day 5 Of Learning Lean

Day 5 of learning Lean

why is proving ¬(p ↔ ¬p) so hard

Of course with Truth tables and classical logic, this is near trivial to solve. In fact here's the proof

example : ¬(p ↔ ¬p) := Not.intro λ(Iff.intro pnp npp) => have hnp : ¬p := (imp_iff_not_or.mp pnp).elim id id have hp : p := npp hnp hnp.elim hp

Could be a lot shorter, especially at proving the (¬p ∨ ¬p) part. But you get the gist.

Unfortunately this line exists

imp_iff_not_or is apparently only in classical logic, because it relies on the law of excluded middle which is (p ∨ ¬p) which intuitionistic logic does not have as ¬p is defined as (p -> False).

right now I'm looking into modal logic for solutions and it seems promising, having translations from Intuitional to KT4 modal logic, though I still don't know how I could translate it to a lean solution. It's also very likely there is a simpler solution that I am not seeing.

Either way, it's pretty fun despite my frustrations.

So far still stuck at page 3 of theorem proving in lean 4, though I only have 1 problem to solve.

The best part of ricing is you can never know whether you will spend 14 hours fixing issues and by the end of the day your config looks almost exactly the same as before. Or try a hundred different programs and your config ends up looking nothing like the original.

Learning Haskell as my second language has heavily skewed my perspective on programming.

Curry-howard correspondence is a neat little thing.

Tuples are equivalent to And

Sum Types are equivalent to Or

atleast Exclusive Or I think, since you can't have an `Either p q` be both `Left p` and `Right q` at once. They'd need to be more like `Either a (Either b (a,b))`

Keep in mind that `a,b` can be any type, not just booleans. It's not so much a comparison as much as it just says if the type exists.

(Exists in the way there's a representation of it in code.)

For the longest time I just thought it was just some cool equivalence. I've never really utilized this concept until I've used Lean which actually utilizes this concept. Proving two statements are equivalent means creating an isomorphism between both of the types.

For example

Proving

(P ∨ Q) ∨ R = P ∨ (Q ∨ R)

Is similar to proving the Isomorphism

Either (Either P Q) R

<=> Either P (Either Q R)

(a <=> b is equal to a -> b and b <- a) btw

And

Proving

(P ∧ Q) ∧ R = P ∧ (Q ∧ R)

Is similar to making the Isomorphism

((P,Q),R) <=> (P,(Q,R))

(Though of course And is easier due to the inclusivity thing I mentioned earlier)

Hey so, Type Families and Propositional Type Equality in Haskell are pretty cool even if I mostly used them as hacks for Haskell not having dependent typing.

First time I've heavily used Data.Type.Equality.

Rewriting proofs with `trans` is significantly more tedious in compound types and results in quite a few functions to help guide the types.

Overall pretty fun experience. Lack of `rewrite` really does ruin a lot of the satisfaction though.

(I also made it into a Kata)

Codewars

Prove without Truth Tables

You are to prove the following equality: (p ∨ q) ⇒ r ≡ (p ⇒ r) ∧ (p ⇒ r) proof :: Bool p -&gt; Bool q -&gt; Bool r -&gt; (p || q) ==&gt;

Anyone else learn languages designed to be proof assistants? Or atleast designed with theorem proving as a usecase. Whilst barely knowing any pure Math?

When I first started learning Idris2, I had no idea how to even structure a proof. Needless to say I was quite lost, even if I was experienced in Haskell at that point.

Even now when I'm learning Lean, when I started which was about 5 days ago, I only knew how to prove with truth tables. It wasn't until yesterday when I found about the logics other than Classical.

So basically all I know about pure math is just me brute-forcing my way into learning languages like Idris as well as the occasional Haskell article or codewars kata ethat deep dives into a concept.

It wasn't until recently when I decided to finally sit down and learn Pure Math starting from basic Discrete Math. It's fun because I keep recognizing the concepts that's become commonplace in the languages I use. I learned about Connection intros and eliminations before knowing the difference between classical and intuitionistic logic.

What I'm saying is I love Curry-Howard correspondence