dealing with the Option monad in proofs

Stream: Is there code for X?

[Paige Thomas]

Is there a way to make goals like this easier to work with, for example by some tactic to automatically turn it into a bunch of if, then, else cases that I could do a split_ifs on? That is cases on whether or not the eval V F is a some val_phi or none?

⊢ (¬∃ V,
      (do
          let val_phi ← eval V F
          some ¬val_phi) =
        some True) ↔
  ∀ (V : PropValuation), eval V F = some True

[Eric Wieser]

cases h : eval V F?

[Eric Wieser]

(it might only work with cases')

[Paige Thomas]

Unfortunately I don't have the V to use.

[Paige Thomas]

That is, it is only quantified.

[Edward van de Meent]

in that case, can you first rewrite using not_exists, then apply something like forall_congr?

[Edward van de Meent]

at that point you should be able to use v, i think...

[Paige Thomas]

  ...
  rewrite [not_exists]
  simp
  congr!
  case _ V =>
    cases h : eval V F
    simp

case none
F : Formula_
V : PropValuation
h : eval V F = none
⊢ False

[Paige Thomas]

The forall_congr wouldn't apply.

[Paige Thomas]

Not a MWE, but workable code:

import Lean
import Batteries.Tactic.Lint.Frontend
import Mathlib.Util.CompileInductive
import Mathlib.Tactic


set_option autoImplicit false


/--
  The type of formulas.
-/
inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  | forall_ : String → Formula_ → Formula_
  | exists_ : String → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Repr

compile_inductive% Formula_

open Formula_

def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi
  | or_ phi psi
  | imp_ phi psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | forall_ _ phi
  | exists_ _ phi => atom_occurs_in A phi


def PropValuation : Type := String → Prop
  deriving Inhabited


def eval
  (V : PropValuation) :
  Formula_ → Option Prop
  | false_ => some False
  | true_ => some True
  | atom_ X => some (V X)
  | not_ phi => do
    let val_phi ← eval V phi
    ¬ val_phi
  | and_ phi psi => do
    let val_phi ← eval V phi
    let val_psi ← eval V psi
    val_phi ∧ val_psi
  | or_ phi psi => do
    let val_phi ← eval V phi
    let val_psi ← eval V psi
    val_phi ∨ val_psi
  | imp_ phi psi => do
    let val_phi ← eval V phi
    let val_psi ← eval V psi
    val_phi → val_psi
  | iff_ phi psi => do
    let val_phi ← eval V phi
    let val_psi ← eval V psi
    val_phi ↔ val_psi
  | forall_ _ _
  | exists_ _ _ => none


def satisfies
  (V : PropValuation)
  (F : Formula_) :
  Prop :=
  eval V F = some True

def Formula_.is_tautology
  (F : Formula_) :
  Prop :=
  ∀ (V : PropValuation), satisfies V F

def Formula_.is_satisfiable
  (F : Formula_) :
  Prop :=
  ∃ (V : PropValuation), satisfies V F

def Formula_.is_unsatisfiable
  (F : Formula_) :
  Prop :=
  ¬ ∃ (V : PropValuation), satisfies V F


example
  (F : Formula_) :
  (not_ F).is_unsatisfiable ↔ F.is_tautology :=
  by
  unfold is_tautology
  unfold is_unsatisfiable
  unfold satisfies
  simp only [eval]
  sorry

[Edward van de Meent]

add on these:

  rw [not_exists]
  rw [iff_eq_eq]
  apply forall_congr
  simp? says simp only [Option.bind_eq_bind, eq_iff_iff]
  intro V

[Paige Thomas]

I think maybe the cases isn't working in this proof.

[Paige Thomas]

Or I am applying it wrong.

[Edward van de Meent]

ah, maybe it's not true?

[Edward van de Meent]

due to how exists works, it seems there might be an issue?

[Paige Thomas]

I think it needs classical?

[Paige Thomas]

oh, hmm.

[Edward van de Meent]

no, the issue is that if your formula contains exists, satisfies V F will always be false

[Paige Thomas]

yeah, hmm

[Edward van de Meent]

meaning that F.is_unsatisfiable while it might be a tautology

[Edward van de Meent]

(looking at the code again, it looks like the same issue happens for forall

[Paige Thomas]

I need a different definition of satisfies that only holds if F is a proposition (does not have Forall and Exists)

[Edward van de Meent]

alternatively, you can create an F.is_proposition predicate, and have that as hypothesis for the theorem

[Paige Thomas]

yeah

[Paige Thomas]

I guess then I need to do an induction on F.

[Paige Thomas]

Thank you for finding that.