package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Proof format used by the proof-generating procedures. It is fairly close to Coq format but a bit more liberal.

It is used for proofs over Z, Q, R. However, certain constructions e.g. CutPrf are only relevant for Z.

type prf_rule =
  1. | Annot of string * prf_rule
  2. | Hyp of int
  3. | Def of int
  4. | Cst of NumCompat.Q.t
  5. | Zero
  6. | Square of Vect.t
  7. | MulC of Vect.t * prf_rule
  8. | Gcd of NumCompat.Z.t * prf_rule
  9. | MulPrf of prf_rule * prf_rule
  10. | AddPrf of prf_rule * prf_rule
  11. | CutPrf of prf_rule
type proof =
  1. | Done
  2. | Step of int * prf_rule * proof
  3. | Split of int * Vect.t * proof * proof
  4. | Enum of int * prf_rule * Vect.t * prf_rule * proof list
  5. | ExProof of int * int * int * var * var * var * proof
val pr_size : prf_rule -> NumCompat.Q.t
val pr_rule_max_def : prf_rule -> int
val pr_rule_max_hyp : prf_rule -> int
val proof_max_def : proof -> int
val normalise_proof : int -> proof -> int * proof
val output_prf_rule : Stdlib.out_channel -> prf_rule -> unit
val output_proof : Stdlib.out_channel -> proof -> unit
val add_proof : prf_rule -> prf_rule -> prf_rule
val mul_cst_proof : NumCompat.Q.t -> prf_rule -> prf_rule
val mul_proof : prf_rule -> prf_rule -> prf_rule
val compile_proof : int list -> proof -> Micromega.zArithProof
val cmpl_prf_rule : ('a Micromega.pExpr -> 'a Micromega.pol) -> (NumCompat.Q.t -> 'a) -> prf_rule list -> prf_rule -> 'a Micromega.psatz
val proof_of_farkas : prf_rule Mutils.IMap.t -> Vect.t -> prf_rule
val eval_prf_rule : (int -> LinPoly.t * op) -> prf_rule -> LinPoly.t * op
val eval_proof : (LinPoly.t * op) Mutils.IMap.t -> proof -> bool
val simplify_proof : proof -> proof * Mutils.ISet.t
module PrfRuleMap : Stdlib.Map.S with type key = prf_rule
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct