• Home
• About Coq
• Get Coq
• Documentation
• Community

Library Random.Prelude

• Preliminaries
  • Definition of iterator comp
  • Monotonicity of sequences for an arbitrary relation
  • Reducing if constructs
  • Classical reasoning

Library Random.Ubase

• Ubase.v: Specification of , interval
  • Basic operators of
  • Basic Properties
  • Least upper bound, corresponds to limit for increasing sequences

Library Random.Uprop

• Uprop.v : Properties of operators on [0,1]
  • Direct consequences of axioms
  • Properties of == derived from properties of
  • U is a setoid
  • Definition and properties of
    • Properties of
    • Properties of
  • Properties of and
  • More properties on + and * and Uinv
  • Disequality
    • Properties of <
    • Compatibility of operations with respect to order.
    • More Properties
  • Definition of
  • Definition and properties of
  • Definition and properties of
  • Definition and properties of max
  • Definition and properties of min
  • Other properties
  • Definition and properties of generalized sums
  • Definition and properties of generalized products
  • Properties of Unth
    • Mean of two numbers :
    • Properties of
  • Density
  • Properties of least upper bounds
  • Greatest lower bounds
    • Definitions
    • Elementary properties
    • Defining morphisms
  • Fixpoints of functions of type
  • Properties of barycenter of two points
  • Properties of generalized sums sigma
  • Product by an integer
    • Definition of Nmult n x written n */ x
    • Condition for n */ x to be exact : or
    • Properties of n */ x
  • Conversion from booleans to U
  • Particular sequences
    • Properties of the invariant
  • Tactic for simplification of goals
  • Intervals
    • Definition
    • Relations
    • Properties
    • Operations on intervals
    • limits
    • Fixpoints

Library Random.Monads

• Monads.v: Monads for randomized constructions
  • Definition of monadic operators
  • Properties of monadic operators
  • Properties of distributions
    • Expected properties of measures
    • Stability for equality
    • Monotonicity
    • Stability for inversion
    • Stability for addition
    • Stability for product
    • Continuity

Library Random.Probas

• Probas.v: The monad for distributions
  • Definition of distribution
  • Properties of measures
  • Monadic operators for distributions
  • Operations on distributions
  • Properties of monadic operators
  • A specific distribution
  • Least upper bound of increasing sequences of distributions
  • Distribution for flip
  • Uniform distribution beween 0 and n
    • Definition of fnth
    • Basic properties of fnth
    • Distribution for random n
    • Properties of random
• Nondeterministic choice

Library Random.Prog

• Prog.v: Composition of distributions
  • Conditional
  • Fixpoints
    • Hypotheses
    • Iteration of the functional from the -distribution
    • Definition
    • Properties
  • Continuity
• Prog.v: Axiomatic semantics
  • Definition of correctness judgements
  • Stability properties
  • Basic rules
    • Rules for application
    • Rules for abstraction
    • Rule for conditional
    • Rule for fixpoints
    • Rules using commutation properties
  • Rules for intervals
    • Stability
    • Rule for values
    • Rule for application
    • Rule for abstraction
    • Rule for conditional
    • Rule for fixpoints
  • Rules for Flip
  • Rules for total (well-founded) fixpoints

Library Random.IterFlip

• IterFlip.v: An example of probabilistic termination
  • Definition of a random walk
  • Main result
    • Auxiliary function
    • Proof of probabilistic termination

Library Random.Choice

• Choice.v: An example of probabilistic choice
  • Definition of a probabilistic choice
  • Main result
    • Assumptions
    • Proof of estimation

Library Random.Nelist

• Nelist.v: A general theory of non empty lists on Type

Library Random.Sets

• Sets.v: Definition of sets as predicates over a type A
  • Equivalence
  • Setoid structure
  • Finite sets given as an enumeration of elements
    • Emptyness is decidable for finite sets
    • Size of a finite set
  • Inclusion
  • Properties of operations on sets
  • Removing an element from a finite set
  • Decidable sets
    • Filter operation
    • Selecting elements in a finite set

Library Random.Carac

• Carac.v: Characteristic functions
  • Modular reasoning on programs
  • Uniform measure on finite sets
    • Distribution for random_fin P over
    • Definition and Properties of random_fin

Library Random.Bernoulli

• Bernoulli.v: Simulating Bernoulli and Binomial distributions
  • Program for computing a Bernoulli distribution
  • Properties of the Bernoulli program
    • Proofs using fixpoint rules
    • p is an invariant of Mubern qtrue
    • Proofs using lubs
  • Binomial distribution
    • Definition and properties of binomial coefficients
    • Definition of binomial distribution
    • Properties of binomial distribution

Library Random.Ycart

• Ycart.v: Axiomatisation of the uniform measure
  • Interval [0,x]
• Ycart.v: An exemple of partial termination
  • Program giving an example of partiality
  • Properties of Ycart

Library Random.Transitions

• Transitions.v: Probabilistic Deterministic Transition System
  • One step of probabilistic transition
  • Extension to distributions on sequences of length k

• webmaster
• xhtml valid
• CSS valid