Boolean expression experiment

Stream: general

[Steven Clontz]

@Brandon Sisler shared this Lean file with me as the foremost Lean expert on faculty at his institution. Which ain't saying much, so I thought moving the conversation here would be more productive in general. :upside_down:

-- Hello Dr.Clontz! I was reading up on how the some of the simplifying tactics work in Lean4 and found that it was remarably insightful into teaching students how to reduce logical statements. So I thought that I would write this up and send it along.
-- Document Start:
-- To begin we need to be specific about what a logical statement is. One thing it is not for instance is "I think therefore I am." I am just a computer and I do not understand how you want me to parse such a thing. Perhaps "IThink therefore IAM" is a little better, and even best would probably be "IThink ⇒ IAM." So the lesson is clear. A logical statment should have implications, on each end should be some variable (prop.) and there are some special variables which we will call True and False, each with their own unique features.

-- So let us say that a Boolean Expresion consists of
inductive BoolExpr where
  | var (name : String) -- variables, which have names (atomic statments)
  | val (b : Bool) -- special variables, T or F
  | implication  (p q : BoolExpr) -- an implication of other Boolean Expressions
  | not (p : BoolExpr) -- the negation of a Boolean Expression
  deriving Repr, BEq, DecidableEq

-- Okay great, so now we should discuss how these things aught to actually work. We have a few cases.

-- ⬝ T ⇒ T should be True
-- ⬝ T ⇒ F should be False
-- ⬝ F ⇒ T should be True
-- ⬝ F ⇒ F should be True
-- ⬝ P ⇒ T should be True
-- ⬝ P ⇒ F should be equivalent to ~ P
-- ⬝ T ⇒ P should be equivalent to P
-- and ~ should work in the typical way of flipping true to falses and falses to trues.

-- Lets do an example by hand (ugh.)
-- ~((T ⇒ (P ⇒ T)) ⇒ F)
-- To begin I look at the not, but there is really nothing I can do about it, and I wish to simplify what is inside first. Therefore, next I look at the first implication. I see that the implication ends in a false, which means that only the truth of the predicate matters (and its negation, see our chart).
  -- ⇒ ~ ~ (T ⇒ (P ⇒ T))
-- Now again I look at the interior again and we notice that the implication begins with true, so the truth value depends solely on the consequence.
  -- ⇒ ~ ~ (P ⇒ T)
-- Similairly here, we can recodnize that we only need care about the consequence.
  -- ⇒ ~ ~ T
-- At this point there is no longer anything to simplify for implications, so we look at the nots.
  -- ⇒ ~ F
-- and again,
  -- ⇒ T
--  et voila

-- Well that was exhasting, lets spend a few hours writing a simplifier so that we never have to do five minutes of work again.

def simplify (P : BoolExpr) : BoolExpr :=
match P with -- Let P be some Boolean Expression, which implies it is of one such form.
  | BoolExpr.not p => mkNot (simplify p) -- If we have ~ (T ⇒ T)  then we wish to write ~ T. That is we wish to simplify what is bracketed and then take the negation.
  | BoolExpr.implication p q => mkIm (simplify p) (simplify q) -- similairly we simplify the subimplications before the main implication.
  | e => e --everything else we just return as is
where
  mkNot : BoolExpr → BoolExpr --negates booleans
    |BoolExpr.val p => BoolExpr.val (¬ p)
    |p => BoolExpr.not p
  mkIm : BoolExpr → BoolExpr → BoolExpr --simplifies implications with T or F in them.
    | BoolExpr.val true, q => q
    | BoolExpr.val false, _ => BoolExpr.val True
    | _, BoolExpr.val true => BoolExpr.val true
    | p, BoolExpr.val false => BoolExpr.not p
    | p, q => BoolExpr.implication p q

-- There is one issue we still have, which is that it is difficult to write even simple statements. As an example,
-- T ⇒ T → BoolExpr.implication (BoolExpr.val true) (BoolExper.val true)
-- is expressed like this, which is already unmanagable. So we should start to define notation to make our lives easier.

-- Here we just define the notation so it is natural and protect some common variable names.
notation:65 lhs:65 " ⇒ " rhs:66 => BoolExpr.implication lhs rhs
notation:67 " ~ " rhs:40 => BoolExpr.not rhs
notation:max "T" => BoolExpr.val true
notation:max "F" => BoolExpr.val false

def atom (P : String) : BoolExpr := BoolExpr.var P --Lets you define your own atomic formulas.
-- Define an atomic proposition
def P := BoolExpr.var "P"
def Q := BoolExpr.var "Q"
notation:max "prop " P => BoolExpr.var P

-- And now, we can see our work in action.
#reduce simplify (~ ((T ⇒ (P ⇒ T)) ⇒ F))

#reduce simplify (~((T ⇒ T) ⇒ (~(F ⇒ T))))

-- And let us see where this tactic couls be improved. Consider
#reduce simplify (P ⇒ P)
-- We know this is a tautology, and yet our tactic does not know how to handle it! This is a common encounter in tactic writing. After all, we can always add features that do more, but which slow our program down. We also note that we can only handle implications and nots at the moment. But we have no way to speak about ors, ands, ect!

[Steven Clontz]

I've been nerd-baited into trying to add P⇒P simplifications, but as a relative novice it's going slow

[Eric Wieser]

Note that you can just write

#eval "lean code"

and Zulip will add a link to the top right that opens the web editor. It might make sense to edit that into your first message so that people don't need to leave Zulp.

[Eric Wieser]

Note that what you have written there is not a "tactic" in the usual lean sense of the word

[Brandon Sisler]

Thats true, but I wrote it for absolute beginners and I find the actual tactic notations to be just slightly harder to read than definitions. In my mind it "acts like" a tactic, and gives intuition into how you can automate irritating parts of proofs. On the other hand, perhaps it would be better for me to avoid using the word tactic, since I suppose the meaning is sort of protected.

[Eric Wieser]

One crucial way in which it does not act like a tactic is that it does not produce a proof!

[Brandon Sisler]

Aha, thats a good point! Yes, I'm convinced the wording aught to be changed now

[Eric Wieser]

(to elaborate on that: I can add | BoolExpr.val false => BoolExpr.val true and it clearly doesn't do what you want, but Lean won't protect you against it)

[Eric Wieser]

To prove that simplify is correct, you could define BoolExpr.eval vars : Bool, and prove that (simplify b).eval vars = b.eval vars

[Eric Wieser]

⬝ F ⇒ P should be equivalent to ~ P

This is not true classically, or in lean's logical framework; are you working in a weird logical system, or is this an error? It contradicts

-- ⬝ F ⇒ T should be True
-- ⬝ F ⇒ F should be True

[Eric Wieser]

Steven Clontz said:

I've been nerd-baited into trying to add P⇒P simplifications, but as a relative novice it's going slow

-| p, q => BoolExpr.implication p q
+| p, q => if p = q then T else BoolExpr.implication p q

is enough to do that

[Brandon Sisler]

Eric Wieser said:

⬝ F ⇒ P should be equivalent to ~ P

This is not true classically, or in lean's logical framework; are you working in a weird logical system, or is this an error?

Just an error there, but to save face I'll say its a weird logical system. And I like the suggestion for the proof, it would be a nice addition.

[Eric Wieser]

In your defence your implementation looks correct, and the comment was the only error

[Brandon Sisler]

Well there we have it, I have a marvelous bit of code but the margins of my text editor are simply too narrow for me to include correct information

[Steven Clontz]

Eric Wieser said:

Steven Clontz said:

I've been nerd-baited into trying to add P⇒P simplifications, but as a relative novice it's going slow

-| p, q => BoolExpr.implication p q
+| p, q => if p = q then T else BoolExpr.implication p q

is enough to do that

Thanks - that's what I had in my head but I was obviously overthinking how it'd be expressed in Lean

[Steven Clontz]

Eric Wieser said:

Note that you can just write

#eval "lean code"

and Zulip will add a link to the top right that opens the web editor. It might make sense to edit that into your first message so that people don't need to leave Zulp.

Took me a while to realize what you were saying here: in this Zulip every(?) code block has the feature to open the code in the web editor in one click, if you hover over it and click the external link icon. Neat.

[Eric Wieser]

Every code editor marked as lean (which is the default) gets this button. lean3 blocks get a similar link.

[Steven Clontz]

Anyway Brandon, who needs ANDs and ORs when you have NOTs and IMPLIESs? :grinning:

-- or
#reduce simplify ((~T)⇒ T) -- T
#reduce simplify ((~T)⇒ F) -- T
#reduce simplify ((~F)⇒ T) -- T
#reduce simplify ((~F)⇒ F) -- F
-- and
#reduce simplify (~(T⇒ ~T)) -- T
#reduce simplify (~(T⇒ ~F)) -- F
#reduce simplify (~(F⇒ ~T)) -- F
#reduce simplify (~(F⇒ ~F)) -- F

[Brandon Sisler]

We have logical operators at home!
The logical operators at home:

Steven Clontz said:

Anyway Brandon, who needs ANDs and ORs when you have NOTs and IMPLIESs? :grinning:

-- or
#reduce simplify ((~T)⇒ T) -- T
#reduce simplify ((~T)⇒ F) -- T
#reduce simplify ((~F)⇒ T) -- T
#reduce simplify ((~F)⇒ F) -- F
-- and
#reduce simplify (~(T⇒ ~T)) -- T
#reduce simplify (~(T⇒ ~F)) -- F
#reduce simplify (~(F⇒ ~T)) -- F
#reduce simplify (~(F⇒ ~F)) -- F

[Brandon Sisler]

Actually if you want them included you're in luck because that is going to be document two, where I add in not, and, or, and implication. Then you really get cooking with writing a super simplify.

[Brandon Sisler]

Heres an odd problem, I am not sure if it is possible to prove that simplify terminates (which I would actually need to prove what we discussed earlier, at least if I am doing things in a sensible way). After all if I have an expression p ⇒ q it will try and compute mkIm (simplify p) (simplify q) but what if p is an implication, and what if its components are implications. In principle I know that this is no issue because I must have entered a finite expression, and it is not turtles all the way down, so I do stop calling mkIm at some point. But the question is, does Lean realy know that, is it build into the inductive type somehow or is this really an instance in which we cannot prove the function terminates?

Disregard, got it