Canonical exhaustively searches for terms in dependent type theory. The canonical tactic proves theorems, synthesizes programs, and constructs objects in Lean.
Canonical.mp4
Canonical is available for Lean v4.19.0.
Add the following dependency to your lakefile.toml:
[[require]]
name = "Canonical"
git = "https://github.com/chasenorman/CanonicalLean"
Or, if you are using a lakefile.lean:
require Canonical from git
"https://github.com/chasenorman/CanonicalLean.git"
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.