Module Logtk_proofs.LLProof

Low Level Proofs

Low level proofs, intended for mechanical proof checking.

Instantiations (substitutions) are explicit because that should make the job of the checker easier.

NOTE: this is still uncooked, and will probably change.

val section : Logtk.Util.Section.t
type term = Logtk.TypedSTerm.t
type ty = term
type form = term
type inst = term list

Instantiate some binder with the following terms. Order matters.

type tag = Logtk.Proof.tag
type name = string
type t
type step =
  1. | Goal
  2. | Assert
  3. | Negated_goal of t
  4. | Trivial
  5. | By_def of Logtk.ID.t
  6. | Define of Logtk.ID.t
  7. | Instantiate of {
    1. form : t;
    2. inst : inst;
    3. tags : tag list;
    }
  8. | Esa of name * t list
  9. | Inference of {
    1. intros : term list;
    2. local_intros : term list;
    3. name : name;
    4. parents : parent list;
    5. tags : tag list;
    }
and parent = {
  1. p_proof : t;
  2. p_inst : inst;
}
val id : t -> int
val concl : t -> form
val step : t -> step
val parents : t -> parent list
val premises : t -> t list
val p_of : t -> parent
val p_inst : t -> inst -> parent
val pp_step : step CCFormat.printer
val pp_parent : parent CCFormat.printer
val pp_id : t CCFormat.printer
val pp_res : t CCFormat.printer

Print only this step

val pp_dag : t CCFormat.printer

Print the whole DAG

val pp_inst : inst CCFormat.printer
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val goal : form -> t
val negated_goal : form -> t -> t
val assert_ : form -> t
val trivial : form -> t
val by_def : Logtk.ID.t -> form -> t
val define : Logtk.ID.t -> form -> t
val instantiate : ?tags:tag list -> form -> t -> inst -> t
val esa : form -> name -> t list -> t
val inference : intros:term list -> local_intros:term list -> tags:tag list -> form -> name -> parent list -> t

Checking steps

type check_res =
  1. | R_ok
  2. | R_fail
  3. | R_skip
val get_check_res : t -> check_res option
val set_check_res : t -> check_res -> unit
val pp_check_res : check_res CCFormat.printer

Printing

module Tbl : CCHashtbl.S with type key = t
module Dot : sig ... end