Module Logtk_proofs.LLProofSource

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.

Sourcetype ty = term
Sourcetype form = term
Sourcetype inst = term list

Instantiate some binder with the following terms. Order matters.

Sourcetype name = string
Sourcetype t
Sourcetype 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;
    }
Sourceand parent = {
  1. p_proof : t;
  2. p_inst : inst;
}
Sourceval id : t -> int
Sourceval concl : t -> form
Sourceval step : t -> step
Sourceval parents : t -> parent list
Sourceval premises : t -> t list
Sourceval p_of : t -> parent
Sourceval p_inst : t -> inst -> parent

Print only this step

Print the whole DAG

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

Checking steps

Sourcetype check_res =
  1. | R_ok
  2. | R_fail
  3. | R_skip
Sourceval get_check_res : t -> check_res option
Sourceval set_check_res : t -> check_res -> unit

Printing

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