Module Wp.Auto

module Auto: sig .. end

Basic Strategies

It is always safe to apply strategies to any goal.

val array : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val choice : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val absurd : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val contrapose : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val compound : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val cut : ?priority:float ->
       ?modus:bool -> Wp.Tactical.selection -> Wp.Strategy.strategy

val filter : ?priority:float -> ?anti:bool -> unit -> Wp.Strategy.strategy

val havoc : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val separated : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val instance : ?priority:float ->
       Wp.Tactical.selection -> Wp.Tactical.selection list -> Wp.Strategy.strategy

val lemma : ?priority:float ->
       ?at:Wp.Tactical.selection ->
       string -> Wp.Tactical.selection list -> Wp.Strategy.strategy

val intuition : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val range : ?priority:float ->
       Wp.Tactical.selection -> vmin:int -> vmax:int -> Wp.Strategy.strategy

val split : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

val definition : ?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy

Registered Heuristics

val auto_split : Wp.Strategy.heuristic

val auto_range : Wp.Strategy.heuristic

module Range: sig .. end

Trusted Tactical Process

Tacticals with hand-written process are not safe. However, the combinators below are guarantied to be sound.

val t_absurd : Wp.Tactical.process

Find a contradiction.

val t_id : Wp.Tactical.process

Keep goal unchanged.

val t_finally : string -> Wp.Tactical.process

Apply a description to a leaf goal. Same as t_descr "..." t_id.

val t_descr : string -> Wp.Tactical.process -> Wp.Tactical.process

Apply a description to each sub-goal

val t_split : ?pos:string -> ?neg:string -> Wp.Lang.F.pred -> Wp.Tactical.process

Split with p and not p.

val t_cut : ?by:string -> Wp.Lang.F.pred -> Wp.Tactical.process -> Wp.Tactical.process

Prove condition p and use-it as a forward hypothesis.

val t_case : Wp.Lang.F.pred ->
       Wp.Tactical.process -> Wp.Tactical.process -> Wp.Tactical.process

Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.

val t_cases : ?complete:string ->
       (Wp.Lang.F.pred * Wp.Tactical.process) list -> Wp.Tactical.process

Complete analysis: applies each process under its guard, and proves that all guards are complete.

val t_chain : Wp.Tactical.process -> Wp.Tactical.process -> Wp.Tactical.process

Apply second process to every goal generated by the first one.

val t_range : Wp.Lang.F.term ->
       int ->
       int ->
       upper:Wp.Tactical.process ->
       lower:Wp.Tactical.process -> range:Wp.Tactical.process -> Wp.Tactical.process

Raises Invalid_argument when range is empty

val t_replace : ?equal:string ->
       src:Wp.Lang.F.term ->
       tgt:Wp.Lang.F.term -> Wp.Tactical.process -> Wp.Tactical.process

Prove src=tgt then replace src by tgt.