## Stream: new members

### Topic: CNF transformation of Propositional expressions

#### Alexandre Rademaker (Aug 28 2019 at 11:25):

In Lean 3, would it be possible to implement the CNF transformation of a propositional formula? How?

#### Patrick Massot (Aug 28 2019 at 11:27):

Isn't it part of what finish or tauto are doing?

#### Alexandre Rademaker (Aug 28 2019 at 11:29):

Not sure. But I am teaching a logic course in Lean using Avigad book and I want to show the students the CNF transformation, I thought that would be nice to implement it in Lean

#### Patrick Massot (Aug 28 2019 at 11:30):

I have no idea what I'm talking about, but you can have a look at the code of those tactics

#### Mario Carneiro (Aug 28 2019 at 11:48):

Yes, we've done that in class before

#### Mario Carneiro (Aug 28 2019 at 11:49):

The simple way is to use a carefully chosen simp set

#### Mario Carneiro (Aug 28 2019 at 11:50):

The more efficient way is to prove it by recursion on the term

#### Alexandre Rademaker (Aug 28 2019 at 12:12):

Hi Mario , can you share examples? It is still not clear to me how implement this kind of computation in Lean. Have you implemented it over the type Prop or implemented your on data type for formulas and functions over this type?

(deleted)

#### Mario Carneiro (Aug 28 2019 at 21:45):

Since I like to give this as an exercise, I won't give exactly CNF, but here's a similar implementation for NNF (negation normal form), which turns everything into 'and', 'or', and negations of propositional atoms.

Method 1, using simp:

import logic.basic

meta def nnf₁ : tactic unit :=
[simp only [iff_def, classical.imp_iff_not_or, not_or_distrib, classical.not_and_distrib]]

example (p q r s : Prop) : (p  (q  r)  (r  s))  p :=
by nnf₁ -- ⊢ (¬p ∨ (¬q ∨ r) ∧ (¬r ∨ s)) ∨ p

Method 2, by recursion:

theorem nnf.iff (p q r : Prop) (h : (p  q)  (q  p)  r) : (p  q)  r :=
by rw [ h, @iff_def p q]
theorem nnf.imp (p q r : Prop) (h : (¬ p  q)  r) : (p  q)  r :=
by rw [ h, classical.imp_iff_not_or]
theorem nnf.not_and (p q p' q' : Prop) (hp : ¬ p  p') (hq : ¬ q  q') : ¬ (p  q)  (p'  q') :=
by rw [ hp,  hq, classical.not_and_distrib]
theorem nnf.not_or (p q p' q' : Prop) (hp : ¬ p  p') (hq : ¬ q  q') : ¬ (p  q)  (p'  q') :=
by rw [ hp,  hq, not_or_distrib]
theorem nnf.and (p q p' q' : Prop) (hp : p  p') (hq : q  q') : (p  q)  (p'  q') := by rw [hp, hq]
theorem nnf.or (p q p' q' : Prop) (hp : p  p') (hq : q  q') : (p  q)  (p'  q') := by rw [hp, hq]

meta def nnf₂_aux : expr  expr × expr
| (%%a  %%b) :=
let (e, p) := nnf₂_aux (((%%a:Prop)  %%b)  ((%%b:Prop)  %%a)) in
(e, (nnf.iff %%a %%b %%e %%p))
| (%%a  %%b) :=
let (e, p) := nnf₂_aux (¬ %%a  %%b) in
(e, (nnf.imp %%a %%b %%e %%p))
| (%%a  %%b) :=
let (a', ha) := nnf₂_aux a, (b', hb) := nnf₂_aux b in
((%%a'  %%b'), (nnf.or %%a %%b %%a' %%b' %%ha %%hb))
| (%%a  %%b) :=
let (a', ha) := nnf₂_aux a, (b', hb) := nnf₂_aux b in
((%%a'  %%b'), (nnf.and %%a %%b %%a' %%b' %%ha %%hb))
| (¬ (%%a  %%b)) :=
let (a', ha) := nnf₂_aux (¬ %%a), (b', hb) := nnf₂_aux (¬ %%b) in
((%%a'  %%b'), (nnf.not_and %%a %%b %%a' %%b' %%ha %%hb))
| (¬ (%%a  %%b)) :=
let (a', ha) := nnf₂_aux (¬ %%a), (b', hb) := nnf₂_aux (¬ %%b) in
((%%a'  %%b'), (nnf.not_or %%a %%b %%a' %%b' %%ha %%hb))
| e := (e, (iff.refl %%e))

meta def nnf₂ : tactic unit :=
do e  tactic.target,
let (e', p) := nnf₂_aux e,
tactic.refine (@iff.mpr %%e %%e' %%p _)

example (p q r s : Prop) : (p  (q  r)  (r  s))  p :=
by nnf₂ -- ⊢ (¬p ∨ (¬q ∨ r) ∧ (¬r ∨ s)) ∨ p

#### Alexandre Rademaker (Aug 29 2019 at 13:42):

Thank you @Mario Carneiro ! In the first approach, I got the error

8:5: unknown identifier 'classical.imp_iff_not_or'
state:
p q r s : Prop
⊢ (p → (q → r) ∧ (r → s)) ∨ p

Where the symbol imp_iff_not_or is defined?

#### Alexandre Rademaker (Aug 29 2019 at 13:47):

Maybe this next question will sound silly, but I am being curious to ask. In cases such the one above, how can I find definitions in Lean? Using emacs, how can I know if a need to open a namespace or import some file? How can I know what is already in the Lean distribution?

#### Patrick Massot (Aug 29 2019 at 13:53):

I guess you don't have mathlib

#### Patrick Massot (Aug 29 2019 at 13:54):

In case where you know the exact name but clearly don't have the right imports I think nothing is faster than grep

#### Alexandre Rademaker (Aug 31 2019 at 22:34):

I guess I didn't understand how to install mathlib. In https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md it says that I need to install lean using elan. But I have already Lean and Emacs running fine. I just want to have mathlib but I don't know how.

#### Kevin Buzzard (Aug 31 2019 at 22:44):

If you're not doing it the community supported way then you don't just want to know how to install mathlib, you want to know how to install it, how to compile it and how to use it as a dependency in another project. The community have solved all these problems. Why don't you try it the community supported way first and then afterwards try and get it working with Emacs

#### Kevin Buzzard (Aug 31 2019 at 22:45):

The whole thing is still a mess but we have worked hard to write documentation that just works, or at least usually does

#### Kevin Buzzard (Aug 31 2019 at 22:46):

Once you see it all working the supported way you can try and switch back and then your problems will be far more precise

#### Mario Carneiro (Aug 31 2019 at 22:46):

I don't think installing mathlib directly is that technically challenging, it's just time consuming to compile

#### Mario Carneiro (Aug 31 2019 at 22:47):

and frankly, I am far happier to wait for lean to compile for an hour than spend a day doing installation troubleshooting

#### Mario Carneiro (Aug 31 2019 at 22:49):

the macos.md file is a bit strange to me... it doesn't say anything about mathlib itself

#### Alexandre Rademaker (Aug 31 2019 at 22:49):

Hi @Mario Carneiro , that is my point too. I just want to understand how to install mathlib considering that lean and emacs are already working together and I have been using Lean only for my course, not with other projects or dependencies.

#### Mario Carneiro (Aug 31 2019 at 22:53):

@Kevin Buzzard I think it is a problem if we don't have the "low tech" installation instructions available. There are various reasons why the "install a script that does everything" approach can fail (usually system configuration things, or paranoid people) and we should have a backup that just goes through the steps that the script is doing

#### Mario Carneiro (Aug 31 2019 at 22:55):

In particular, I'm not comfortable with the section that says to run:

curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

The containing section doesn't say anything precise about what the script is doing or how you can do it yourself

#### Mario Carneiro (Aug 31 2019 at 22:56):

(This will install tools that, amongst other things, let you download compiled binaries for mathlib.)

How do I use said tools? What tools? Where should I do this, and how will it affect my filesystem?

#### Mario Carneiro (Aug 31 2019 at 22:59):

The linux install instructions end with a link to https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md . The OSX instructions should probably also link there, and it looks like a good place to start once you have lean but not mathlib

#### Alexandre Rademaker (Aug 31 2019 at 23:03):

Yep. I am those paranoid people! :grinning:

Mario, I got

9:4: tactic failed, there are unsolved goals
state:
p q r s : Prop
(¬p  (¬q  r)  (¬r  s))  p

is that the expected output? If I understood it right, the approach is all done in the type level, rewriting the goal. It would be interesting to contrast it with the transformation been done in the term level, with the explicit manipulation of the terms. But for that, I guess I would need to define my own datatype for propositional logic formulas, right?

#### Mario Carneiro (Aug 31 2019 at 23:13):

The approach is to create a proof by recursion on the expr type

#### Mario Carneiro (Aug 31 2019 at 23:13):

and then hand it to lean

#### Mario Carneiro (Aug 31 2019 at 23:14):

It has to be done in meta land because directly interfacing with the elaborator is "untrusted"

#### Mario Carneiro (Aug 31 2019 at 23:14):

There isn't really an alternative if you want something that acts like a tactic

#### Mario Carneiro (Aug 31 2019 at 23:15):

But you can minimize the untrusted part to only "reification", that is, rewriting your propositional formula as the semantics of some inductive datatype

#### Mario Carneiro (Aug 31 2019 at 23:16):

and then you can do manipulations on the inductive datatype in pure code

#### Alexandre Rademaker (Aug 31 2019 at 23:26):

Hum, I will need to assimilate it ... thank you

#### Alexandre Rademaker (Aug 31 2019 at 23:34):

I believe we are talking about the same thing ... define a data type for formulas and provide code to manipulate them. But I didn’t understand the mention to reification and untrusted.

#### Mario Carneiro (Sep 01 2019 at 00:22):

@Alexandre Rademaker Here's some code that does NNF via reification:

import logic.basic tactic.interactive

@[derive has_reflect]
inductive prop : Type
| var :   prop
| not : prop  prop
| and : prop  prop  prop
| or : prop  prop  prop
| imp : prop  prop  prop
| iff : prop  prop  prop

def prop.eval (ps : list Prop) : prop  Prop
| (prop.var n) := (ps.nth n).get_or_else false
| (prop.not p) := ¬ p.eval
| (prop.and p q) := p.eval  q.eval
| (prop.or p q) := p.eval  q.eval
| (prop.imp p q) := p.eval  q.eval
| (prop.iff p q) := p.eval  q.eval

def prop.nnf : bool  prop  prop
| ff p@(prop.var _) := p
| tt p@(prop.var _) := prop.not p
| b (prop.not p) := p.nnf (bnot b)
| ff (prop.and p q) := (p.nnf ff).and (q.nnf ff)
| tt (prop.and p q) := (p.nnf tt).or (q.nnf tt)
| ff (prop.or p q) := (p.nnf ff).or (q.nnf ff)
| tt (prop.or p q) := (p.nnf tt).and (q.nnf tt)
| ff (prop.imp p q) := (p.nnf tt).or (q.nnf ff)
| tt (prop.imp p q) := (p.nnf ff).and (q.nnf tt)
| ff (prop.iff p q) := ((p.nnf tt).or (q.nnf ff)).and ((q.nnf tt).or (p.nnf ff))
| tt (prop.iff p q) := ((p.nnf ff).and (q.nnf tt)).or ((q.nnf ff).and (p.nnf tt))

instance : has_equiv prop := ⟨λ p q,  l, p.eval l  q.eval l

theorem prop.rfl {p : prop} : p  p := λ l, iff.rfl
theorem prop.symm {p₁ p₂ : prop} (h : p₁  p₂) : p₂  p₁ := λ l, (h l).symm
theorem prop.trans {p₁ p₂ p₃ : prop} (h₁ : p₁  p₂) (h₂ : p₂  p₃) : p₁  p₃ := λ l, (h₁ l).trans (h₂ l)

theorem prop.not_congr {p₁ p₂ : prop} (hp : p₁  p₂) : p₁.not  p₂.not :=
λ l, not_congr (hp l)
theorem prop.and_congr {p₁ p₂ q₁ q₂ : prop} (hp : p₁  p₂) (hq : q₁  q₂) : p₁.and q₁  p₂.and q₂ :=
λ l, and_congr (hp l) (hq l)
theorem prop.or_congr {p₁ p₂ q₁ q₂ : prop} (hp : p₁  p₂) (hq : q₁  q₂) : p₁.or q₁  p₂.or q₂ :=
λ l, or_congr (hp l) (hq l)
theorem prop.imp_congr {p₁ p₂ q₁ q₂ : prop} (hp : p₁  p₂) (hq : q₁  q₂) : p₁.imp q₁  p₂.imp q₂ :=
λ l, imp_congr (hp l) (hq l)
theorem prop.iff_congr {p₁ p₂ q₁ q₂ : prop} (hp : p₁  p₂) (hq : q₁  q₂) : p₁.iff q₁  p₂.iff q₂ :=
λ l, iff_congr (hp l) (hq l)

theorem prop.nnf_equiv :  b (p : prop), p.nnf b  cond b p.not p
| ff (prop.var _) := prop.rfl
| tt (prop.var _) := prop.rfl
| ff (prop.not p) := p.nnf_equiv tt
| tt (prop.not p) := prop.trans (p.nnf_equiv ff) $λ l, classical.not_not.symm | ff (prop.and p q) := prop.and_congr (p.nnf_equiv ff) (q.nnf_equiv ff) | tt (prop.and p q) := prop.trans (prop.or_congr (p.nnf_equiv tt) (q.nnf_equiv tt))$
λ l, classical.not_and_distrib.symm
| ff (prop.or p q) := prop.or_congr (p.nnf_equiv ff) (q.nnf_equiv ff)
| tt (prop.or p q) := prop.trans (prop.and_congr (p.nnf_equiv tt) (q.nnf_equiv tt)) $λ l, not_or_distrib.symm | ff (prop.imp p q) := prop.trans (prop.or_congr (p.nnf_equiv tt) (q.nnf_equiv ff))$
λ l, classical.imp_iff_not_or.symm
| tt (prop.imp p q) := prop.trans (prop.and_congr (p.nnf_equiv ff) (q.nnf_equiv tt)) $λ l, by classical; exact not_imp.symm | ff (prop.iff p q) := prop.trans (prop.and_congr (prop.or_congr (p.nnf_equiv tt) (q.nnf_equiv ff)) (prop.or_congr (q.nnf_equiv tt) (p.nnf_equiv ff)))$
λ l, iff.symm $iff_def.trans$
and_congr classical.imp_iff_not_or classical.imp_iff_not_or
| tt (prop.iff p q) := prop.trans (prop.or_congr
(prop.and_congr (p.nnf_equiv ff) (q.nnf_equiv tt))
(prop.and_congr (q.nnf_equiv ff) (p.nnf_equiv tt))) $λ l, iff.symm$ (not_congr iff_def).trans $classical.not_and_distrib.trans$
by classical; exact or_congr not_imp not_imp

meta def reify : expr  state (list expr) prop
| (¬ %%a) := prop.not <$> reify a | (%%a %%b) := prop.and <$> reify a <*> reify b
| (%%a  %%b) := prop.or <$> reify a <*> reify b | (%%a %%b) := prop.imp <$> reify a <*> reify b
| (%%a  %%b) := prop.iff <\$> reify a <*> reify b
| a := ⟨λ l,
let n := list.find_index (= a) l in
(prop.var n, if n < l.length then l else l ++ [a])

protected meta def list.reflect' (u : level) (α : expr) : list expr  expr
| [] := (expr.const list.nil [u] : expr) α
| (a :: l) := (expr.const list.cons [u] : expr) α a l.reflect'

open tactic

meta def nnf₃ : tactic unit :=
do e  tactic.target,
let (p, l) := (reify e).run [],
let es : expr := l.reflect' level.zero (Prop),
refine (iff.mp (prop.nnf_equiv ff %%(reflect p) %%es) _),
let p' := p.nnf ff,
tactic.change `(prop.eval %%es %%(reflect p'))

example (p q r s : Prop) : (p  (q  r)  (r  s))  p :=
begin
nnf₃,
dsimp only [prop.eval, option.get_or_else, list.nth],
end

I didn't write a function to convert from prop back to Prop, so the goal is left in a messy state after nnf, but it is defeq to the "right" goal and dsimp will clean it up

#### Mario Carneiro (Sep 01 2019 at 00:26):

Notice which parts are marked meta. The reify function will take the target expression from the elaborator and built an equivalent element of the inductive datatype prop; the eval function converts back to Prop and the first few lines convert the goal to something of the form prop.eval es p where es is a literal list of propositions and p is an expression of type prop

#### Mario Carneiro (Sep 01 2019 at 00:28):

The main theorem is nnf_equiv, which says that prop.eval es (p.nnf ff) <-> prop.eval es p, and we apply it in the forward direction so that we only need to show prop.eval es (p.nnf ff), which defeq simplifies to the desired expression

#### Alexandre Rademaker (Sep 01 2019 at 00:29):

Thank you so much!

#### Johan Commelin (Sep 01 2019 at 04:56):

I do understand the general feeling that curl foobar | sh is an evil pattern. But it is not that hard to curl foobar > bla; less bla; sh bla. So I don't really find it evil in practice.

#### Johan Commelin (Sep 01 2019 at 04:58):

Also, if you are paranoid about the shell scripts and tooling provided by the mathlib community, be sure to not put import logic.foobar at the top of your Lean files, if you haven't read through that import (and all its dependencies!). After all, it might be a bomb! Lean can execute code... it's not some sandbox.

#### Keeley Hoek (Sep 01 2019 at 05:07):

FWIW, even if you trust current mathlib, mathlib is not secure. Just after a pull request is approved but before it is merged someone could commit malicious code to logic.basic with the message "spelling" or something and have that merged and not noticed for a while, infecting everyone who upgrades checks-out the new master.

#### Andrew Ashworth (Sep 01 2019 at 05:33):

installation scripts are particularly attractive targets for criminals, though, since they are frequently run with administrator permissions

#### Keeley Hoek (Sep 01 2019 at 05:34):

I don't know if people are exactly installing mathlib at a breakneck pace right now though :P

#### Andrew Ashworth (Sep 01 2019 at 05:35):

just explaining the thought process of many paranoid people

#### Andrew Ashworth (Sep 01 2019 at 05:35):

some things deserve more scrutiny than others

#### Daniel Donnelly (Sep 01 2019 at 06:01):

Hey, I'm paranoid at times. Doesn't mean I want break into systems :) j/k

#### Mario Carneiro (Sep 01 2019 at 06:53):

My point isn't about the security of the curl | sh practice, it's about the lack of documentation

#### Mario Carneiro (Sep 01 2019 at 06:54):

Suppose the script breaks for some obscure reason. How can I diagnose what's going on (assuming I'm technically literate but unfamiliar with lean), and possibly work around whatever problem arises? Documentation describing the intent and effect of the script goes a long way toward being able to address these problems, as well as mollifying the paranoid

#### Mario Carneiro (Sep 01 2019 at 06:58):

@Keeley Hoek Note that in your attack the malicious spelling commit would have to be authored by someone with write access. Granted we aren't very strict about enforcement, but there aren't that many people with write access

#### Keeley Hoek (Sep 01 2019 at 06:59):

That's good to know

Last updated: May 13 2021 at 17:42 UTC