Module Wp.AutoSource

Basic Strategies

It is always safe to apply strategies to any goal.

Sourceval array : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval choice : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval absurd : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval compound : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval cut : ?priority:float -> ?modus:bool -> Tactical.selection -> Strategy.strategy
Sourceval filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy
Sourceval havoc : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval separated : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval instance : ?priority:float -> Tactical.selection -> Tactical.selection list -> Strategy.strategy
Sourceval lemma : ?priority:float -> ?at:Tactical.selection -> string -> Tactical.selection list -> Strategy.strategy
Sourceval intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval range : ?priority:float -> Tactical.selection -> vmin:int -> vmax:int -> Strategy.strategy
Sourceval split : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval definition : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval compute : ?priority:float -> Tactical.selection -> Strategy.strategy

Registered Heuristics

Sourceval auto_split : Strategy.heuristic
Sourceval auto_range : Strategy.heuristic
Sourcemodule Range : sig ... end

Trusted Tactical Process

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

Sourceval t_absurd : Tactical.process

Find a contradiction.

Keep goal unchanged.

Sourceval t_finally : string -> Tactical.process

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

Sourceval t_descr : string -> Tactical.process -> Tactical.process

Apply a description to each sub-goal

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

Split with p and not p.

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

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

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

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

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

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

Sourceval t_range : Lang.F.term -> int -> int -> upper:Tactical.process -> lower:Tactical.process -> range:Tactical.process -> Tactical.process
Sourceval t_replace : ?equal:string -> src:Lang.F.term -> tgt:Lang.F.term -> Tactical.process -> Tactical.process

Prove src=tgt then replace src by tgt.