• Basics
  • Some results about Z
• Classical Logic
  • Classical or
  • Classical Existential
  • Pidgeon Hole Principle
  • Decidability of connectives
• Extending the Coq Logic
  • Basics
  • CProp-valued Relations
  • Prop-valued Relations
  • The relation le, lt, odd and even in CProp
  • Miscellaneous
  • Results about the natural numbers
  • Algebraic Properties
  • Logical Properties
  • Integers
• N
  • About N
    • Apartness
    • Addition
    • Multiplication
    • Decidability
  • N⁺
• Lazy Nat
  • Successor
  • Predecessor
  • Addition
  • Multiplication
• Z
  • About Z
    • Apartness
    • Addition
    • Multiplication
    • Miscellaneous
• Basic facts on Z
  • Arithmetic over nat
  • Arithmetic over Z
  • Facts on inequalities over Z
  • Facts on the absolute value-function over Z
  • Facts on the sign-function over Z
• The Divides-function over Z
• The GCD-function over Z
  • GCD over `positive'
  • GCD over Z
  • Relative primality
  • Primes
• Working modulo a positive number over Z
  • Facts on `mod'
• CProp-valued lemmas about 'mod'
• Q
  • About Q
    • Constants
    • Equality
    • Apartness
    • Addition
    • Opposite
    • Multiplication
    • Inverse
    • Less-than
    • Miscellaneous
• Classic Setoids
  • Morhpisms between Setoids
  • Basic Combinators for Setoids
• Partial Order
  • Dual Order
  • Default Monotone and Antitone
• SemiLattice
• Lattice
  • Dual Latice
• Total Order
  • Dual Total Order
  • Default meet and join.
  • Example of a Total Order: <Z, Zle, Zmin, Zmax>
  • Example of a Total Order: <Q, Qle, Qmin, Qmax>
• Setoids
  • Relations necessary for Setoids
  • Definition of Setoid
  • Setoid axioms
  • Setoid basics
  • The product of setoids
  • Relations and predicates
    • Predicates
    • Definition of a setoid predicate
    • Relations
    • Definition of a setoid relation
    • CProp Relations
    • Definition of a CProp setoid relation
  • Functions between setoids
  • The unary and binary (inner) operations on a csetoid
  • The binary outer operations on a csetoid
  • Subsetoids
    • Subsetoid unary operations
    • Subsetoid binary operations
  • Miscellaneous
  • The Setoid of Setoid functions
  • Nullary and n-ary operations
  • Composition of Setoid functions
    • Composition as operation
    • Projections
  • Combining operations
  • The Free Setoid
  • Partial Functions
    • Subsets of Setoids
    • Operations
  • Bijections
  • Inclusion
  • Example of a setoid: N
    • Addition
    • Multiplication
    • Ternary addition
  • Example of a setoid: N⁺
    • Setoid
    • Addition and multiplication
  • Example of a setoid: Z
    • Z
    • Addition
    • Opposite
    • Multiplication
    • Zero
  • Example of a setoid: Q
    • Setoid
    • Addition
    • Opposite
    • Multiplication
    • Less-than
  • Example of a setoid: setoids with two elements
  • Setoids of the first n natural numbers
  • Setoids of the integers between 0 and z
• Semigroups
  • Definition of the notion of semigroup
  • Semigroup axioms
  • Semigroup basics
  • Morphism
  • About the unit
  • Functional operations
  • Subsemigroups
  • Direct Product
  • The SemiGroup of Setoid functions
  • The Free SemiGroup
  • Example of a semi-group: ⟨N,+⟩
  • Examples of semi-groups: ⟨N⁺,+⟩ and ⟨N⁺,×⟩
    • ⟨N⁺,+⟩
    • ⟨N⁺,×⟩
  • Examples of semi-groups: ⟨Z,+⟩ and ⟨Z,×⟩
    • ⟨Z,+⟩
    • ⟨Z,×⟩
  • Examples of semi-groups: ⟨Q,+⟩ and ⟨Q,×⟩
    • ⟨Q,+⟩
    • ⟨Q,×⟩
  • Example of a semigroup: semigroups with two elements
• Monoids
  • Definition of monoids
  • Monoid axioms
  • Monoid basics
  • Submonoids
  • Morphism, isomorphism and automorphism of Monoids
  • Power in a monoid
  • Cyclicity
  • Invertability
  • Direct Product
  • The Monoids of Setoid functions and bijective Setoid functions.
  • The free Monoid
  • The unit in the setoid of Setoid functions
  • Intersection
  • Example of a monoid: ⟨N,+⟩
  • A function from the natural numbers to a cyclic monoid
  • A morphism from a free monoid to the natural numbers
  • A morphism from the natural numbers to the free setoid with one element
  • Example of a monoid: ⟨N⁺,×⟩
  • Example of a monoid: monoids with two elements
  • Examples of monoids: ⟨Z,+⟩ and ⟨Z,×⟩
    • ⟨Z,+⟩
    • ⟨Z,×⟩
  • Examples of a monoid: ⟨Q,+⟩ and ⟨Q,×⟩
    • ⟨Q,+⟩
    • ⟨Q,×⟩
  • Non-example of a monoid: ⟨N⁺,+⟩
• Cyclic CMonoids
• Abelian Monoids
  • Subgroups of an Abelian Monoid
• Groups
  • Definition of the notion of Group
  • Group axioms
  • Group basics
  • Sub-groups
  • Associative properties of groups
  • Apartness in Constructive Groups
  • The Group of bijective Setoid functions
  • Functional operations
  • Example of a group: ⟨Z,+⟩
  • Example of a group: ⟨Q,+⟩
  • Non-example of a group: ⟨N,+⟩
  • Non-example of a group: ⟨N⁺,+⟩
• Abelian Groups
  • Subgroups of an Abelian Group
  • Basic properties of Abelian groups
  • Building an abelian group
  • Iteration
  • Example of an abelian group: ⟨Z,+⟩
  • Example of an abelian group: ⟨Q,+⟩
• Sums
• Rings
  • Definition of the notion of Ring
  • Ring axioms
  • Ring constructions
  • Ring unfolded
  • Ring basics
  • Ring Definitions
    • Exponentiation
    • The injection of natural numbers into a ring
    • The injection of integers into a ring
  • Ring sums
    • Infinite Ring sums
    • Ring Sums over Lists
  • Distribution properties
  • Properties of exponentiation (with the exponent in N)
  • Functional Operations
  • Example of a ring: ⟨Z,+,×⟩
  • Example of a ring: ⟨Q,+,×⟩
• Ring Homomorphisms
  • Definition of Ring Homomorphisms
  • Lemmas on Ring Homomorphisms
    • Axioms on Ring Homomorphisms
    • Facts on Ring Homomorphisms
• Ideals and coideals
  • Definition of ideals and coideals
  • Axioms of ideals and coideals
• Quotient Rings
  • QuotRing is a setoid
  • QuotRing is a semigroup
  • QuotRing is a monoid
  • QuotRing is a group
  • QuotRing is an Abelian group
  • QuotRing is a ring
• Modules
  • Definition of the notion of an R-Module
  • Lemmas on Modules
    • Axioms on Modules
    • Facts on Modules
  • Rings are Modules
  • Definition of sub- and comodules
  • Axioms on sub- and comodules
• Quotient Modules
  • QuotMod is a setoid
  • QuotMod is a semigroup
  • QuotMod ia a monoid
  • QuotMod is a group
  • QuotMod is an Abelian group
  • QuotMod is an R-module
• Module Homomorphisms
  • Definition of Module Homomorphisms
  • Lemmas on Module Homomorphisms
    • Axioms on Module Homomorphisms
    • Facts on Module Homomorphisms
• Homomorphism Theorems
  • The homomorphism theorem for modules
    • Cs is a comodule
  • The homomorphism theorem for rings
    • CsR is a coideal
• Fields
  • Definition of the notion Field
  • Field axioms
  • Field basics
  • Properties of multiplication
  • Properties of reciprocal
  • The multiplicative group of nonzeros of a field.
  • Properties of division
  • Cancellation laws for apartness and multiplication
  • Functional Operations
  • Example of a field: ⟨Q,+,×⟩
• Zm
  • Zm is a CSetoid
  • Zm is a CAbGroup
  • Zm is a CRing
  • Zp is a field
    • The inverse element in Zp
• Vector Spaces
• Ordered Fields
  • Definition of the notion of ordered field
  • Ordered field axioms
  • Basics
  • Basic properties of ≤
  • Infinity of ordered fields
    • Properties of one up to four
    • Properties of some other numbers
    • Consequences of infinity
  • Properties of <
    • Addition and subtraction
    • Multiplication and division
    • Miscellaneous properties
  • Properties of ≤
    • Addition and subtraction
    • Multiplication and division
    • Miscellaneous Properties
  • Properties of positive numbers
  • Properties of one over successor
  • Properties of ½
  • Properties of AbsSmall
  • Properties of AbsBig
  • Cauchy sequences
  • Multiplication is continuous
  • Monotonous Functions
  • Example of an ordered field: ⟨Q,+,×,<⟩
• Exponentiation
  • More properties about nexp
  • Definition of zexp: integer exponentiation
  • Properties of zexp
• Q⁺
  • • Equality
    • Addition
    • Multiplicaiton
    • Inverse
    • Tactics
    • Power
    • Summing lists
  • Example of a Total Order: <Qpos, Qpos_le, Qpos_min, Qpos_max>
  • Example of a setoid: Q⁺
    • Setoid
    • Multiplication
    • Inverse
    • Special multiplication and inverse
• Q⁺
  • Example of a semi-group: ⟨Q⁺,(x,y) ↦ xy/2⟩
  • Example of a semi-group: ⟨Q⁺,×⟩
  • Example of a monoid: ⟨Q⁺, (x,y) ↦ xy/2⟩
  • Example of a monoid: ⟨Q⁺,×⟩
  • Example of a group: ⟨Q⁺, (x,y) ↦ xy/2⟩
  • Example of a group: ⟨Q⁺,×⟩
  • Example of an abelian group: ⟨Q⁺, (x,y) ↦ xy/2⟩
  • Example of an abelian group: ⟨Q⁺,×⟩
• Polynomials
  • Definition of polynomials; they form a ring
    • The polynomials form a setoid
    • The polynomials form a semi-group and a monoid
    • The polynomials form a group
    • The polynomials form a ring
  • Apartness, equality, and induction
  • Basic properties of polynomials
    • Constant and identity
    • Application of polynomials
  • Induction properties of polynomials for Prop
  • Bernstein Polynomials
• Polynomials: Nth Coefficient
  • Definitions
  • Properties of nth_coeff
• Degrees of Polynomials
  • Degrees of polynomials over a ring
  • Degrees of polynomials over a field
• An irreducibility criterion
  • Integers modulo p
  • Integer polynomials over Fp
  • Lemmas
  • Working towards the criterion
    • Definitions
    • The criterion
• Polynomials apart from zero
  • Representation of polynomials
  • Polynomials are nonzero on any interval
• Definition of the notion of reals
• The Field of Cauchy Sequences
  • Setoid Structure
  • Group Structure
  • Ring Structure
  • Field Structure
  • Order Structure
  • Other Results
• The Real Number Structure
  • Injection of Q
  • Cauchy Completeness
• Cauchy Real Numbers
• On density of the image of Q in an arbitrary real number structure
  • Injection from Q to an arbitrary real number structure
  • Injection preserves Cauchy property
  • Injection of Q is dense
• Real Number Structures
  • CReals axioms
  • Cauchy sequences
    • Alternative definitions
    • Inequalities of Limits
    • Equivalence of formulations of Cauchy
    • Properties of Cauchy sequences
  • Maximum, Minimum and Absolute Value
    • Maximum
    • Mininum
    • Absolute value
    • Bound of sequence
    • Functional Operators
  • Miscellaneous
    • More properties of Cauchy sequences
    • Subsequences
    • More properties of Exponentiation
    • IR has characteristic zero
• Sums over Reals
• Lists of Real Numbers
• Continuity of Functions on Reals
• Metric Fields
• Continuity of polynomials
• Intermediate Value Theorem
  • Nested intervals
  • Bissections
  • IVT for operations
  • IVT for polynomials
• Roots of polynomials of odd degree
  • Monic polynomials are positive near infinity
  • Flipping a polynomial
  • Sign of a polynomial of odd degree
  • The norm of a polynomial
  • Roots of polynomials of odd degree
• Roots of Real Numbers
  • Existence of roots
  • Square root
  • More on absolute value
  • Cauchy sequences
    • Functional Operators
• Complex Numbers
  • Algebraic structure
  • Properties of i
  • Properties of ℜ and ℑ
  • Properties of conjugation
  • Properties of the real axis
  • C has characteristic zero
• Roots of Complex Numbers
  • Roots of the imaginary unit
  • Roots of complex numbers
• Absolute value on C
  • Properties of AbsCC
  • The triangle inequality
• More properties of complex numbers
  • Sequences and limits
  • Continuity for C
• Technical lemmas for the FTA
  • Key Lemma
  • Main Lemma
  • Kneser Lemma
• Continuity of complex polynomials
• Shifting polynomials
• Reverse of polynomials
• FTA for regular polynomials
  • The Kneser sequence
  • Main results
  • The Kneser sequence is Cauchy in C
• Fundamental Theorem of Algebra
• Search tactics for reasoning in Real Analysis
• Intervals
  • Definitions
  • Totally Bounded
  • Compact sets
• Equality of Partial Functions
  • Definitions
  • Properties of Inclusion
  • Away from Zero
  • The FEQ tactic
  • Properties of Equality
  • Nth Power
• Sums of Functions
• Functions with compact domain
• Continuity
  • Definitions and Basic Results
  • Algebraic Properties
• Correspondence
  • Mappings
  • Mappings Preserve Operations
• Derivatives
  • Basic Properties
  • Algebraic Operations
  • Local Results
• Differentiability
• Nth Derivative
  • Definitions
  • Trivia
  • Basic Results
  • The Nth Derivative
• Generalized Intervals
  • Definitions and Basic Results
  • Constructions with Compact Intervals
  • Properties of Functions in Intervals
• More about Functions
  • Continuity
  • Derivative
  • Differentiability
  • Nth Derivative
• Rolle's Theorem
• Taylor's Theorem
  • First case
  • General case
• Series of Real Numbers
  • Definitions
  • Power Series
  • Operations
  • Almost Everywhere
  • Convergence Criteria
  • Alternate Series
  • Important Numbers
• Sequences of Functions
  • Definitions
  • Irrelevance of Proofs
  • Other Properties
  • Algebraic Properties
• Series of Functions
  • Definitions
  • Convergence Criteria
• More on Sequences and Series
  • Sequences
    • Definitions
    • Basic Properties
    • Algebraic Properties
    • Miscellaneous
  • Series
  • Algebraic Operations
    • Convergence Criteria
    • Translation
• Composition
  • Maps into Compacts
  • Continuity
  • Derivative
  • Differentiability
  • Generalizations
• Partitions
  • Definitions
  • Constructions
  • Properties of the mesh
  • Miscellaneous
  • Separation
• Calculus Theorems
• Lemmas for Integration
  • Merging orders
  • Summations
• IVT for Partial Functions
  • First Lemmas
  • The IVT
  • Strong IVT for partial functions
  • Other formulations
• The Refinement Lemmas
• Integral
• The generalized integral
  • Definitions
  • Properties of the Integral
• The Fundamental Theorem of Calculus
  • Indefinite Integrals
  • The FTC
  • Corollaries
  • Integration by substitution
• More on Power Series
  • General results
  • Function definitions through power series
• Taylor Series
  • Definitions
  • Convergence
• Exponential and Logarithmic Functions
  • Properties of Exponential
  • Properties of Logarithm
• Arbitrary Real Powers
  • Powers of Real Numbers
  • Power Function
• The Trigonometric Functions
  • Basic properties
  • Definition of Pi
  • Properties of Pi
  • More formulas
  • Derivative of Tangent
  • The Complex Exponential
• Inverse Trigonometric Functions
  • Definitions
    • Arcsine
    • Arccosine
    • Arctangent
  • Composition properties
    • Sine and Arcsine
    • Cosine and Arcosine
    • Tangent and Arctangent
  • ArcTan Series
• Inverse Hyperbolic Tangent Function
• Coq Real Numbers
  • Coq real numbers form a setoid
  • Coq real numbers form a semigroup
  • Coq real numbers form a monoid
  • Coq real numbers form a group
  • Coq real numbers form an abelian group
  • Coq real numbers form a ring
  • Coq real numbers form a field
  • Coq real numbers form an ordered field
  • Coq real numbers form a real number structure
• Coq Real Numbers and IR isomorphisms
  • The isomorphism
• Metric Spaces (traditional)
  • Relations necessary for Pseudo Metric Spaces and Metric Spaces
  • Definition of Pseudo Metric Space
  • Pseudo Metric Space axioms
  • Pseudo Metric Space basics
  • Zero function
  • Continuous functions, uniformly continuous functions and Lipschitz functions
  • Identity
  • Constant functions
  • Composition
  • Limit
  • Real numbers
  • Addition of continuous functions
  • Equivalent Pseudo Metric Spaces
  • Product-Pseudo-Metric-Spaces
  • Sub-Pseudo-Metric-Spaces
  • Definition of Metric Space
  • Metric Space basics
  • Product-Metric-Spaces and Sub-Metric-Spaces
  • Pseudo Metric Spaces vs Metric Spaces
  • Limit
  • Lists
  • Pseudo Metric Space theory
• Metric Space
  • Classification of metric spaces
  • Uniform Continuity
    • The metric space of uniformly continuous functions
    • The category of metric spaces.
  • Complete metric space
    • Regular functions
    • Cunit
    • Cjoin
    • Cmap (slow)
    • Strong Monad
    • Completion and Classification
  • Prelength space
    • A more effictient Cmap and Cbind
  • Product Metric
    • Completion of product spaces.
  • Limits
  • Example of a Metric: <Q, Qball>
• Hausdorff Metric
  • Strong Hausdorff Metric
• Finite Enumerations
  • Equivalence
  • Metric Space
  • Strong Hausdroff Metric
• Compact sets
  • Bishop Compactness
  • Definition of Compact
  • Compact is Bishop Compact.
  • Bishop Compact is Compact.
  • Isomorphism
  • FinEnum distributes over Complete
  • Compact Image
• Graphing
  • Graph and Bind
• Complete Metric Space: Computable Reals (CR)
  • Compression
  • Addition
  • Negation
  • Subtraction
  • Inequality
  • Maximum
  • Minimum
  • Example of a Partial Order: <CR, le>
  • Example of a Lattice: <CR, CRle, CRmin, CRmax>
  • Strict Inequality
  • Apartness
  • Multiplication
  • Inverse
  • Isomorphism between CR and Cauchy_IR
    • CR to Cauchy_IR
    • Cauchy_IR to CR
    • Functions preserved by isomorphism.
  • Example of a setoid: CR
    • CR
  • Examples of semi-groups: ⟨CR,+⟩
    • ⟨CR,+⟩
  • Examples of monoids: ⟨CR,+⟩
    • ⟨CR,+⟩
  • Example of a group: ⟨CR,+⟩
  • Example of a abelian group: ⟨CR,+⟩
  • Example of a ring: ⟨CR,+,*⟩
  • Example of a field: ⟨CR,+,*⟩
  • Example of a real number structure: ⟨CR⟩
  • Ring
  • Isomorphism between CR and IR
  • Absolute Value
  • Tactics for Inequalities
  • Computing Alternating Series.
    • Decreasing and Nonnegative
  • Geometric Series
  • Operations on Sequences
    • everyOther
    • mult_Streams
    • StreamBounds
    • powers
    • positives
    • recip_positives
    • factorials
    • recip_factorials
  • Correctness of continuous functions.
  • Modulus of continity and derivatives.
  • Positive Integer Powers
  • Multivariable polynomails
  • Exponential
    • e
  • Square Root
  • Arctangent (small)
  • Pi (alternate)
  • Pi
  • Arctangent
  • Sine
  • Cosine
  • Area Tangens Hyperbolicus (artanh)
  • Logarithm
• OpenUnit
  • • Equality
• Step Functions
  • Step Functions over setoids
  • Equivalence
  • Common subdivision view
  • Applicative Functor
  • Monad
  • A Partial Order on Step Functions.
  • L1 metric for Step Functions
    • Integeral for Step Functions.
    • Example of a Metric Space <StepQ, L1Ball>
  • Linf metric for Step Functions
    • Example of a Metric Space <Step, StepFSupBall>
    • Sup for Step Functions on Q.
  • Example of a Complete Metric Space: BoundedFunction
  • Example of a Complete Metric Space: IntegrableFunction
  • Completion distributes over Step Functions
• Effective Integration
  • stepSample
  • StepFunctions distribute over Completion
  • Riemann-Stieltjes Integral
• Intervals as a Compact Set.
• Rasters
  • Rasters on Planes
  • Rasterization
• Plotting

---

This page has been generated by coqdoc