Canonical

Stream: general

[Chase Norman]

@Jared green We are planning to release Canonical this Spring!

[Ruben Van de Velde]

Spring in which hemisphere? :)

[Jason Rute]

@Chase Norman What is Canonical?

[Chase Norman]

@Jason Rute chasenorman.com It's an automated theorem prover for dependent type theory. If you recall, it was the big goal I was discussing at IPAM Machine Assisted Proofs.

[Jason Rute]

@Chase Norman will it eventually be a lean tactic (either native or through a hammer-like interface or through a plugin)? How does it compare to Duper in both scope and capabilities? What applications will it shine on? How does it handle many available premises or many applicable premises? Does it need a premise/lemma selector for real-world applications? It works by application, right? So does/will it use the Lean discrimination tree for the apply? tactic, or does it have it’s own data structures?

[Jason Rute]

Also @Victor Maia says his tool can be used for proof synthesis in Lean (or Kind, his theorem prover). So maybe it is a competitor to Duper or Canonical. https://x.com/victortaelin/status/1876579350382096745?s=46

[Chase Norman]

@Jason Rute Canonical will be a Lean tactic on Day 1, through a hammer-like interface. Canonical is a sound and complete proof search for dependent type theory, and generates terms--not tactic based proofs.

Canonical has no knowledge of theories like equality, natural numbers, or classical logic. It receives this information directly from Lean's internal representation. Canonical is made for higher-order reasoning where you intend to have a short proof term as a witness; think synthesizing motives for (generalized) induction or other axiom schema, working with user-written (indexed) inductive types, program synthesis by specification or examples, proof minimization, non-Prop types like isomorphisms and typeclasses, generating multiple witnesses of a given type, etc.

This is in contrast to Duper, which is strong at inhabiting Prop types for problems that translate into a first-order logic, and can handle large numbers of premises and well-understood theories like equality and LEM. Duper is intended to close goals where you don't really care what is generated. Canonical replaces itself with an exact proof term upon completion and does not stay in your code.

To facilitate millions of steps per second and a complete search procedure, Canonical has its own internal representation and outputs a complete term without interacting with Lean.

[Asei Inoue]

That sounds nice

[Jared green]

@Chase Norman can we get a more precise time frame for the availability of Canonical?

[Asei Inoue]

I have found suggest_premises tactic is added in Lean.
any related?

[Chase Norman]

@Jared green April

[Jared green]

@Chase Norman where your page says Canonical only generates canonical forms, how is that defined? how do you assure that?

[Mario Carneiro]

IIUC it normalizes things at parse time

[Chase Norman]

@Jared green @Mario Carneiro In general it does not require normalization at parse time. Canonical cannot place a lambda inside an application (by construction), cannot place a constructor in the major argument of a recursor/projection (hard-coded), and always places as many lambdas as is required to be eta-long (by construction, nontrivial). In this sense it only searches canonical forms. The internal representation of Canonical is BNEL, but can support beta unreduced forms using let definitions.

[Chase Norman]

You can choose which definitions Canonical can use, so canonicity with respect to delta reduction is at the user’s discretion.

[Jared green]

@Chase Norman can we get a more precise release time for Canonical?

[Chase Norman]

For those on this thread that have been waiting for quite some time, I want to inform you that Canonical is "released." The tactic, source code, arXiv paper, and demo videos are on my website https://chasenorman.com. I have spent much of the past month battling build and link issues, and these are still ongoing. I'm choosing not to make a big announcement on this Zulip and elsewhere yet, because:

1. precompileModules is broken on the latest version of MacOS.
2. lake build and VSCode builds expect dynlibs to be in different places.
3. I am struggling to get buildArchive to download from a github release, so I am not currently packaging dynlibs for Intel Macs or Linux on Arm.
4. The dynlibs feature intended to directly support the linking of dynamic libraries has not been released yet (coming with v4.19.0).
5. Users that attempt to reset their build by deleting the Canonical package directory will find that it is not compiled upon redownloading.
6. There are miscellaneous build issues even for some users meeting the system requirements, such as undefined symbol: lean_alloc_small on Ubuntu, missing symbols and ld64.lld: error: library not found for -lcanonical on MacOS.
7. Windows users require extra installation instructions to ensure that the canonical.dll is linked.

In short, I want to make sure that users have an easy time installing Canonical, and Lean's dynlib functionality is still being developed.

[Kim Morrison]

I also encountered a build issue, which seems to be different from those above:

info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading plugin, initializer not found 'initialize_canonical'
error: Lean exited with code 134

For me, this reproduces by checking out branch#canonical of Mathlib and typing lake build.

[Chase Norman]

@Kim Morrison I think on 4.19 they are revamping the “plugin” system. Perhaps trying this on 4.18 will avoid this particular error.

[Kim Morrison]

Thanks, I've rebased branch#canonical on the v4.18.0 tag of Mathlib, and now get the error:

info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(/Users/kim/projects/lean/mathlib4-4/.lake/packages/Canonical/.lake/build/lib/lean/Canonical.dylib, 0x0009): Library not loaded: @loader_path/libcanonical.dylib
  Referenced from: <4C4C4429-5555-3144-A1EB-2D39C1A645EE> /Users/kim/projects/lean/mathlib4-4/.lake/packages/Canonical/.lake/build/lib/lean/Canonical.dylib (built for macOS 99.0 which is newer than running OS)
  Reason: tried: '/Users/kim/projects/lean/mathlib4-4/.lake/packages/Canonical/.lake/build/lib/lean/libcanonical.dylib' (no such file)

[Chase Norman]

Is this on lake build or via VSCode?

[Chase Norman]

And I apologize for this. It really should be one-click; I hope it’s clear why I am waiting

[Kim Morrison]

Just lake build! Somehow in VSCode it seems to work!

Also, I get multiple

warning: Canonical: repository '././.lake/packages/Canonical' has local changes

warnings.

[Kim Morrison]

Chase Norman said:

And I apologize for this. It really should be one-click; I hope it’s clear why I am waiting

No worries -- I'm looking forward to getting to try it out, and I appreciate the effort to make things one-click for users.

[Kim Morrison]

I'm trying it out in VSCode a bit. Can I suggest that when you find a proof and show the info message, you also discharge the goal with sorry, so as to avoid a red squiggly (which nearly obscures the blue squiggly!)

[Kim Morrison]

Do you have other publicly available examples besides those from NNG? I'm having a bit of trouble finding interesting examples where it succeeds. So far my efforts have only got

example (x y : Nat × Nat) (h : x = y.swap) : y.swap = x := by canonical
example : { x : Nat × Nat // x.1^2 = x.2 + 1} := by canonical
example (x y : Nat) (h : x = y) : x^2 = y^2 := by canonical

(and even there, the proof terms for the 2nd and 3rd are unnecessarily large, but I guess that comes with the territory.)

I have a list of negative examples I could post if you're interested (here or elsewhere).

[Chase Norman]

Perhaps you would be interested in the Examples section of the Canonical for Automated Theorem Proving in Lean paper

[Chase Norman]

It can be difficult to tell whether there exists a short proof term for a statement or not, and I hope Canonical can be a useful tool to determine this. Since Canonical has no native support for natural numbers, the performance on the NNG is more indicative of reasoning about the foundations of any axiomatic system (indeed, you can replace all instances of Nat with a custom MyNat in the NNG and get the same results).

My next formalization project might be to formalize the properties of the type theory of Canonical. This will involve custom inductive types and foundational proofs by induction on them. I expect Canonical to do quite well there, just as in NNG.

[Wang Jingting]

I tried to run Canonical locally both in a new lake project and in the cloned version of that mathlib branch, but in both cases I met the error error loading library, libcanonical.so: cannot open shared object file: No such file or directory. (when using both VSCode and lake build) Is there some way I could deal with this?

The system information is as below (I don't really know what some of these entries mean, just copied them from system information, hopefully it's useful):

System:
  Kernel: 6.8.0-51-generic arch: x86_64 bits: 64 compiler: gcc v: 13.3.0 clocksource: tsc
  Desktop: Cinnamon v: 6.4.6 tk: GTK v: 3.24.41 wm: Muffin v: 6.4.1 vt: 7 dm: LightDM v: 1.30.0
    Distro: Linux Mint 22.1 Xia base: Ubuntu 24.04 noble
Machine:
  Type: Laptop System: LENOVO product: 21N5 v: ThinkBook 16p G5 IRX serial: <superuser required>
    Chassis: type: 10 v: ThinkBook 16p G5 IRX serial: <superuser required>
  Mobo: LENOVO model: LNVNB161216 v: SDK0T76479 WIN serial: <superuser required>
    part-nu: LENOVO_MT_21N5_BU_idea_FM_ThinkBook 16p G5 IRX uuid: <superuser required> UEFI: LENOVO
    v: P5CN26WW date: 09/03/2024
CPU:
  Info: 24-core (8-mt/16-st) model: Intel Core i9-14900HX bits: 64 type: MST AMCP smt: enabled
    arch: Raptor Lake rev: 1 cache: L1: 2.1 MiB L2: 32 MiB L3: 36 MiB
  Speed (MHz): avg: 1981 high: 5600 min/max: 800/5600:5800:4100 cores: 1: 1230 2: 2974 3: 3010
    4: 800 5: 5600 6: 800 7: 800 8: 800 9: 800 10: 800 11: 800 12: 800 13: 3628 14: 800 15: 4600
    16: 800 17: 4002 18: 800 19: 800 20: 800 21: 1542 22: 3371 23: 3572 24: 3232 25: 800 26: 1837
    27: 3088 28: 4102 29: 800 30: 800 31: 1745 32: 3065 bogomips: 154828
  Flags: avx avx2 ht lm nx pae sse sse2 sse3 sse4_1 sse4_2 ssse3 vmx

[Chase Norman]

I’ve tested on something similar with Ubuntu x86. I assume your .lake/packages/Canonical/.lake/build/lib folder has libcanonical.so, so it’s a linker issue.

[Wang Jingting]

Yes. The file is actually under the path you described.

[Wang Jingting]

So is there currently a way to fix this? (Or should I wait until the error is fixed properly?) Thanks!

[Chase Norman]

I feel that this would need further investigation to resolve; there’s not a clear fix

[Wang Jingting]

OK, Thanks for the reply! Then I'll just wait for a while and see if this error can be fixed. But anyway, I'm still looking forward to having a try!

[Niels Voss]

Out of curiosity, did you get this error from lake build or VSCode? According to https://github.com/chasenorman/CanonicalLean/issues/1, Canonical currently only works when built and run from VSCode, due to an issue with loader_path. This is a different error than what you are getting, so it's probably not the issue, but it's worth checking.

[Chase Norman]

(deleted)

[Chase Norman]

He says both (I take it with the same error). And @loader_path is a MacOS thing. Regardless, Canonical is meant to be used primarily through the VSCode plugin, so I tested with that in mind.

[Wang Jingting]

Niels Voss said:

Out of curiosity, did you get this error from lake build or VSCode? According to https://github.com/chasenorman/CanonicalLean/issues/1, Canonical currently only works when built and run from VSCode, due to an issue with loader_path. This is a different error than what you are getting, so it's probably not the issue, but it's worth checking.

Yeah, actually I tried both of these methods, and unfortunately, none worked. But anyway, I guess I'll just wait until a fix of that problem has been found. By the way, should I also submit a detailed description in an issue to that repository? @Chase Norman (Since you said you've met the same error, I wonder if submitting an issue is still necessary/recommended)

Edit: I also met the undefined symbol: lean_alloc_small error.

[Niels Voss]

He says both (I take it with the same error). And @loader_path is a MacOS thing. Regardless, Canonical is meant to be used primarily through the VSCode plugin, so I tested with that in mind.

It makes sense that you would focus on VSCode, though it's clearly not ideal that lake build always fails in a repository with canonical installed.

[Chase Norman]

@Wang Jingting that lean_alloc_small error is much better than the earlier one. I specifically checked that the linux-x86_64 build of Lean has lean_alloc_small in the libleanshared.so. It seems like this depends on the specific installation of Linux, but I still find it hard to imagine that Lean wouldn’t be linking this very necessary primitive.

[Chase Norman]

You can verify my work by running nm -D --defined-only ~/.elan/toolchains/leanprover--lean4---v4.18.0/lib/lean/libleanshared.so | grep lean_alloc_small

[Chase Norman]

I guess I could add a linker argument to force this library to be linked.

[Sebastian Ullrich]

This symbol vanished in 4.19.0 so might there be some Lean version confusion?

[Chase Norman]

Oh, what should I use instead?

[Sebastian Ullrich]

lean_alloc_small_object is the one Lean itself calls

[Sebastian Ullrich]

But if code compiled against 4.18 is run against 4.19, there must be some more fundamental issue

[Wang Jingting]

Chase Norman said:

Wang Jingting that lean_alloc_small error is much better than the earlier one. I specifically checked that the linux-x86_64 build of Lean has lean_alloc_small in the libleanshared.so. It seems like this depends on the specific installation of Linux, but I still find it hard to imagine that Lean wouldn’t be linking this very necessary primitive.

I remember that the first time the lean_alloc_small error didn't show up on my first attempt, but then I don't know why, but sometimes lake automatically update the lean-toolchain to v4.19.0-rc3 and this starts to appear. So maybe this isn't much to worry if it's only a version problem, I guess I can solve the version problem anyway.

[Chase Norman]

It is in fact a version problem

[Wang Jingting]

Thanks. I'll try to first fix this easier problem locally.

Edit: Hooray! I don't know exactly what is happening, but things start to work on my laptop now!

[Notification Bot]

49 messages were moved here from #general > Duper and Program Synthesis by Patrick Massot.

[Wang Jingting]

Kim Morrison said:

Do you have other publicly available examples besides those from NNG? I'm having a bit of trouble finding interesting examples where it succeeds. So far my efforts have only got

example (x y : Nat × Nat) (h : x = y.swap) : y.swap = x := by canonical
example : { x : Nat × Nat // x.1^2 = x.2 + 1} := by canonical
example (x y : Nat) (h : x = y) : x^2 = y^2 := by canonical

(and even there, the proof terms for the 2nd and 3rd are unnecessarily large, but I guess that comes with the territory.)

I have a list of negative examples I could post if you're interested (here or elsewhere).

It seems that the second and third example doesn't work on my computer? The first one returned a result, but the second and third one both returned no proof found, even after I raised the time limit to a larger number.

[Deming Xu]

I changed my lean-toolchain file to leanprover/lean4:v4.18.0 and canonical started to work, but then import Mathlib failed because of the version change. I don't know how to downgrade Mathlib to v4.18.0. Whenever I run lake update mathlib, lake always changes the toolchain file back to v4.19.0-rc3 for me...

I think the idea of proving things only from first principles of the language is really cool!

The fact that canonical can find the Cantor diagonal proof on its own is also cool.

I ran these tests:

import Canonical

example : 1 ≠ 2 := by
  -- canonical  -- Timeout. Here is my proof:
  intro h  -- 1 = 2. Goal: False
  let P (x : Nat) : Prop := match x with
    | 1 => True
    | _ => False
  have h1 : P 1 := True.intro
  rw [h] at h1  -- (h1 : P 2) after substitution. Now P 2 is False
  exact h1

example : ∃ x : Nat, x * x = 0 := by
  -- exact Exists.intro 0 (Eq.refl 0)
  -- canonical 10  -- It finds this proof:
  exact
    Exists.intro Nat.zero
      (Eq.rec (motive := fun a t ↦ a = Nat.zero) (Eq.refl Nat.zero)
        (Nat.rec (motive := fun t ↦ t = t) (Eq.refl Nat.zero) (fun n n_ih ↦ Eq.refl n.succ)
          (Nat.zero.mul Nat.zero)))

example : ∃ x : Nat, x * x = 1 := by
  -- exact Exists.intro 1 (Eq.refl 1)
  -- canonical 10  -- It finds this proof:
  exact
    Exists.intro Nat.zero.succ
      (Eq.rec (motive := fun a t ↦ a) (Eq.refl Nat.zero.succ)
        (Eq.rec (motive := fun a t ↦ (a = a) = (a.mul a = a))
          (Eq.refl (Nat.zero.succ = Nat.zero.succ))
          (Nat.rec (motive := fun t ↦ Nat.zero.succ = Nat.zero.succ) (Eq.refl Nat.zero.succ)
            (fun n n_ih ↦ n_ih) (Nat.zero.mul Nat.zero))))

example : ∃ x : Nat, x * x = 4 := by
  -- canonical 10  -- Timeout. Here is my proof:
  exact Exists.intro 2 (Eq.refl 4)

canonical failed to prove 1 ≠ 2, but I think this is reansonable because the actual mechanism in Lean is pretty complicated.

It succeeded in proving ∃ x, x * x = 0 and ∃ x, x * x = 1, but the proof seems to have some redundant parts. Running Eq.rec to do substitution is not necessary here. We only need Eq.refl to prove 0*0=0 and 1*1=1. The whole Eq.rec block from canonical has type 0*0=0, 1*1=1, so they should be replaced with refl. canonical failed on ∃ x, x * x = 4.

I also tried import Mathlib.Tactic and replacing canonical with aesop. Aesop also failed the ∃ x, x * x = 4 test and succeeded in proving ∃ x, x * x = 0 and ∃ x, x * x = 1, so I think canonical achieved similar performance to aesop with less domain-specific knowledge.

Maybe manually optimizing for Eq in canonical will make the search faster. For example when a new search node requires a proof of a = b, always try Eq.refl by definitional equality first.

[Kevin Buzzard]

@Deming Xu it's possible to say which version of mathlib you want in the config file of your project. Do you have a lakefile.lean or a lakefile.toml?

[Kevin Buzzard]

Once you change that file, lake update mathlib will "update" mathlib to the commit or branch or tag specified in the config file.

[Sebastian Ullrich]

(It would be great to document these dependency pinning instructions at https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency)

[Yaël Dillies]

Yes sorry I told Johan I would update those instructions two weeks ago, but it slipped off the radar :sweat:

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Deming Xu said:

Maybe manually optimizing for Eq in canonical will make the search faster. For example when a new search node requires a proof of a = b, always try Eq.refl by definitional equality first.

This could be reasonable in some contexts, but in others an equality may be provable by a 'heavy rfl' which you do not want to use because it will take the kernel ages to compute through it. A slider which tells a proof search procedure how 'heavy' of a rfl is considered acceptable seems like the most flexible control for this.

[Deming Xu]

It worked. Thank you!

package «lean_proj» where

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.18.0"

require Canonical from git
  "https://github.com/chasenorman/CanonicalLean.git"

I did these things:

• Change my lean-toolchain file to leanprover/lean4:v4.18.0
• Add the @ "v4.18.0" to the require mathlib line in my lakefile.lean
• Delete the .lake folder and the lake-manifest.json file
• Run lake update mathlib
• Run Reload Window in VSCode

I thought the lean-toolchain file controlled the toolchain version, but it seems like mathlib determines it instead.

[Chase Norman]

@Deming Xu In short, Canonical does as you say, preferring Eq.refl to Eq.rec where possible. However, there are some complexities here due to definitional equality. Canonical decides to work on the goal x * x = 0 before the goal x : Nat, and since x * x does not definitionally reduce to 0, Eq.refl fails in the default setting.

[Chase Norman]

This is what the +synth flag is for, but it is currently an unstable feature.

[Kim Morrison]

Deming Xu said:

I thought the lean-toolchain file controlled the toolchain version, but it seems like mathlib determines it instead.

lean-toolchain does control the toolchain version! The subtlety is that lake update will modify it if the updated dependencies all agree on some later toolchain.