Tactic to convert logical propositions into DNF

Stream: metaprogramming / tactics

[TauTastic]

I want to write a Lean program that converts logical propositions into their DNF. First of all I don't know a tactic is the right way to go. I started off by trying to write a tactic that expands implications

$$A \to B \iff \lnot A \lor B$$

Here is the lean code thus far:

import Lean.Elab.Tactic

open Lean Elab Tactic Meta in
elab "simp_logic" : tactic => do
  liftMetaTactic fun mvarId => do
    trace[simp_logic] "arrow {mvarId}"
    let (Expr.forallE _ p q .default) ← mvarId.getType | Lean.Meta.throwTacticEx `simp_logic mvarId ("Goal is not of the form P → Q")
    let notP := mkNot p
    let mvarIdP ← mkFreshExprMVar p
    let mvarIdQ ← mkFreshExprMVar q

    let proofTerm := mkOr notP q
    mvarId.assign proofTerm

    return [mvarId]

theorem myTest (A B : Prop) : A → B := by
  simp_logic
  sorry

I get the following error:

(kernel) declaration type mismatch, 'myTest' has type
  Prop → Prop → Prop
but it is expected to have type
  ∀ (A B : Prop), A → B

[Daniel Weber]

The problem is that you assigm to mvarId the Prop ¬A∨B, but what it should have is a proof of A -> B. Using Qq you can do:

import Lean.Elab.Tactic
import Qq

open Lean Elab Tactic Meta Qq in
elab "simp_logic" : tactic => do
  liftMetaTactic fun mvarId => do
    trace[simp_logic] "arrow {mvarId}"
    let (Expr.forallE _ p q .default) ← mvarId.getType | throwTacticEx `simp_logic mvarId "Goal is not of the form P → Q"
    let some p ← checkTypeQ p q(Prop) | throwTacticEx `simp_logic mvarId m!"{p} isn't a proposition"
    let some q ← checkTypeQ q q(Prop) | throwTacticEx `simp_logic mvarId m!"{q} isn't a proposition"

    let newMVar ← mkFreshExprMVarQ q(¬$p ∨ $q)

    mvarId.assign (q(($newMVar).elim (fun nh h ↦ (nh h).elim) (fun h _ ↦ h)) : Q($p → $q))

    return [newMVar.mvarId!]

[TauTastic]

@Daniel Weber That works great thank you :)