Module Proof.Step

An inference step is composed of a set of premises, a rule, a status (theorem/trivial/equisatisfiable…), and is used to deduce new result using these premises and metadata.

A single step can be used to deduce several results.

type t = step
val kind : t -> kind
val parents : t -> parent list
val infos : t -> infos
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
val src : t -> source option
val tags : t -> tag list
val trivial : t
val by_def : ID.t -> t
val define : ID.t -> source -> parent list -> t
val define_internal : ID.t -> parent list -> t
val lemma : source -> t
val intro : source -> role -> t
val assert_ : source -> t
val assert' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val goal : source -> t
val goal' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val inferences_performed : t -> int
val count_rules : name:string -> t -> int
val has_ho_step : t -> bool
val inference : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
val simp : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
val esa : ?infos:infos -> rule:rule -> parent list -> t
val to_attrs : t -> UntypedAST.attrs
val is_inference : t -> bool
val is_simpl : ?name:String.t option -> step -> bool
val is_trivial : t -> bool
val is_by_def : t -> bool
val is_assert : t -> bool

Proof: the statement was asserted in some file

val is_goal : t -> bool

The statement comes from the negation of a goal in some file

val rule : t -> rule option

Rule name for Esa/Simplification/Inference steps

val distance_to_goal : t -> int option

distance_to_conjecture p returns None if p has no ancestor that is a conjecture (including p itself). It returns Some d if d is the distance, in the proof graph, to the closest conjecture ancestor of p