src/Tools/Metis/src/Proof.sml

The Metis prover (slightly modified version from Larry);

(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC                                               *)
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
(* ========================================================================= *)

structure Proof :> Proof =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* A type of first order logic proofs.                                       *)
(* ------------------------------------------------------------------------- *)

datatype inference =
    Axiom of LiteralSet.set
  | Assume of Atom.atom
  | Subst of Subst.subst * Thm.thm
  | Resolve of Atom.atom * Thm.thm * Thm.thm
  | Refl of Term.term
  | Equality of Literal.literal * Term.path * Term.term;

type proof = (Thm.thm * inference) list;

(* ------------------------------------------------------------------------- *)
(* Printing.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun inferenceType (Axiom _) = Thm.Axiom
  | inferenceType (Assume _) = Thm.Assume
  | inferenceType (Subst _) = Thm.Subst
  | inferenceType (Resolve _) = Thm.Resolve
  | inferenceType (Refl _) = Thm.Refl
  | inferenceType (Equality _) = Thm.Equality;

local
  open Parser;

  fun ppAssume pp atm = (addBreak pp (1,0); Atom.pp pp atm);

  fun ppSubst ppThm pp (sub,thm) =
      (addBreak pp (1,0);
       beginBlock pp Inconsistent 1;
       addString pp "{";
       ppBinop " =" ppString Subst.pp pp ("sub",sub);
       addString pp ","; addBreak pp (1,0);
       ppBinop " =" ppString ppThm pp ("thm",thm);
       addString pp "}";
       endBlock pp);

  fun ppResolve ppThm pp (res,pos,neg) =
      (addBreak pp (1,0);
       beginBlock pp Inconsistent 1;
       addString pp "{";
       ppBinop " =" ppString Atom.pp pp ("res",res);
       addString pp ","; addBreak pp (1,0);
       ppBinop " =" ppString ppThm pp ("pos",pos);
       addString pp ","; addBreak pp (1,0);
       ppBinop " =" ppString ppThm pp ("neg",neg);
       addString pp "}";
       endBlock pp);

  fun ppRefl pp tm = (addBreak pp (1,0); Term.pp pp tm);

  fun ppEquality pp (lit,path,res) =
      (addBreak pp (1,0);
       beginBlock pp Inconsistent 1;
       addString pp "{";
       ppBinop " =" ppString Literal.pp pp ("lit",lit);
       addString pp ","; addBreak pp (1,0);
       ppBinop " =" ppString (ppList ppInt) pp ("path",path);
       addString pp ","; addBreak pp (1,0);
       ppBinop " =" ppString Term.pp pp ("res",res);
       addString pp "}";
       endBlock pp);

  fun ppInf ppAxiom ppThm pp inf =
      let
        val infString = Thm.inferenceTypeToString (inferenceType inf)
      in
        beginBlock pp Inconsistent (size infString + 1);
        ppString pp infString;
        case inf of
          Axiom cl => ppAxiom pp cl
        | Assume x => ppAssume pp x
        | Subst x => ppSubst ppThm pp x
        | Resolve x => ppResolve ppThm pp x
        | Refl x => ppRefl pp x
        | Equality x => ppEquality pp x;
        endBlock pp
      end;

  fun ppAxiom pp cl =
      (addBreak pp (1,0);
       ppMap
         LiteralSet.toList
         (ppBracket "{" "}" (ppSequence "," Literal.pp)) pp cl);
in
  val ppInference = ppInf ppAxiom Thm.pp;

  fun pp p prf =
      let
        fun thmString n = "(" ^ Int.toString n ^ ")"
                          
        val prf = enumerate prf

        fun ppThm p th =
            let
              val cl = Thm.clause th

              fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl
            in
              case List.find pred prf of
                NONE => addString p "(???)"
              | SOME (n,_) => addString p (thmString n)
            end

        fun ppStep (n,(th,inf)) =
            let
              val s = thmString n
            in
              beginBlock p Consistent (1 + size s);
              addString p (s ^ " ");
              Thm.pp p th;
              addBreak p (2,0);
              ppBracket "[" "]" (ppInf (K (K ())) ppThm) p inf;
              endBlock p;
              addNewline p
            end
      in
        beginBlock p Consistent 0;
        addString p "START OF PROOF";
        addNewline p;
        app ppStep prf;
        addString p "END OF PROOF";
        addNewline p;
        endBlock p
      end
(*DEBUG
      handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
*)

end;

val inferenceToString = Parser.toString ppInference;

val toString = Parser.toString pp;

(* ------------------------------------------------------------------------- *)
(* Reconstructing single inferences.                                         *)
(* ------------------------------------------------------------------------- *)

fun inferenceToThm (Axiom cl) = Thm.axiom cl
  | inferenceToThm (Assume atm) = Thm.assume (true,atm)
  | inferenceToThm (Subst (sub,th)) = Thm.subst sub th
  | inferenceToThm (Resolve (atm,th,th')) = Thm.resolve (true,atm) th th'
  | inferenceToThm (Refl tm) = Thm.refl tm
  | inferenceToThm (Equality (lit,path,r)) = Thm.equality lit path r;

local
  fun reconstructSubst cl cl' =
      let
        fun recon [] =
            let
(*TRACE3
              val () = Parser.ppTrace LiteralSet.pp "reconstructSubst: cl" cl
              val () = Parser.ppTrace LiteralSet.pp "reconstructSubst: cl'" cl'
*)
            in
              raise Bug "can't reconstruct Subst rule"
            end
          | recon (([],sub) :: others) =
            if LiteralSet.equal (LiteralSet.subst sub cl) cl' then sub
            else recon others
          | recon ((lit :: lits, sub) :: others) =
            let
              fun checkLit (lit',acc) =
                  case total (Literal.match sub lit) lit' of
                    NONE => acc
                  | SOME sub => (lits,sub) :: acc
            in
              recon (LiteralSet.foldl checkLit others cl')
            end
      in
        Subst.normalize (recon [(LiteralSet.toList cl, Subst.empty)])
      end
(*DEBUG
      handle Error err =>
        raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err);
*)

  fun reconstructResolvant cl1 cl2 cl =
      (if not (LiteralSet.subset cl1 cl) then
         LiteralSet.pick (LiteralSet.difference cl1 cl)
       else if not (LiteralSet.subset cl2 cl) then
         Literal.negate (LiteralSet.pick (LiteralSet.difference cl2 cl))
       else
         (* A useless resolution, but we must reconstruct it anyway *)
         let
           val cl1' = LiteralSet.negate cl1
           and cl2' = LiteralSet.negate cl2
           val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2']
         in
           if not (LiteralSet.null lits) then LiteralSet.pick lits
           else raise Bug "can't reconstruct Resolve rule"
         end)
(*DEBUG
      handle Error err =>
        raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err);
*)

  fun reconstructEquality cl =
      let
(*TRACE3
        val () = Parser.ppTrace LiteralSet.pp "Proof.reconstructEquality: cl" cl
*)

        fun sync s t path (f,a) (f',a') =
            if f <> f' orelse length a <> length a' then NONE
            else
              case List.filter (op<> o snd) (enumerate (zip a a')) of
                [(i,(tm,tm'))] =>
                let
                  val path = i :: path
                in
                  if tm = s andalso tm' = t then SOME (rev path)
                  else 
                    case (tm,tm') of
                      (Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a'
                    | _ => NONE
                end
              | _ => NONE

        fun recon (neq,(pol,atm),(pol',atm')) =
            if pol = pol' then NONE
            else
              let
                val (s,t) = Literal.destNeq neq

                val path =
                    if s <> t then sync s t [] atm atm'
                    else if atm <> atm' then NONE
                    else Atom.find (equal s) atm
              in
                case path of
                  SOME path => SOME ((pol',atm),path,t)
                | NONE => NONE
              end

        val candidates =
            case List.partition Literal.isNeq (LiteralSet.toList cl) of
              ([l1],[l2,l3]) => [(l1,l2,l3),(l1,l3,l2)]
            | ([l1,l2],[l3]) => [(l1,l2,l3),(l1,l3,l2),(l2,l1,l3),(l2,l3,l1)]
            | ([l1],[l2]) => [(l1,l1,l2),(l1,l2,l1)]
            | _ => raise Bug "reconstructEquality: malformed"

(*TRACE3
        val ppCands =
            Parser.ppList (Parser.ppTriple Literal.pp Literal.pp Literal.pp)
        val () = Parser.ppTrace ppCands
                   "Proof.reconstructEquality: candidates" candidates
*)
      in
        case first recon candidates of
          SOME info => info
        | NONE => raise Bug "can't reconstruct Equality rule"
      end
(*DEBUG
      handle Error err =>
        raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err);
*)

  fun reconstruct cl (Thm.Axiom,[]) = Axiom cl
    | reconstruct cl (Thm.Assume,[]) =
      (case LiteralSet.findl Literal.positive cl of
         SOME (_,atm) => Assume atm
       | NONE => raise Bug "malformed Assume inference")
    | reconstruct cl (Thm.Subst,[th]) =
      Subst (reconstructSubst (Thm.clause th) cl, th)
    | reconstruct cl (Thm.Resolve,[th1,th2]) =
      let
        val cl1 = Thm.clause th1
        and cl2 = Thm.clause th2
        val (pol,atm) = reconstructResolvant cl1 cl2 cl
      in
        if pol then Resolve (atm,th1,th2) else Resolve (atm,th2,th1)
      end
    | reconstruct cl (Thm.Refl,[]) =
      (case LiteralSet.findl (K true) cl of
         SOME lit => Refl (Literal.destRefl lit)
       | NONE => raise Bug "malformed Refl inference")
    | reconstruct cl (Thm.Equality,[]) = Equality (reconstructEquality cl)
    | reconstruct _ _ = raise Bug "malformed inference";
in
  fun thmToInference th =
      let
(*TRACE3
        val () = Parser.ppTrace Thm.pp "Proof.thmToInference: th" th
*)

        val cl = Thm.clause th

        val thmInf = Thm.inference th

(*TRACE3
        val ppThmInf = Parser.ppPair Thm.ppInferenceType (Parser.ppList Thm.pp)
        val () = Parser.ppTrace ppThmInf "Proof.thmToInference: thmInf" thmInf
*)

        val inf = reconstruct cl thmInf

(*TRACE3
        val () = Parser.ppTrace ppInference "Proof.thmToInference: inf" inf
*)
(*DEBUG
        val () =
            let
              val th' = inferenceToThm inf
            in
              if LiteralSet.equal (Thm.clause th') cl then ()
              else
                raise
                  Bug
                    ("Proof.thmToInference: bad inference reconstruction:" ^
                     "\n  th = " ^ Thm.toString th ^
                     "\n  inf = " ^ inferenceToString inf ^
                     "\n  inf th = " ^ Thm.toString th')
            end
*)
      in
        inf
      end
(*DEBUG
      handle Error err =>
        raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err);
*)
end;

(* ------------------------------------------------------------------------- *)
(* Reconstructing whole proofs.                                              *)
(* ------------------------------------------------------------------------- *)

local
  fun thmCompare (th1,th2) =
      LiteralSet.compare (Thm.clause th1, Thm.clause th2);

  fun buildProof (th,(m,l)) =
      if Map.inDomain th m then (m,l)
      else
        let
          val (_,deps) = Thm.inference th
          val (m,l) = foldl buildProof (m,l) deps
        in
          if Map.inDomain th m then (m,l)
          else
            let
              val l = (th, thmToInference th) :: l
            in
              (Map.insert m (th,l), l)
            end
        end;
in
  fun proof th =
      let
(*TRACE3
        val () = Parser.ppTrace Thm.pp "Proof.proof: th" th
*)
        val (m,_) = buildProof (th, (Map.new thmCompare, []))
(*TRACE3
        val () = Parser.ppTrace Parser.ppInt "Proof.proof: size" (Map.size m)
*)
      in
        case Map.peek m th of
          SOME l => rev l
        | NONE => raise Bug "Proof.proof"
      end;
end;

end