Canonical

Canonical exhaustively searches for terms in dependent type theory. The canonical tactic proves theorems, synthesizes programs, and constructs objects in Lean.

Canonical.mp4

Installation

Canonical is available for Lean v4.20.0-rc3.

Add the following dependency to your lakefile.toml:

[[require]]
name = "Canonical"
scope = "chasenorman"

Or, if you are using a lakefile.lean:

require "chasenorman" / "Canonical"

You should then be prompted to run lake update Canonical.

Usage

Basic examples:

import Canonical

-- prove properties by induction
def add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := 
  by canonical

-- enumerate over elements of a type
example : List Nat := by canonical (count := 10)

-- supply premises
def Set (X : Type) := X → Prop
axiom P_ne_not_P : P ≠ ¬ P
theorem Cantor (f : X → Set X) : ¬ ∀ y, ∃ x, f x = y :=
  by canonical [P_ne_not_P, congrFun]

More examples can be found in the Canonical repository.