Commit 2022-03-10 10:43 62c2af36

feat: LRAT proof replay (#222) This is based on a suggestion by @avigad. From the docs:

lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

produces the theorem:

foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1

There is still some design work to be done on how exactly to make this usable in practice; in particular the generated theorem is always written in DNF, while for a tactic we would generally want to infer the structure from the goal statement instead of the CNF file. The main aim of this implementation is to be as high performance as can be reasonably achieved while still being proof-object-based (there is some definitional unfolding but nothing too heavy). I haven't tried to give it any truly massive proofs yet (I will have to figure out how to run it compiled first), but it seems to hold up reasonably well even on proofs in the 10000 line range.