using System.Text using Nemerle.Collections using Nemerle.Utility using Nemerle.Logging using Nemerle.Imperative set namespace Fx7 public class ProofGen mutable lemmas : list [Lemma] dumped : Hashtable [Clause, int] = Hashtable () core : Core public class Lemma public name : string public comment : string public clause : Clause public formula : Term public proof : E public this (name : string, comment : string, clause : Clause, proof : E) this.name = name this.comment = comment this.clause = clause this.proof = proof public this (name : string, comment : string, formula : Term, proof : E) this.name = name this.comment = comment this.formula = formula this.proof = proof public variant E | Lit l : Literal | InfTerm t : void -> Fx7.Term prop : bool | Term t : Fx7.Term prop : bool | Ref hd : string | App hd : string children : list [E] | Fun parms : list [string * E] body : E | Lambda parm : string body : E | Let name : string val : E body : E | RawClause c : Clause // not used here | Id | GenApp t1 : E t2 : E | Comp t1 : E t2 : E public IsFake : bool get mutable fake = false Iter (fun (_) { | App ("eq_fake", _) => fake = true | _ => {} }) fake public Iter (f : E -> void) : void f (this) match (this) | Lit | InfTerm | Term | Ref | RawClause | Id => {} | App (_, children) => children.Iter (_.Iter (f)) | Let (_, e1, e2) | GenApp (e1, e2) | Comp (e1, e2) => e1.Iter (f) e2.Iter (f) | Lambda (_, e) => e.Iter (f) | Fun (parms, body) => foreach ((_, b) in parms) b.Iter (f) body.Iter (f) public override ToString () : string match (this) | Lit (l) => $"Lit($l)" | InfTerm (_, _) => "_" | Term (t, _) => $ "Term($t)" | Ref (h) => $ "Ref($h)" | App (h, children) => $ "$h%$children" | Fun (parms, body) => $ "fun $parms $body" | Lambda (x, body) => $ "lambda $x $body" | Let (name, val, body) => $ "let $name := $val in $body" | RawClause (c) => $ "$c" | Id => "id" | GenApp (t1, t2) => $"$t1 . $t2" | Comp (t1, t2) => $"$t1 * $t2" Match (pat : Term, grnd : Term, subst : Subst) : Subst //log (COQ, $"cmp: $pat $grnd") if (subst.Contains (pat.Id)) def pat' = subst.Get (pat.Id) if (pat' == null) subst.Replace (pat.Id, grnd) else assert (pat' === grnd) subst else if (pat === grnd) subst else if (pat.Name != "=" && grnd.Name == "=") assert (grnd.Child_2of2 === core.TermPool.True) Match (pat, grnd.Child_1of2, subst) else assert (pat.Name == grnd.Name, $ "prob: $pat $grnd") assert (pat.Arity == grnd.Arity) List.FoldLeft2 (pat.Children, grnd.Children, subst, Match) FindInst (c : Clause) : list [Term * Term] assert (c.Lits.Length == 2) def (qlit, inst) = if (c.Lits [0].atom.IsQuantified) (c.Lits [0], c.Lits [1]) else (c.Lits [1], c.Lits [0]) def inst = if (qlit.IsNeg) inst else ~inst def qatom = qlit.atom :> QAtom def subst = qatom.Vars.FoldLeft (IntTree.Empty (), (v, a) => a.Add (v.Id, null)) def subst = Match (qatom.Formula, inst.ToTerm (), subst) qatom.Vars.Map (v => (v, if (subst.Get (v.Id) == null) v else subst.Get (v.Id))) FindDeep (c : Clause) : Literal * list [Literal] mutable max = c.Lits [0] foreach (l in c.Lits) when (l.atom.term1.Depth > max.atom.term1.Depth) max = l (max, $[l | l in c.Lits, l !== max]) FindDeep2 (c : Clause) : Literal * Literal match (FindDeep (c)) | (l, [q]) => (l, q) | _ => assert (false) ResolutionProofWithAssume (c : Clause, r : Rule.Resolution) : E def ini = r.initial def steps = r.steps log (COQ, $"c:$c, ini=$ini, st=$steps") Save (ini) def steps_ht = Hashtable () foreach ((l, c) in steps) Save (c) log (COQ, $ "steps_ht -> $l -> $c") steps_ht [l] = c def ids = Hashtable () mutable lets = [] def add (l) log (COQ, $"add: $l -> $(ids.Count)") ids [l] = ids.Count $ "p$(ids.Count - 1)" foreach (l in c.Lits) _ = add (~l) def prove_lit (l) log (COQ, $ "dump_lit $l") if (ids.Contains (l)) {} else if (steps_ht [l] == null) {} else def c = steps_ht [l] steps_ht [l] = null assert (! ids.Contains (l)) assert (! ids.Contains (~l)) lets ::= (add (l), dump (l, c)) and dump (l, c) log (COQ, $"( dump: $l in $c") foreach (q in c.Lits) if (q === l) {} else prove_lit (~q) def s = if (l != null && c.Lits.Length >= 1 && c.Lits.Length <= 3) def pos = System.Array.IndexOf (c.Lits, l) def args = E.Ref ($"c$(dumped[c])") :: $[E.Ref ($"p$(ids[~q])") | q in c.Lits, q !== l] def res = E.App ($"simple_res_$(c.Lits.Length)_$(pos + 1)", args) if (l.IsNeg) res else E.App ("nnpp", [res]) else def args = $[E.Ref ($"p$(ids[if (q === l) q else ~q])") | q in c.Lits] def s = args.FoldLeft (E.Ref ($"c$(dumped[c])"), (arg, acc) => E.App ("mp", [acc, arg])) if (l == null) s else def suf = if (l.IsPos) "n" else "p" E.App ("absurd_" + suf, [E.Fun ([($"p$(ids[l])", E.Lit (~l))], s)]) log (COQ, $"dump -> $s )") s def d = dump (null, ini) def d = lets.FoldLeft (d, fun ((n, v), a) { E.Let (n, v, a) }) def d = if (c.Lits.Length == 0) d else E.Fun ($[($"p$(ids[~l])", E.Lit (~l)) | l in c.Lits], d) d mutable comment : string ProcessArithProof (get_lit : Literal -> E, clause : Clause) : E def ap = ArithProofs (get_lit, core) def res = ap.TryFindContradiction ($[~l | l in clause.Lits]) if (res == null) def rewrites = Hashtable () def visited = Hashtable () def add_eq (t1, t2, proof) //assert (t1.Root === t2.Root, $"t1 = $t1 -> $(t1.Root) t2 = $t2 -> $(t2.Root)") when (t1 !== t2 && !proof.IsFake) def d1 = t1.Depth def d2 = t2.Depth if (d1 > d2 || (d1 == d2 && t1.Id > t2.Id)) add_eq (t2, t1, E.App ("eq_symm", [proof])) else rewrites [t2] = (t1, E.App ("eq_symm", [proof])) def newlits = Hashtable () mutable lets = [] def find_eq (p : Proof) if (visited.Contains (p)) {} else visited [p] = p match (p) | Rule1 (_, p1) with ps = [p1] \ | Rule2 (_, p1, p2) with ps = [p1, p2] \ | Rule3 (_, p1, p2, p3) with ps = [p1, p2, p3] \ | Rule4 (_, p1, p2, p3, p4) with ps = [p1, p2, p3, p4] => foreach (p in ps) find_eq (p) | EqProof (t1, t2) => //log (TEMP, $"got eq proof $(t1.ToExactString()) = $(t2.ToExactString())") if (t1.IsReal && t2.IsReal) def l = Atom (t1, t2).GetLiteral (false) unless (newlits.Contains (l)) def proof = t1.EProofOfEqualityWith (get_lit, t2) add_eq (t1, t2, proof) def id = newlits.Count def name = $"new1_eq$id" newlits [l] = name lets ::= (name, proof) else find_eq (t1.ProofOfEqualityWith (t2)) | Leaf (l) => when (l.IsPos && l.atom.term2 != null) add_eq (l.atom.term1, l.atom.term2, get_lit (l)) | Token | True => {} //log (TEMP, $"proof = $(core.ProofObject)") find_eq (core.ProofObject) // eq_rewrite(t) = (t',p) // where p is proof of t=t' def eq_rewrite (t) if (rewrites.Contains (t)) def (t', p) = rewrites [t] def (t'', p') = eq_rewrite (t') (t'', E.App ("eq_trans", [p, p'])) else def map_children (acc, lst) match (lst) | c :: cc => def (c', p) = eq_rewrite (c) if (c' === c) map_children (c :: acc, cc) else def t' = core.TermPool.Get (t.Name, acc.RevAppend (c' :: cc)) def to_e = t => E.Term (t, prop = false) def p = E.App ("eq_mon", [E.Lambda ("eqtmp", E.App (t.Name, acc.Map (to_e).RevAppend (E.Ref ("eqtmp") :: cc.Map (to_e)))), p]) def (t'', p') = eq_rewrite (t') (t'', E.App ("eq_trans", [p, p'])) | [] => (t, E.App ("eq_refl", [E.Term (t, prop = false)])) map_children ([], t.Children) foreach (l in clause.Lits) def l = ~l def t = l.Abs.ToTerm () def (t', proof) = eq_rewrite (t) //log (TEMP, $"rewr: $t -> $(t')") // if it wasn't there when (t !== t') def l'= match (t'.Name) | "<=" | ">=" | "<" | ">" => Atom (t', null).GetLiteral (l.IsNeg) | "=" => def t1 = t'.Child_1of2 def t2 = t'.Child_2of2 if (t1 === t2) null else Atom (t1, t2).GetLiteral (l.IsNeg) | _ => null if (l' == null) { } else //log (TEMP, "got l'") def id = newlits.Count def name = $"new_eq$id" newlits [l'] = name def lambda = if (l'.IsNeg) E.Lambda ("x", E.App ("not", [E.Ref ("x")])) else E.Lambda ("x", E.Ref ("x")) lets ::= (name, E.App ("mp", [E.App ("eq_mon2", [lambda, proof]), get_lit (l)])) def get_lit2 (l) if (newlits.Contains (l)) E.Ref (newlits [l]) else get_lit (l) def lits = newlits.Fold ($[~l | l in clause.Lits], (k, _, acc) => k :: acc) def ap = ArithProofs (get_lit2, core) def res = ap.TryFindContradiction (lits) if (res == null) ap.ScanForEqualities () foreach (l in clause.Lits) when (l.atom.term2 != null && l.IsPos) def (t1, p1) = ap.SimplifyTerm (l.atom.term1) def (t2, p2) = ap.SimplifyTerm (l.atom.term2) log (TEMP, $"$(l.atom.term1) -> $t1 ::: $(l.atom.term2) -> $t2") when (t1 === t2) log (TEMP, $"generated eq-prop proof: $(l.atom.term1) -> $t1 ::: $(l.atom.term2) -> $t2") def pfalse = E.App ("excl_mid_pn", [E.App ("eq_trans", [p1, E.App ("eq_symm", [p2])]), get_lit (~l)]) return (lets.FoldLeft (pfalse, fun ((name, proof), acc) { E.Let (name, proof, acc) })) null else //log (INFO, $"found proof after canonicalization, for $clause") lets.FoldLeft (res, fun ((name, proof), acc) { E.Let (name, proof, acc) }) else res ProcessEqProof (clause : Clause) : E def literals = Hashtable () foreach (l in clause.Lits) literals [~l] = literals.Count def get_lit (lit) assert (literals.Contains (lit)) E.Ref ($ "eq$(literals [lit])") // neq: d1 != d2 // proof: t1 = t2 def finish (t1, d1, t2, d2, neq, proof) def eq = E.App ("eq_trans", [ E.App ("eq_trans", [d1.EProofOfEqualityWith (get_lit, t1), t1.ExtractProof (get_lit, proof, t1, t2)]), t2.EProofOfEqualityWith (get_lit, d2)]) E.App ("excl_mid_np", [neq, eq]) def fake_neq (comm, d1, d2) E.App ("eq_fake", [E.Ref (comm), E.App ("not", [ E.App ("=", [E.Term (d1, false), E.Term (d2, false)])])]) def get_neq_proof (d1, d2, p : Proof) match (p) | Leaf (neq_lit) => if (neq_lit.IsNeg && (neq_lit.atom.term1 === d1 && neq_lit.atom.term2 === d2)) get_lit (neq_lit) else if (neq_lit.IsNeg && (neq_lit.atom.term1 === d2 && neq_lit.atom.term2 === d1)) E.App ("neq_symm", [get_lit (neq_lit)]) else fake_neq ("wrong_neq", d1, d2) | _ => fake_neq ("wrong_neq", d1, d2) def get_distinct_proof (d1, d2, dist_proof) match (dist_proof : Proof) | Leaf (dist_lit) when dist_lit.atom.term1.Name == "distinct" && dist_lit.IsPos => def dists = dist_lit.atom.term1.Children.ToArray () def i1 = System.Array.IndexOf (dists, d1) def i2 = System.Array.IndexOf (dists, d2) assert (i1 >= 0 && i2 >= 0) def loop (acc, i1, i2) if (i1 > 0) loop (E.App ("distinct_skip1", [acc]), i1 - 1, i2) else if (i2 > 0) loop (E.App ("distinct_skip2", [acc]), i1, i2 - 1) else acc def (last, acc) = if (i1 < i2) (i2, loop (get_lit (dist_lit), i1, i2 - i1 - 1)) else (i1, loop (get_lit (dist_lit), i2, i1 - i2 - 1)) def acc = if (last == dists.Length - 1) acc else E.App ("distinct_skip3", [acc]) def acc = E.App ("distinct_to_neq", [acc]) if (i1 < i2) acc else E.App ("neq_symm", [acc]) | _ => fake_neq ("wrong_dist", d1, d2) def proof_of_false = match (core.ProofObject) | Rule2 ("impossible-merge", Rule3 ("distinct", EqProof (d1, t1), EqProof (d2, t2), dist_proof), proof) => def neq = get_distinct_proof (d1, d2, dist_proof) finish (t1, d1, t2, d2, neq, proof) | Rule2 ("impossible-merge", Rule3 ("cannot-merge", EqProof (d1, t1), EqProof (d2, t2), neq_proof), proof) => finish (t1, d1, t2, d2, get_neq_proof (d1, d2, neq_proof), proof) | Rule2 ("forbid-merge", neq_proof, EqProof (t1, t2)) => def neq = get_neq_proof (t1, t2, neq_proof) def eq = t1.EProofOfEqualityWith (get_lit, t2) E.App ("excl_mid_np", [neq, eq]) | Rule3 ("direct-distinct", EqProof (t1, root), EqProof (t2, root'), dist_proof) => assert (root === root') def neq = get_distinct_proof (t1, t2, dist_proof) def eq = t1.EProofOfEqualityWith (get_lit, t2) E.App ("excl_mid_np", [neq, eq]) | _ => null def proof_of_false = if (proof_of_false == null || proof_of_false.IsFake) def res = ProcessArithProof (get_lit, clause) if (res == null) log (INFO, $ "failed to find arith proof for $clause") E.App ("eq_fake", [E.Ref ("strange-proof-object"), E.Ref ("false")]) else res else proof_of_false E.Fun ($[ ( $"eq$(literals [~l])", E.Lit (~l) ) | l in clause.Lits ], proof_of_false) BuildProof (c : Clause) : E match (c.Proof) | Resolution as r => if (Driver.ResolutionProofs) ResolutionProofWithAssume (c, r) else null | TheoryConflict => def atom = c.Lits [0].atom if (c.Lits.Length == 1 && c.Lits [0].IsPos && atom.term1 === atom.term2 && atom.term1 === core.TermPool.True) E.Ref ("true_false") else core.PushState () foreach (l in c.Lits) core.Assert (~l) unless (core.Refuted) core.FinalCheck (true) assert (core.Refuted, $"c=$c") def res = ProcessEqProof (c) comment = core.ProofObject.ToString () core.PopState () res | InitialFormula => null | Skolemize => assert (false, "shouldn't happen in skolemized NNF") /* def inst = FindInst (c) say ($ "c$(dumped[c]): LEMMA % skolemization $inst\n") say_clause (c) */ | Instantiate => if (Driver.InstProofs) def inst = FindInst (c) def (conv, qatom, i) = if (c.Lits [0].atom.IsQuantified) ("to_clause_1", c.Lits [0].atom, c.Lits [1]) else ("to_clause_2", c.Lits [1].atom, c.Lits [0]) def (conv, i) = if (i.IsNeg) (conv + "_sn", ~i) else (conv, i) _ = i def args = inst.Map ((_, t) => E.Term (t, prop = false)) def q = E.Term (qatom.term1, prop = true) def inside = args.FoldLeft (E.App ("id", [q]), (arg, acc) => E.App ("inst", [arg, acc])) E.App (conv, [inside]) else null | And => if (Driver.AndProofs) def (par, ch) = FindDeep2 (c) mutable s = E.Ref ("par") def loop (_) | [_] => {} | x :: xs => def args = [E.InfTerm (() => x, true), E.InfTerm (() => core.TermPool.Get ("and", xs), true), s] if (core.TermToLiteral (0, x) === ch) s = E.App ("and_get", args) else s = E.App ("and_skip", args) loop (xs) | [] => assert (false) loop (par.atom.term1.Children) def parms = $[(if (l === par) "par" else "ch", E.Lit (~l)) | l in c.Lits] def suf = if (ch.IsNeg) "pn" else "np" E.Fun (parms, E.App ("excl_mid_" + suf, [E.Ref ("ch"), s])) else null | Or => if (Driver.OrProofs) def (par, rest) = FindDeep (c) def numbers = Hashtable () foreach (l in rest) numbers [l] = numbers.Count mutable s = E.Ref ("par") def loop (_) | l :: ls => def l = core.TermToLiteral (0, l) def suf = if (l.IsNeg) "pn" else "np" def tail = [E.Ref ($ "p$(numbers[l])"), s] s = if (ls is []) E.App ($"excl_mid_$suf", tail) else E.App ($"unit_res_$suf", tail) loop (ls) | [] => {} loop (par.atom.term1.Children) E.Fun ($[(if (l === par) "par" else $"p$(numbers[l])", E.Lit (~l)) | l in c.Lits], s) else null | NegOr \ | NegAnd => log (INFO, $"shouldn't happen in skolemized NNF: $c") null Save (c : Clause) : void if (dumped.Contains (c)) {} else def name = $"c$(dumped.Count)" dumped [c] = dumped.Count comment = c.Proof.GetType().Name def proof = BuildProof (c) lemmas ::= Lemma (name, comment, c, proof) public this (c : Core) core = c public Run (l : list [Lemma], root : Clause, initial : Clause) : list [Lemma] lemmas = l Save (initial) Save (root) lemmas.Rev ()