Lean4
/-- A decision procedure for intuitionistic propositional logic.
* `useDec` will add `a ∨ ¬ a` to the context for every decidable atomic proposition `a`.
* `useClassical` will allow `a ∨ ¬ a` to be added even if the proposition is not decidable,
using classical logic.
* `extraDec` will add `a ∨ ¬ a` to the context for specified (not necessarily atomic)
propositions `a`.
-/
def itautoCore (g : MVarId) (useDec useClassical : Bool) (extraDec : Array Expr) : MetaM Unit := do
AtomM.run (← getTransparency) do
let mut hs := mkNameMap Expr
let t ← g.getType
let (g, t) ←
if ← isProp t then
pure (g, ← reify t)
else
pure (← g.exfalso, .false)
let mut Γ : Except (IProp → Proof) ITauto.Context := .ok TreeMap.empty
let mut decs := TreeMap.empty
for ldecl in ← getLCtx do
if !ldecl.isImplementationDetail then
let e := ldecl.type
if ← isProp e then
let A ← reify e
let n := ldecl.fvarId.name
hs := hs.insert n (Expr.fvar ldecl.fvarId)
Γ := do
(← Γ).add A (.hyp n)
else
if let .const ``Decidable _ := e.getAppFn then
let p : Q(Prop) := e.appArg!
if useDec then
let A ← reify p
decs := decs.insert A (false, Expr.fvar ldecl.fvarId)
let addDec (force : Bool) (decs : TreeMap IProp (Bool × Expr) IProp.cmp) (e : Q(Prop)) := do
let A ← reify e
let dec_e := q(Decidable $e)
let res ← trySynthInstance q(Decidable $e)
if !(res matches .some _) && !useClassical then
if force then
_ ← synthInstance dec_e
pure decs
else
pure
(decs.insert A
(match res with
| .some e => (false, e)
| _ => (true, e)))
decs ← extraDec.foldlM (addDec true) decs
if useDec then
let mut decided := TreeSet.empty (cmp := compare)
if let .ok Γ' := Γ then
decided :=
Γ'.foldl (init := decided) fun m p _ =>
match p with
| .var i => m.insert i
| .not (.var i) => m.insert i
| _ => m
let ats := (← get).atoms
for e in ats, i in [0:ats.size]do
if !decided.contains i then
decs ← addDec false decs e
for (A, cl, pf) in decs do
let n ← mkFreshId
hs := hs.insert n pf
Γ := return (← Γ).insert (A.or A.not) (.em cl n)
let p : Proof :=
match Γ with
| .ok Γ => (prove Γ t 0).1.2
| .error p => p t
applyProof g hs p
