Skip to content

weakmemory/hahn

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Hahn : A Coq library for lists and relations

Hahn is a Coq library that contains a useful collection of lemmas and tactics about lists and binary relations.

  • Hahn.v : exports all other files except HahnExtraNotation.v
  • HahnAcyclic.v : proving acyclicity of relations
  • HahnBase.v : basic tactics used throughout the development
  • HahnCountable.v : countable sets
  • HahnDom.v : (co)domain of a relation
  • HahnEquational.v : relational equivalences
  • HahnExtraNotation.v : notation for decidable equality.
  • HahnFun.v : functional update
  • HahnFuneq.v : functional preservation properties of relations
  • HahnLift.v : lifting relations to partial equivalence relations
  • HahnList.v : lemmas about lists
  • HahnListBefore.v : list-induced ordering
  • HahnMaxElt.v : maximal elements of a relation
  • HahnMinElt.v : minimum elements of a relation
  • HahnNatExtra.v : a few properties of natural numbers
  • HahnWf.v : well-founded and finitely supported relations
  • HahnMinPath.v : minimal paths/cycles over relations
  • HahnOmega.v : natural numbers with infinity
  • HahnPath.v : paths over relations
  • HahnRelationsBasic.v : binary relations
  • HahnRewrite.v : support for rewriting equivalent relations
  • HahnSets.v : lemmas about sets (i.e., unary relations)
  • HahnSegment.v : lemmas about segments of total orders
  • HahnSorted.v : lemmas about sortedness of lists
  • HahnTotalExt.v : extension of a partial order to a total order.
  • HahnTotalList.v : building finite relations for program order.
  • HahnTrace.v : possibly infinite sequences.
  • Zorn.v : A mechanization of Zorn's lemma (thanks to Johannes Kloos)

Build

  • Install Coq 8.15
  • make

Use

  • In a Coq file, write "Require Import Hahn".
  • Optionally, also "Require Import HahnExtraNotation".

Packages

No packages published

Languages

  • Coq 99.3%
  • Other 0.7%