Lean4
/-- Construct an individual proof step `⊢ ctx.proof c`.
* `db`: the current global context
* `ns`, `clause`: the new clause
* `pf`: the LRAT proof trace
* `ctx`: the main formula
The proof has three steps:
1. Introduce local assumptions `have h1 : ctx.proof c1 := p1` for each clause `c1`
referenced in the proof. We actually do all the introductions at once,
as in `(fun h1 h2 h3 ↦ ...) p1 p2 p3`, because we want `p_i` to not be under any binders
to avoid the cost of `instantiate` during typechecking and get the benefits of dag-like
sharing in the `pi` (which are themselves previous proof steps which may be large terms).
The hypotheses are in `gctx`, keyed on the clause ID.
2. Unfold `⊢ ctx.proof [a, b, c]` to
`∀ v, v.satisfies_fmla ctx → v.neg a → v.neg b → v.neg c → False` and `intro v hv ha hb hc`,
storing each `ha : v.neg a` in `lctx`, keyed on the literal `a`.
3. For each LRAT step `hc : ctx.proof [x, y]`, `hc v hv : v.neg x → v.neg y → False`.
We look for a literal that is not falsified in the clause. Since it is a unit propagation
step, there can be at most one such literal.
* If `x` is the non-falsified clause, let `x'` denote the negated literal of `x`.
Then `x'.negate` reduces to `x`, so `hnx : v.neg x'.negate |- hc v hv hnx hy : False`,
so we construct the term
`by_cases (fun hnx : v.neg x'.negate ↦ hc v hv hnx hy) (fun hx : v.neg x ↦ ...)`
and `hx` is added to the local context.
* If all clauses are falsified, then we are done: `hc v hv hx hy : False`.
-/
partial def buildProofStep (db : HashMap Nat Clause) (ns pf : Array Int) (ctx clause : Expr) : Except String Expr :=
Id.run
(do
let mut lams := #[]
let mut args := #[]
let mut gctx : HashMap Nat LClause :=
{ }
-- step 1
for i in pf do
let i := i.natAbs
let some cl := db[i]? |
return Except.error "missing clause"
if !gctx.contains i then
lams := lams.push (mkApp2 (mkConst ``Sat.Fmla.proof) ctx cl.expr)
args := args.push cl.proof
gctx :=
gctx.insert i
{ lits := cl.lits
expr := cl.expr
depth := args.size }
let n := args.size
let mut f :=
(mkAppN · args) ∘
lams.foldr (mkLambda `c default) ∘
mkLambda `v default (mkConst ``Sat.Valuation) ∘
mkLambda `hv default (mkApp2 (mkConst ``Sat.Valuation.satisfies_fmla) (mkBVar 0) ctx)
let v depth := mkBVar (depth + 1)
let hv depth := mkBVar depth
lams := #[]
let mut clause := clause
let mut depth := 0
let mut lctx : HashMap Int Nat := { }
for i in ns do
let l := clause.appFn!.appArg!
clause := clause.appArg!
lams := lams.push (mkApp2 (mkConst ``Sat.Valuation.neg) (v depth) l)
depth := depth.succ
lctx := lctx.insert i depth
f :=
f ∘
lams.foldr
(mkLambda `h default)
-- step 3
for (step : Int) in pf do
if step < 0 then
return Except.error "unimplemented: RAT step"
let some cl := gctx[step.toNat]? |
return Except.error "missing clause"
let mut unit := none
for i in cl.lits do
unless lctx.contains i do
if unit.isSome then
return Except.error s! "not unit: {cl.lits}"
depth := depth.succ
unit := some i
let mut pr := mkApp2 (mkBVar (depth + n + 2 - cl.depth)) (v depth) (hv depth)
for i in cl.lits do
pr :=
mkApp pr <|
mkBVar
(match lctx[i]? with
| some k => depth - k
| _ => 0)
let some u := unit |
return Except.ok <| f pr
let lit := toExpr <| Sat.Literal.ofInt u
let nlit := toExpr <| Sat.Literal.ofInt (-u)
let d1 := depth - 1
let app :=
mkApp3 (mkConst ``Sat.Valuation.by_cases) (v d1) nlit <|
mkLambda `h default (mkApp2 (mkConst ``Sat.Valuation.neg) (v d1) lit) pr
let dom := mkApp2 (mkConst ``Sat.Valuation.neg) (v d1) nlit
f := fun e ↦ f <| mkApp app <| mkLambda `h default dom e
lctx := lctx.insert (-u) depth
return Except.error s! "no refutation: {ns }, {pf }, {lctx.toList}")
