Library hydras.OrdinalNotations.ON_Omega

Library hydras.OrdinalNotations.ON_Generic

• • Relative correctness of a constant or a function

Library hydras.OrdinalNotations.ON_Finite

Library hydras.OrdinalNotations.ON_mult

• Definitions
• Properties

Library hydras.OrdinalNotations.ON_Omega_plus_omega

Library hydras.OrdinalNotations.ON_plus

Library hydras.OrdinalNotations.ON_O

Library hydras.OrdinalNotations.ON_Omega2

• • Additive principal ordinals

Library hydras.OrdinalNotations.Example_3PlusOmega

Library hydras.OrdinalNotations.OmegaOmega

• An implementation of ω^ω
• Representation by lists of pairs of integers
• well formed ordinal representation

Library hydras.Prelude.ssrnat_extracts

• Notations adapted from Mathcomp's ssrnat

Library hydras.Prelude.MoreDecidable

Library hydras.Prelude.STDPP_compat

Library hydras.Prelude.Comparable

Library hydras.Prelude.First_toggle

Library hydras.Prelude.Simple_LexProd

Library hydras.Prelude.DecPreOrder

Library hydras.Prelude.Exp2

Library hydras.Prelude.Sort_spec

Library hydras.Prelude.Merge_Sort

Library hydras.Prelude.WfVariant

Library hydras.Prelude.More_Arith

Library hydras.Prelude.DecPreOrder_Instances

Library hydras.Prelude.Fuel

Library hydras.Prelude.Iterates

• • Abstract properties of arithmetic functions
  • Abstract properties of iterate
  • Second-order iterate
  • Exponential and hyper exponential of base 2

Library hydras.Prelude.OrdNotations

Library hydras.Prelude.MoreLists

• Sets of natural numbers as lists
  • Definitions
  • Lemmas

Library hydras.Prelude.Restriction

Library hydras.Prelude.MoreOrders

Library hydras.Prelude.MoreVectors

• Maximum of a vector of nat

Library hydras.Prelude.Compat815

Library hydras.Prelude.MoreLibHyps

Library hydras.Prelude.LibHyps_Experiments

Library hydras.Epsilon0.Hessenberg

• Hessenberg sum of ordinals terms (commutative and strictly monotonous)

Library hydras.Epsilon0.Large_Sets

• • minimal large sequences
  • Last step of a minimal path
  • Paths starting with a finite ordinal (fin n)
  • Properties of m-largeness and L-functions
  • About the length of mlarge intervals
  • Properties of L_spec
  • Finite ordinals
  • omega × omega
    • Closed formula
• Plain large sequences (not necessarily minimal)
  • large sequences (as in KS ) (may contain zeros)

Library hydras.Epsilon0.Epsilon0rpo

• Module Type Variables.

Library hydras.Epsilon0.Hprime

• A hierarchy of rapidly growing functions
  • A variant of the Hardy Wainer hierarchy
  • Monotony of H' w.r.t. its first argument

Library hydras.Epsilon0.E0

• • Lifting functions from T1 to E0
  • Lemmas
  • On equality on type E0
  • Adaptation to E0 of lemmas about T1
  • Rewriting lemmas

Library hydras.Epsilon0.T1

• Definitions
  • A type of terms (not necessarily in normal form)
  • A linear strict order on T1
  • Properties of compare
  • Properties of Eq
  • Properties of lt
  • Properties of lt inv
  • The predicate "to be in normal form"
  • Arithmetic functions
    • Successor
    • Predecessor (partial function
    • Addition
    • multiplication
    • Substraction (used as a helper for exponentiation)
    • exponentiation functions
• Lemmas
  • Successors, limits and zero
  • Second part on lt and le
  • Properties of compare: second part
  • Properties of max
  • Restriction of lt and le to terms in normal form
  • Well foundedness of LT
    • Strong accessibility (inspired by Tait's proof)
    • A (last) structural induction
  • Properties of successor
  • properties of addition
  • plus and LT
  • On additive principal ordinals
  • monotonicity of succ
  • monotonicity of phi0
  • Multiplication
  • About minus
  • Exponential
  • Relations between cons, phi0 and +
  • An abstract syntax for ordinals in Cantor normal form
• Examples

Library hydras.Epsilon0.Paths

• • relations associated with canonical sequences
  • Paths inside epsilon_0
  • Accessibility (without traces)
  • following a path
  • Paths with constant index
  • standard paths
  • Bridge Lemmas
  • Composition/decomposition of paths
  • Properties of gnaw
  • Properties of acc_from
  • Paths with constant index: lemmas
• Adaptation to E0

Library hydras.Epsilon0.Canon

• Definitions
• Properties of canonical sequences
  • Canonical sequences and the order LT
  • Canonical sequences of limit ordinals
  • Adaptation to E0 (well formed terms of type T1 )

Library hydras.Epsilon0.Large_Sets_Examples

Library hydras.Epsilon0.L_alpha

• Computing the length of paths from alpha to zero

Library hydras.Epsilon0.Epsilon0

Library hydras.Epsilon0.F_alpha

• The Wainer hierarchy of rapidly growing functions (variant)
  • Definition, using coq-equations
  • We get the "usual" equations for F_
    • Relations between F_star and F_
    • Usual equations for F_
  • First steps of the hierarchy
• Comparison with the Hardy hierarchy
• A variant (Lob-Wainer hierarchy)
  • We get the "usual" equations for F_
    • Relations between F_star and F_
    • Usual equations for f_

Library hydras.Epsilon0.F_omega

• • Rewriting lemmas
  • Comparison between Ack n and F_ n
  • F_ omega is not primitive recursive
  • F_ alpha is not primitive recursive, for omega ≤ alpha
  • On the other hand, F_ n is PR for any n:nat

Library hydras.Gamma0.T2

• Definitions
  • • Examples
  • Length (as in Schutte)

Library hydras.Gamma0.Gamma0

• A notation system for ordinals less than Gamma0
  • terms in normal form
• Well-foundedness (with rpo) (Evelyne Contejean)
  • Module Type Variables.
  • Every (representation of a) natural number is less than
  • inclusion of the order lt in the rpo
• the Veblen function phi
  • Temporary compatibility nf/nfb

Library hydras.rpo.decidable_set

Library hydras.rpo.dickson

• Dickson Lemma: the multiset extension of a well-founded ordering is well-founded.
  • Definition of the multiset extension of a relation.
    • Accessibility lemmata.

Library hydras.rpo.list_set

• Sets built with lists
  • Definition of sets using lists.

Library hydras.rpo.list_permut

• Permutation over lists, and finite multisets.
  • Definition of permutation over lists.
  • Permutation is a equivalence relation.
  • Compatibility Properties.
  • Permutation for short lists.
  • Link with AC syntactic decomposition.

Library hydras.rpo.more_list

• Some additional properties for the Coq lists.
  • Relations between length, map, append, In and nth.
  • A measure on lists based on a measure on elements.
  • Induction principles for list.
  • How to remove an element in a list, whenever it is present.
  • Iterators.
  • more properties on the nth element.
  • Association lists.
    • find.
    • number of occurences of the first element of a pair.

Library hydras.rpo.closure

Library hydras.rpo.rpo

• • Module Type Precedence,
  • Definition of a precedence.
  • Module Type RPO,
  • Definition of RPO from a precedence on symbols.
  • Definition of rpo.
  • rpo is a preorder, and its reflexive closure is an ordering.
  • Main theorem: when the precedence is well-founded, so is the rpo.
  • RPO is compatible with the instanciation by a substitution.
  • RPO is compatible with adding context.
  • Definition of size-based well-founded orderings for induction.
  • Definition of rpo.
  • rpo is a preorder, and its reflexive closure is an ordering.
  • Well-foundedness of rpo.
  • Main theorem: when the precedence is well-founded, so is the rpo.
  • RPO is compatible with the instanciation by a substitution.
  • RPO is compatible with adding context.

Library hydras.rpo.term

• Term algebra defined as functor from a Module Signature and a Module Variable.
• Module Type Signature.
• Module Type Variables.
• Module Type Term built from a signature and a set of variables.
  • Recursion on terms.
  • Double recursion on terms.
  • Equality on terms is decidable.
  • Well-formedness of terms, according to the arity.
  • Substitutions.
  • Positions in a term.
• A functor building a Term Module from a Signature and a set of Variables.
  • Recursion on terms.
  • Double recursion on terms.
  • Equality on terms is decidable.
  • Well-formedness of terms, according to the arity.
  • Substitutions.
  • Positions in a term.

Library hydras.Schutte.MoreEpsilonIota

Library hydras.Schutte.CNF

• • • Every countable ordinal has (at least) a Cantor normal form
    • Unicity of cnf
    • The main result
  • Cantor Normal Form and the ordinal epsilon0

Library hydras.Schutte.AP

• Additive principal ordinals
  • Main Definitions
    • Additive principal ordinals
    • Exponential of basis omega
    • Omega-towers
    • The limit ordinal epsilon0
  • Proofs, proofs, proofs ...
  • About additive principals
  • Properties of phi0
  • Properties of epsilon0

Library hydras.Schutte.Schutte_basics

• Definitions
• The three axioms by Schutte
• First definitions
  • Limits
• Basic properties
  • Properties of le and lt
  • Global properties
  • About zero
  • Properties of successor
  • Building limits
  • Sequences of ordinals
  • Properties of omega
  • About zero, is_succ and is_limit
  • About members
  • Extensional equalities on sets of ordinals

Library hydras.Schutte.Ordering_Functions

• • Main definitions
  • Properties of segments

Library hydras.Schutte.Countable

Library hydras.Schutte.Critical

Library hydras.Schutte.Schutte

• Warning
  • Schutte's Axioms
  • Classical logic and Hilbert style
    • From Coq.Logic.Classical
    • From Coq.Logic.Epsilon
    • Needed for epsilon to work properly.

Library hydras.Schutte.Well_Orders

Library hydras.Schutte.Addition

• Definitions
  • addition, multiplication by a positive integer
• Proofs, proofs, proofs
  • Basic properties of addition

Library hydras.Schutte.Correctness_E0

Library hydras.Schutte.PartialFun

• Partial functions
  • Transformation of a functional relation into a function

Library hydras.Schutte.Lub

Library hydras.Schutte.GRelations

Library hydras.Hydra.Battle_length

Library hydras.Hydra.Omega_Small

Library hydras.Hydra.BigBattle

• A long hydra battle

Library hydras.Hydra.Epsilon0_Needed_Generic

Library hydras.Hydra.Hydra_Extraction

Library hydras.Hydra.KP_example

Library hydras.Hydra.Hydra_Termination

• • Proof of termination of all hydra battles
    • Converting any hydra into an ordinal less than
  • Monotonicity lemmas for S0, R1, etc .

Library hydras.Hydra.Hydra_Theorems

• • Liveness
  • Termination of free battles
  • Impossibility theorems
  • Battle length is not PR

Library hydras.Hydra.Omega2_Small

• • • Proof of the inequality m small_h o< m big_h
    • Proof of the inequality m big_h o≤ m small_h
    • Let us decompose any inequality p o< q into elementary steps

Library hydras.Hydra.Hydra_Definitions

• Data types
  • • height (length of longest branch)
  • Abbreviations
    • Heads : A head is just a node without daughters
    • Hydra with 0, 1, 2 or 3 daughters
    • Adds n copies of the same hydra h at the right of s
    • Hydra with n equal daughters
  • Managing sequences of hydras
    • Appending
    • Adds a head to the right of s
    • Adds i heads to the right of s
    • adds i heads to the root of h (to the right of its daughters)
• Hydra Battles
  • Relation associated with a single round.
    • S0
    • R1
    • S1
    • R2
    • round_n
    • Binary relation associated with a battle round
    • transitive closures of round
  • Experimental tactics for interactive battles
    • removes the i-th daughter (should be a head)
  • Traces
  • Classes of battles
    • Uniform termination
    • Variants for proving termination
  • Strictly Bounded variants
    • Liveness

Library hydras.Hydra.Epsilon0_Needed_Free

• • Bounded variants
  • Proof of the inequality m small_h t1< m big_h

Library hydras.Hydra.Hydra_Examples

Library hydras.Hydra.Hydra_Lemmas

• • Properties of the hydra data type
  • Properties of single rounds
  • Properties of battle
  • Properties of standard and free battle classes
  • Generic properties of round_plus

Library hydras.Hydra.O2H

Library hydras.Hydra.Epsilon0_Needed_Std

• • Proof of the inequality m small_h t1< m big_h

Library hydras.Ackermann.codeNatToTerm

Library hydras.Ackermann.code

• Encoding terms, formulas and proofs

Library hydras.Ackermann.extEqualNat

Library hydras.Ackermann.folLogic

Library hydras.Ackermann.fol

• First Order Formulas over a language
  • Extensions of the basic language of formulas
  • Decidability of equality between terms, formulas, ...
• Depth Induction
• Implicit arguments and notations
  • Implicit arguments
  • The fol_scope notation scope
  • Examples

Library hydras.Ackermann.LNN

• Instantiations of a few generic constructs
• Notations (Experimental and unstable)
• Basic and derived properties

Library hydras.Ackermann.NN2PA

Library hydras.Ackermann.PAtheory

Library hydras.Ackermann.prLogic

Library hydras.Ackermann.wellFormed

Library hydras.Ackermann.checkPrf

Library hydras.Ackermann.codePA

Library hydras.Ackermann.cPair

• Bijection from nat × nat to nat
  • Preliminary definitions
  • Definition and properties of cPair
  • Triples

Library hydras.Ackermann.folProof

Library hydras.Ackermann.Languages

• Language of Number Theory: LNT
• Language of Natural Numbers: LNN
• Goedel encoding for LNT
• Goedel encoding for LNN

Library hydras.Ackermann.LNT

• Instantiations of a few generic constructs
• Notations for LNT formulas: experimental and unstable
  • Notations for printing computed formulas/terms with derived connectives
  • Examples
• Basic properties
  • List of free variables of a formula
  • Basic and derived proof rules

Library hydras.Ackermann.NNtheory

Library hydras.Ackermann.PA

Library hydras.Ackermann.subAll

Library hydras.Ackermann.codeFreeVar

Library hydras.Ackermann.codeSubFormula

Library hydras.Ackermann.Deduction

Library hydras.Ackermann.folLogic2

Library hydras.Ackermann.folProp

Library hydras.Ackermann.ListExt

Library hydras.Ackermann.misc

Library hydras.Ackermann.NN

• Axioms of NN
• Properties of the system NN
  • Generic instantiation of axioms

Library hydras.Ackermann.subProp

Library hydras.Ackermann.codeList

Library hydras.Ackermann.codeSubTerm

Library hydras.Ackermann.expressible

Library hydras.Ackermann.folLogic3

Library hydras.Ackermann.folReplace

Library hydras.Ackermann.LNN2LNT

• Translation of terms
  • Inverse translation
• Translation of formulas
  • Translation of (v#0 < v#1)%fol
  • Translation of (t < t')%fol
  • Translation of any LNN-formula
    • Helpful rewriting lemmas
  • Inverse translation
    • Commutation lemmas
• Proof translation

Library hydras.Ackermann.model

Library hydras.Ackermann.PAconsistent

Library hydras.Ackermann.primRec

• Definitions
  • Semantics
    • Constants
    • Projections
    • Function composition
    • Primitive recursion
  • Predicates "to be primitive recursive"
  • Usual projections (in curried form) are primitive recursive
  • Composition lemmas

Library hydras.Ackermann.wConsistent

Library hydras.Ackermann.NewNotations

Library hydras.MoreAck.Ack

• • • Exercise
    • Usual equations
    • First values
    • monotony properties
  • Bounding nested calls of Ack
  • Ack is (partially) strictly monotonous in its first argument

Library hydras.MoreAck.AckNotPR

• Proof that Ack is not primitive recursive
  • Comparing an n-ary and a binary functions
  • Every primitive recursive function is majorized by Ack
    • Base cases
    • The general case is proved by induction on x
    • Now, let us assume that Ack is PR
    • Any function which dominates (diagonalized) Ack fails to be PR
  • Nevertheless, for any n, Ack n is primitive recursive.

Library hydras.MoreAck.FolExamples

• • Preliminary lemmas
  • Universal quantifier

Library hydras.MoreAck.Iterate_compat

Library hydras.MoreAck.PrimRecExamples

• • Examples of terms of type PrimRec n and their interpretation
  • Understanding some constructions ...
• First proofs of isPR statements

Library hydras.MoreAck.LNN_Examples

Library hydras.MoreAck.BadSubst

• • Preliminary lemmas

Library hydras.MoreAck.expressibleExamples

Library hydras.solutions_exercises.MinPR

Library hydras.solutions_exercises.MinPR2

Library hydras.solutions_exercises.FibonacciPR

Library hydras.solutions_exercises.MorePRExamples

• • Solution to an exercise

Library hydras.solutions_exercises.isqrt

Library hydras.solutions_exercises.T1_ltNotWf

Library hydras.solutions_exercises.predSuccUnicity

Library hydras.solutions_exercises.lt_succ_le

Library hydras.solutions_exercises.Limit_Infinity

Library hydras.solutions_exercises.ge_omega_iff

Library hydras.solutions_exercises.schutte_cnf_counter_example

Library hydras.solutions_exercises.F_3

• Proof that F_alpha (S n) > exp2 (F alpha n) for alpha >= 3 and
  • Base case
  • Limit case

Library hydras.solutions_exercises.is_F_monotonous

Library hydras.solutions_exercises.MultisetWf

Library hydras.solutions_exercises.OnCodeList

Library additions.AM

• Euclidean chain generation

Library additions.Addition_Chains

• Addition Chains
  • Computations composed of multiplications over type A
    • Monadic Notation for computations
    • Definition
    • Our Favorite example
    • Chain length (number of mutiplications)
    • Execution of chains
  • Chain correctness
• Correctness Proof by Reflection
• Correctness and parametricity
  • computation of compared to computation of
  • Correctness Theorem
    • Remark
    • Back to 87
  • Correct by construction chains
    • Definition
  • Some chain generators
  • Chains associated to the well-known binary exponentiation algorithm
    • computation of
  • Correctness of the binary method
  • The binary method is not optimal
• How to prove chain correctness in general ?

Library additions.BinaryStrat

Library additions.Compatibility

• Compatibility with StdLib exponentiation functions
  • really logarithmic versions of N.pow, Pos.pow and Z.pow
  • Equivalence between StdLib definitions and ours
  • Tests
    • Adapting lemmas from Standard Library

Library additions.Demo

Library additions.Demo_power

Library additions.Dichotomy

Library additions.Euclidean_Chains

• Euclidean chains
  • Introduction
• CPS chain construction
  • Remark
  • More chain combinators
    • Automatic generation of correct euclidean chains
  • Full correctness

Library additions.fib

Library additions.Fib2

Library additions.FirstSteps

• • Examples
• A wrong definition of correctness

Library additions.Monoid_def

• • The Monoid type class (with Operational Type Classes)
    • Exercice
    • Monoids and Equivalence Relations
    • Coercion from Monoid to EMonoid
    • Commutative Monoids

Library additions.Monoid_instances

• • Some useful instances of Monoid classes
    • Multiplicative monoid on Z
    • Multiplicative monoid on nat
    • Additive monoid on nat
    • Multiplicative monoid on 63-bits integers
    • Monoid of 2x2 matrices
    • Integers modulo m

Library additions.More_on_positive

• Basic lemmas about positive and N
  • Relationship with nat and N
  • Surjection from N into positive
  • Lemmas on Euclidean division

Library additions.Naive

• • Naïve and Monomorphic Functions for Computing Powers.
    • Exponentiation of integers
    • Some basic properties of Z.power
    • Exponentiation modulo m
    • Exponentiation of matrices

Library additions.Pow

• Exponentiation in a Monoid
  • Two functions for computing powers
    • The "naive" reference function
    • The binary exponentiation function (exponents in positive)
  • Properties of the power function
  • Correctness of the binary algorithm
  • Remark
  • Properties of Abelian Monoids

Library additions.Pow_variant

• Exponentiation in a Monoid
  • Two functions for computing powers
    • The "naive" reference function
    • The binary exponentiation function (exponents in positive)
  • Properties of the power function
  • Correctness of the binary algorithm
  • Remark
  • Properties of Abelian Monoids

Library additions.Strategies

Library additions.Trace_exercise

Library additions.Wf_transparent

Library gaia_hydras.T1Bridge

• Bridge between Hydra-battle's and Gaia's T1 (Experimental)
• refinement of constants, functions, etc.
  • Refinements of usual constants
  • unary functions and predicates
  • Equality and comparison
  • Ordinal addition
  • Ordinal multiplication
• Ordinal terms in normal form
• Well formed ordinals as a data type
• Make E0 an ordinal notation
• Abstract properties of arithmetic functions (with SSreflect inequalities)

Library gaia_hydras.GaiaToHydra

Library gaia_hydras.nfwfgaia

• Ordinals in Pure Coq
• prelude
  • Example 1
  • Example 2
  • Example 3
  • More on accessiblity
• The type T1
  • Equality
  • Order on T1
  • Normal form
  • Successor
  • Addition
  • Limits
    • Definition
    • The normal form
    • Realizing the limit
    • Normal functions
  • multiplication
    • Preparation of the exponention
    • Normality of multiplication
  • Exponentiation
    • Existence and uniqueness of the Cantor Normal Form
    • Basic Properties
• The type T2
  • Definition and Equality
  • Order
  • Normal form
  • Successor and predecessor
  • Addition
  • The function phi
• Ackermann
  • Comparison
  • Normal form
  • Successor Predecessor
  • Addition
  • limit
  • additive principal

Library gaia_hydras.GCanon

• Adaptation of canon to type E0

Library gaia_hydras.GF_alpha

• Rapidly growing functions

Library gaia_hydras.GL_alpha

Library gaia_hydras.GHprime

• • Equations for H'_
  • Examples

Library gaia_hydras.ON_gfinite

Library gaia_hydras.GPaths

• Adaptation to E0
• Examples

Library gaia_hydras.GLarge_Sets

Library gaia_hydras.GHessenberg

Library gaia_hydras.HydraGaia_Examples

Library gaia_hydras.GHydra

Library gaia_hydras.T2Bridge

• Bridge between Hydra-battle's and Gaia's T1 (Experimental)

Library gaia_hydras.GPrelude

Library gaia_hydras.T1Choice

Library gaia_hydras.onType

• Preliminaries
  • Complements on orderType
• First instances of ON
  • The Ordinal notation for 'I_i
  • An ordinal notation for omega

Library Goedel.rosser

Library Goedel.goedel1

Library Goedel.PRrepresentable

Library Goedel.fixPoint

Library Goedel.codeSysPrf

Library Goedel.rosserPA

Library Goedel.goedel2