Lean4
/-- Build the type and value of the reified theorem. This rewrites all the SAT definitions
into standard operators on `Prop`, for example if the formula is `[[1, 2], [-1, 2], [-2]]` then
this produces a proof of `⊢ ∀ a b : Prop, (a ∧ b) ∨ (¬a ∧ b) ∨ ¬b`. We use the input `nvars` to
decide how many quantifiers to use.
Most of the proof is under `2 * nvars + 1` quantifiers
`a1 .. an : Prop, v : Valuation, h1 : v 0 ↔ a1, ... hn : v (n-1) ↔ an ⊢ ...`, and we do the index
arithmetic by hand.
1. First, we call `reifyFormula ctx'` which returns `a` and `pr : reify v ctx' a`
2. Then we build `fun (v : Valuation) (h1 : v 0 ↔ a1) ... (hn : v (n-1) ↔ an) ↦ pr`
3. We have to lower expression `a` from step 1 out of the quantifiers by lowering all variable
indices by `nvars+1`. This is okay because `v` and `h1..hn` do not appear in `a`.
4. We construct the expression `ps`, which is `a1 .. an : Prop ⊢ [a1, ..., an] : List Prop`
5. `refute ctx (hf : ctx.proof []) (fun v h1 .. hn ↦ pr) : a` forces some definitional unfolding
since `fun h1 .. hn ↦ pr` should have type `implies v (reify v ctx a) [a1, ..., an] a`,
which involves unfolding `implies` n times as well as `ctx ↦ ctx'`.
6. Finally, we `intro a1 ... an` so that we have a proof of `∀ a1 ... an, a`.
-/
partial def buildReify (ctx ctx' proof : Expr) (nvars : Nat) : Expr × Expr :=
Id.run do
let (e, pr) := reifyFmla ctx'
let mut pr := pr
for i in [0:nvars]do
let j := nvars - i - 1
let ty := mkApp2 (mkConst ``Iff) (mkApp (mkBVar j) (mkRawNatLit j)) (mkBVar nvars)
pr := mkLambda `h default ty pr
pr := mkLambda `v default (mkConst ``Sat.Valuation) pr
let mut e := e.lowerLooseBVars (nvars + 1) (nvars + 1)
let cons := mkApp (mkConst ``List.cons [levelZero]) (mkSort levelZero)
let nil := mkApp (mkConst ``List.nil [levelZero]) (mkSort levelZero)
let rec mkPS depth e
| 0 => e
| n + 1 => mkPS (depth + 1) (mkApp2 cons (mkBVar depth) e) n
pr := mkApp5 (mkConst ``Sat.Fmla.refute) e (mkPS 0 nil nvars) ctx proof pr
for _ in [0:nvars]do
e := mkForall `a default (mkSort levelZero) e
pr := mkLambda `a default (mkSort levelZero) pr
pure (e, pr)
where
/-- The `v` variable under the `a1 ... an, v, h1 ... hn` context -/
v := mkBVar nvars
/-- Returns `a` and `pr : reify v f a` given a formula `f` -/
reifyFmla f :=
match f.getAppFn.constName! with
| ``Sat.Fmla.and =>
let f₁ := f.appFn!.appArg!
let f₂ := f.appArg!
let (e₁, h₁) := reifyFmla f₁
let (e₂, h₂) := reifyFmla f₂
(mkApp2 (mkConst ``Or) e₁ e₂, mkApp7 (mkConst ``Sat.Fmla.reify_or) v f₁ e₁ f₂ e₂ h₁ h₂)
| ``Sat.Fmla.one =>
let c := f.appArg!
let (e, h) := reifyClause c
(e, mkApp4 (mkConst ``Sat.Fmla.reify_one) v c e h)
| _ => panic! "not a valid formula"
/-- Returns `a` and `pr : reify v c a` given a clause `c` -/
reifyClause c :=
if c.appFn!.isConst then (mkConst ``True, mkApp (mkConst ``Sat.Clause.reify_zero) v) else reifyClause1 c
/-- Returns `a` and `pr : reify v c a` given a nonempty clause `c` -/
reifyClause1 c :=
let l := c.appFn!.appArg!
let c := c.appArg!
let (e₁, h₁) := reifyLiteral l
if c.isConst then (e₁, mkApp4 (mkConst ``Sat.Clause.reify_one) v l e₁ h₁)
else
let (e₂, h₂) := reifyClause1 c
(mkApp2 (mkConst ``And) e₁ e₂, mkApp7 (mkConst ``Sat.Clause.reify_and) v l e₁ c e₂ h₁ h₂)
/-- Returns `a` and `pr : reify v l a` given a literal `c` -/
reifyLiteral l :=
let n := l.appArg!
let (e, h) := reifyVar n
match l.appFn!.constName! with
| ``Sat.Literal.pos => (mkApp (mkConst ``Not) e, mkApp4 (mkConst ``Sat.Literal.reify_pos) v e n h)
| ``Sat.Literal.neg => (e, mkApp4 (mkConst ``Sat.Literal.reify_neg) v e n h)
| _ => panic! "not a valid literal"
/-- Returns `a` and `pr : v n ↔ a` given a variable index `n`.
These are both lookups into the context
`(a0 .. a(n-1) : Prop) (v) (h1 : v 0 ↔ a0) ... (hn : v (n-1) ↔ a(n-1))`. -/
reifyVar v :=
let n := v.rawNatLit?.get!
(mkBVar (2 * nvars - n), mkBVar (nvars - n - 1))
