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
• 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.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.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.Logic.ConstructiveLogic

Library Waterproof.Libs.Logic.InformativeEpsilon

Library Waterproof.Notations.Common

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

Library Waterproof.Notations.Reals

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

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.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.Since

Library Waterproof.Util.TypeCorrector