Library Waterproof.Automation

Library Waterproof.Chains

Library Waterproof.Notations

Library Waterproof.Tactics

Library Waterproof.Version

Library Waterproof.Waterproof

Library Waterproof.Waterprove

Library Waterproof.Automation.Hints

• Waterproof core
• Definitions
• Classical logic
• Logical negation
• Constructive logic
• Decidability based on classical epsilon
• Classical logic decidability
• Constructive decidability
• Natural numbers decidability
• Real numbers decidability
• Real numbers' addition and multiplication
• Opposite number
• Real numbers' minus
• Simplification with 0
• Simplification with 1
• Absolute value
• Square root
• Exponential and logarithm
• Integers
• Integer negation
• Natural number negation
• Real numbers
• Real number negation
• Sets
• Function image hints
• Function preimage hints
• Function preimage translation hints
• Left inverse hints
• Right inverse hints
• Inverse hints
• Intuition

Library Waterproof.Chains.Inequalities

• Abstract representations for =, <, ≤, > and ≥ symbols.
• Types of chains.
  • Only contains =- relations.
• Helper functions
  • Head: first term in a chain
  • Tail: last term in a chain
• the global statement of (0 < 1 <= 2) is (0 < 2),
• the weak global statement is (0 <= 2),
• the total statement is (0 < 1 /\ 1 <= 2)
  • Notations for link type classes
  • Full chain
  • Global & total statement - EqualChain
• Helper functions specific to Less- and GreaterChain.
  • The global relation resulting from a combination of relations rel1 and rel2.
  • Returns the global relation of a LessChain.
  • Returns the global relation of a GreaterChain.
  • Global & total statement - LessChain
  • Global & total statement - GreaterChain
  • Interpretations of LessRel and GreaterRel for the naturals.
  • Interpretations of LessRel and GreaterRel for the reals.
  • Embedding INR : nat -> R
    • EqualChain
    • LessChain
    • GreaterChain
  • Embedding IZR : Z -> R
    • EqualChain
    • LessChain
    • GreaterChain

Library Waterproof.Chains.Manipulation

Library Waterproof.Libs.Analysis

Library Waterproof.Libs.Functions

• Function Image
• Basic Properties
• Function Preimage
• Basic Properties for Preimage
• Injective Functions
• Basic Properties of Injective Functions
• Surjective Functions
• Basic Properties of Surjective Functions
• Bijective Functions
• Basic Properties of Bijective Functions
• Lemmas for Left Inverse
• Lemmas for Right Inverse
• Lemmas for Inverse

Library Waterproof.Libs.Integers

Library Waterproof.Libs.Logic

Library Waterproof.Libs.Negation

Library Waterproof.Libs.Reals

• Lemmas linking reals and booleans
• Lemmas regarding identities for absolute values and inverses
• Lemmas for decidability
  • Lemmas to write e.g. {r1 ≤ r2} + {r2 < r1}
  • Lemmas to split e.g. {r1 <= r2} into {r1 < r2} + {r1 = r2}

Library Waterproof.Libs.Sets

Library Waterproof.Libs.Analysis.ContinuityDomainNat

Library Waterproof.Libs.Analysis.ContinuityDomainR

Library Waterproof.Libs.Analysis.LimsupLiminfBolzano

Library Waterproof.Libs.Analysis.MetricSpaces

• • Example : a discrete metric on the real line

Library Waterproof.Libs.Analysis.OpenAndClosed

Library Waterproof.Libs.Analysis.Sequences

• • What is a sequence of real numbers?
    • Examples of sequences
  • Terminology about sequences
  • Asymptotic behavior of sequences
  • A simple limit
  • **Another simple limit**
  • The squeeze theorem
  • Order and limits

Library Waterproof.Libs.Analysis.SequencesMetric

• Sequences in metric spaces
• TODO change the naming in this file

Library Waterproof.Libs.Analysis.SequentialAccumulationPoints

Library Waterproof.Libs.Analysis.Series

Library Waterproof.Libs.Analysis.StrongInductionIndexSequence

Library Waterproof.Libs.Analysis.Subsequences

Library Waterproof.Libs.Analysis.SubsequencesMetric

Library Waterproof.Libs.Analysis.SupAndInf

• Lemmas for convenience

Library Waterproof.Libs.Integers.Divisibility

Library Waterproof.Libs.Integers.Even

Library Waterproof.Libs.Integers.Square

Library Waterproof.Libs.Logic.ConstructiveLogic

Library Waterproof.Libs.Logic.InformativeEpsilon

Library Waterproof.Libs.Logic.Quantification

Library Waterproof.Libs.Reals.ArchimedN

Library Waterproof.Libs.Reals.Integer

Library Waterproof.Libs.Reals.Intervals

Library Waterproof.Libs.Reals.Rational

Library Waterproof.Libs.Reals.RealInequalities

Library Waterproof.Libs.Sets.IndexedOperations

Library Waterproof.Libs.Sets.Operations

Library Waterproof.Notations.Common

• • Standard mathematical function notation.
  • Quantifiers
  • Set symbols, implications

Library Waterproof.Notations.Functions

• Notations for function images and preimages
• Function Composition

Library Waterproof.Notations.IndexedSets

Library Waterproof.Notations.Integers

Library Waterproof.Notations.Reals

• • (In)equalities
  • Scopes and coercions
  • Sequences
• Real numbers
  • Powers
  • Sums and series
  • Subsets and intervals

Library Waterproof.Notations.RealsWithSubsets

Library Waterproof.Notations.Sets

Library Waterproof.Tactics.Assume

Library Waterproof.Tactics.Because

Library Waterproof.Tactics.BothDirections

Library Waterproof.Tactics.BothStatements

Library Waterproof.Tactics.Choose

• Choose

Library Waterproof.Tactics.Claims

Library Waterproof.Tactics.Conclusion

Library Waterproof.Tactics.Contradiction

Library Waterproof.Tactics.Define

Library Waterproof.Tactics.Either

Library Waterproof.Tactics.Help

• Help tactic

Library Waterproof.Tactics.Induction

• induction_without_hypothesis_naming

Library Waterproof.Tactics.ItHolds

• It holds that ... (...)
• By magic it holds that ... (...)

Library Waterproof.Tactics.ItSuffices

Library Waterproof.Tactics.Obtain

Library Waterproof.Tactics.Specialize

Library Waterproof.Tactics.Take

Library Waterproof.Tactics.ToShow

Library Waterproof.Tactics.Unfold

Library Waterproof.Util.Assertions

• Waterproof test framework

Library Waterproof.Util.Binders

Library Waterproof.Util.BySince

Library Waterproof.Util.Constr

• • Auxiliary function to get a coerced type

Library Waterproof.Util.Evars

Library Waterproof.Util.Goals

Library Waterproof.Util.Hypothesis

• get_value_of_hyp_id

Library Waterproof.Util.Init

Library Waterproof.Util.MessagesToUser

Library Waterproof.Util.TypeCorrector