CNF transformation of Propositional expressions

Stream: new members

[Alexandre Rademaker]

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

[Patrick Massot]

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

[Alexandre Rademaker]

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]

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

[Mario Carneiro]

Yes, we've done that in class before

[Mario Carneiro]

The simple way is to use a carefully chosen simp set

[Mario Carneiro]

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

[Alexandre Rademaker]

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?

[Alexandre Rademaker]

(deleted)

[Mario Carneiro]

@Alexandre Rademaker
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]

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]

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]

I guess you don't have mathlib

[Patrick Massot]

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

[Patrick Massot]

or the online analogue https://github.com/leanprover-community/mathlib/search?q=imp_iff_not_or&unscoped_q=imp_iff_not_or

[Alexandre Rademaker]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

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]

I believe you can run leanpkg add leanprover-community/mathlib from your project root and it should download mathlib and put it in your project dependencies

[Mario Carneiro]

@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]

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]

(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]

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]

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]

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

[Mario Carneiro]

and then hand it to lean

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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]

@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]

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]

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]

Thank you so much!

[Johan Commelin]

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]

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]

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]

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

[Keeley Hoek]

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

[Andrew Ashworth]

just explaining the thought process of many paranoid people

[Andrew Ashworth]

some things deserve more scrutiny than others

[Daniel Donnelly]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

@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]

That's good to know