equational-reasoning

Proof assistant for Haskell using DataKinds & PolyKinds

LTS Haskell 22.23:0.7.0.3@rev:1
Stackage Nightly 2024-05-30:0.7.0.3@rev:1
Latest on Hackage:0.7.0.3@rev:1

See all snapshots equational-reasoning appears in

BSD-3-Clause licensed by Hiromi ISHII
Maintained by konn.jinro_at_gmail.com
This version can be pinned in stack with:equational-reasoning-0.7.0.3@sha256:fe66bd6c1a1083ceebedac5f355b41de4a2472072079f17f244a47de87a903ee,1215

Agda-style Equational Reasoning in Haskell by Data Kinds

Build Status Hackage

What is this?

This library provides means to prove equations in Haskell. You can prove equations in Agda’s EqReasoning like style.

See blow for an example:

plusZeroL :: SNat m -> Zero :+: m :=: m
plusZeroL SZero = Refl
plusZeroL (SSucc m) =
  start (SZero %+ (SSucc m))
    === SSucc (SZero %+ m)    `because`   plusSuccR SZero m
    === SSucc m               `because`   succCongEq (plusZeroL m)

It also provides some utility functions to use an induction.

For more detail, please read source codes!

TODOs

  • Automatic generation for induction schema for any inductive types.

Changes

Changelog

0.7.0.2

  • Supports GHC 9.8
  • Drops support for GHC <9

0.6.0.3

  • Support for GHC >= 8.10

0.6.0.2

  • Adds support for th-desugar-1.11

0.6.0.1

  • Supports GHC 8.8.
  • Adds support for th-desugar-1.10 (Thanks: Justin Le @mstksg)