Lean4
/-- Constructs the proofs of `⊢ ctx.proof c` for each clause `c` in `ctx`.
The proofs are stashed in a `HashMap` keyed on the clause ID. -/
partial def buildClauses (arr : Array (Array Int)) (ctx : Expr) (start stop : Nat) (f p : Expr)
(accum : Nat × HashMap Nat Clause) : Nat × HashMap Nat Clause :=
match stop - start with
| 0 => panic! "empty"
| 1 =>
let c := f.appArg!
let proof := mkApp3 (mkConst ``Sat.Fmla.proof_of_subsumes) ctx c p
let n := accum.1 + 1
(n, accum.2.insert n { lits := arr[start]!, expr := c, proof })
| len =>
let mid := start + len / 2
let f₁ := f.appFn!.appArg!
let f₂ := f.appArg!
let p₁ := mkApp4 (mkConst ``Sat.Fmla.subsumes_left) ctx f₁ f₂ p
let p₂ := mkApp4 (mkConst ``Sat.Fmla.subsumes_right) ctx f₁ f₂ p
let accum := buildClauses arr ctx start mid f₁ p₁ accum
buildClauses arr ctx mid stop f₂ p₂ accum
