Proof by reflection

Stream: new members

[Nada Amin]

I was looking at the seminal FOL system from the late 70s, which shows the first instance of proof by reflection.

I have a live playground here: https://io.livecode.ch/learn/namin/GETFOL

I wanted to show a simple example of proof by reflection in GETFOL and Lean 4.
The example is proving that a number is even by calculating parity.

Example in GETFOL: https://io.livecode.ch/repl/namin/GETFOL#9781902967e45e3f0901260be9b9c2d0

Example in Lean 4:

-- Even number checking by reflection in Lean 4
-- This parallels our GETFOL example

-- Object level: inductively defined Even predicate
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ_succ : ∀ n, Even n → Even (n + 2)

-- First, let's prove some facts the hard way by applying the inductive constructors
theorem even2_hard : Even 2 := by
  apply Even.succ_succ
  exact Even.zero

theorem even4_hard : Even 4 := by
  apply Even.succ_succ
  apply Even.succ_succ
  exact Even.zero

-- Meta level: computational even checker
def isEven : Nat → Bool
  | 0 => true
  | 1 => false
  | n + 2 => isEven n

-- Test our computational definition
#eval isEven 0    -- true
#eval isEven 2    -- true
#eval isEven 4    -- true
#eval isEven 7    -- false
#eval isEven 100  -- true

-- Soundness theorem: if isEven returns true, then Even holds
theorem isEven_sound (n : Nat) : isEven n = true → Even n :=
  match n with
  | 0 => fun _ => Even.zero
  | 1 => fun h => by simp [isEven] at h
  | n + 2 => fun h => by
    simp [isEven] at h
    exact Even.succ_succ n (isEven_sound n h)
termination_by n

-- Reflection tactic - this is like GETFOL's reflect command
syntax "reflect_even" : tactic
macro_rules
  | `(tactic| reflect_even) => `(tactic| apply isEven_sound; rfl)

-- Now prove facts by reflection (like GETFOL's reflect MAKETHM FACT2)
example : Even 2 := by reflect_even
example : Even 4 := by reflect_even
example : Even 6 := by reflect_even
example : Even 100 := by reflect_even
example : Even 1000 := by reflect_even

The example in Lean 4 doesn't really move from object level to meta level and back explicitly, and feels rather standard, completely incorporated into the language. Would you still call this proof by reflection, or would you reserve the term for some fancier metaprogramming?

Thanks!

[Eric Wieser]

My very limited understanding is that this does indeed count as reflection, but is doing roughly the same thing as the builtin decide tactic does

[Kyle Miller]

Here's how to hook into decide:

-- Object level: inductively defined Even predicate
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ_succ : ∀ n, Even n → Even (n + 2)

-- Meta level: computational even checker
def isEven : Nat → Bool
  | 0 => true
  | 1 => false
  | n + 2 => isEven n

theorem isEven_iff {n : Nat} : isEven n = true ↔ Even n := by
  constructor
  · fun_induction isEven n <;> simp +contextual [Even.zero, Even.succ_succ, *]
  · intro h; induction h <;> simp [isEven, *]

instance (n : Nat) : Decidable (Even n) :=
  decidable_of_decidable_of_iff isEven_iff

example : Even 2 := by decide
example : Even 4 := by decide
example : Even 6 := by decide
example : Even 100 := by decide
example : Even 1000 := by decide +kernel -- skip the elaborator when evaluating `isEven`.

[Kyle Miller]

The decide tactic wants a decision procedure rather than a semidecision procedure, hence the iff version of the soundness theorem.

That does enable many more applications. For example

example : Even 101 := by decide
/-
error: tactic 'decide' proved that the proposition
  Even 101
is false
-/

example : ¬ Even 101 := by decide -- succeeds

[Kyle Miller]

Or even

example : ∀ n < 10, Even (2 * n) := by decide

example : ∀ n < 10, Even (2 * n) ∧ ¬ Even (2 * n + 1) := by decide

[Kyle Miller]

Nada Amin said:

The example in Lean 4 doesn't really move from object level to meta level and back explicitly, and feels rather standard, completely incorporated into the language.

I guess this illustrates the progress in ITPs since the 70s!

Having a theory with a notion of computation via reduction is very powerful. Lean's kernel can compute with recursively defined functions thanks to the computation rules of recursors.

[Jireh Loreaux]

except that it doesn't work for well-founded recursion :sad:

[Nada Amin]

@Kyle Miller thanks for the snippets. Which version of Lean are you using? In 4.20.1, I get simp made no progress for this simp +contextual [Even.zero, Even.succ_succ, *].

[Kyle Miller]

If you click the "view in lean playground" button in the upper right corner of the snippet, it seems to work. The #version command says it's running 4.21.0-rc3.

[Junyan Xu]

I recently had the idea that since Lean now trusts GMP and uses it in the kernel, it might be very efficient to encode data as integers and perform computations there. (I'm mainly concerned with polynomials. Verifying (1 + X) ^ 11 = 1 + X ^ 11 in ZMod 11 by decide takes 3 seconds with exponentiation by squaring implemented, and I'm thinking about ways to speed this up possibly using a better data structure, e.g. a sigma type of iterated product types, or just a bignum.)

[Kyle Miller]

The new grind tactic (which I believe will not have the "this is experimental warning" in the next Lean release!) does this example in 28ms on my machine:

theorem baz : (X + 1 : (ZMod 11)[X]) ^ 11 = X ^ 11 + 1 := by
  grind

[Kyle Miller]

(Tested on a mathlib master branch from a few days ago.)

[Kyle Miller]

If I'm reading the generated proof correctly, it decides to do a proof by reflection. It converts both polynomials to an efficient polynomial type (docs#Lean.Grind.CommRing.Poly) and then gets the kernel to evaluate both sides.

[Junyan Xu]

Thanks! Where is the conversion from Polynomial to docs#Lean.Grind.CommRing.Poly? Code search and Loogle found nothing relevant.

[Junyan Xu]

cc @Hagb (Junyu Guo) @Junqi Liu

[Kyle Miller]

I believe the integration with grind is done purely through docs#CommRing.toGrindCommRing (and docs#instIsCharPOfCharP)

It's not seeing Polynomial as being polynomials per se, but it's recognizing that these are ring expressions, and that X can be regarded as a variable. (Similar to atoms in linarith.)

This works too:

theorem baz (a b : (ZMod 11)[X]): (a + b : (ZMod 11)[X]) ^ 11 = a ^ 11 + b ^ 11 := by
  grind

In the proof, it's calling a and b variables number 0 and 1.

[Hagb (Junyu Guo)]

It is amazing! I was working on a Batteries.RBMap-based solution for faster speed, and now I can see grind is much faster than it!

[Junyan Xu]

Hmm I'm not quite seeing the difference between docs#CommRing and docs#Lean.Grind.CommRing; it seems they mainly differ in that the latter doesn't extend NatCast etc. but includes them as fields.

[Kyle Miller]

The difference is that Lean.Grind.CommRing is designed specifically for the grind tactic, and it is the interface for hooking user's types into the tactic.

This is good practice for designing tactics. This lets theory develop for sake of theory while letting the metaprogram have a fixed interface. No need for compromises.

[Junyan Xu]

Oh I missed that Grind.CommRing is also more minimal as it doesn't include zsmul etc.

[Kyle Miller]

(Even if it did have a need for zsmul etc., it still is better to have a separate class.)

Another thing to think about is that if Lean.Grind.CommRing extended anything like NatCast, then that instance could start providing the NatCast instance rather than the one that's defined for theory purposes. There might be a more-efficient implementation that's better suited for these grind proofs.

[Hagb (Junyu Guo)]

For polynomial ring R[X] over R, it seems that smul of an element of R and an element of R[X] should be covered to deal with polynomial (or more generally Module)?
As an example:

import Mathlib
open Polynomial
example : (1 / 2 : ℚ) • X * 2 = (X : ℚ[X]) := by
  grind -- fail
example : (-2 : ℤ) • 2 • X  = -4 • (X : ℤ[X]) := by
  module
example : (-2 : ℤ) • 2 • X  = -4 • (X : ℤ[X]) := by
  grind -- fail

edit: add two other examples.
edit 2: sorry for my off-topic. i just found the topic not specially for polynomial.

[Jz Pan]

It's amazing that docs#Lean.Grind.CommRing does not require mathlib...

[Hagb (Junyu Guo)]

Hagb (Junyu Guo)said：

For polynomial ring R[X] over R, it seems that smul of an element of R and an element of R[X] should be covered to deal with polynomial (or more generally Module)?
As an example:

import Mathlib
open Polynomial
example : (1 / 2 : ℚ) • X * 2 = (X : ℚ[X]) := by
  grind -- fail
example : (-2 : ℤ) • 2 • X  = -4 • (X : ℤ[X]) := by
  module
example : (-2 : ℤ) • 2 • X  = -4 • (X : ℤ[X]) := by
  grind -- fail

edit: add two other examples.
edit 2: sorry for my off-topic. i just found the topic not specially for polynomial.

Hmmm after checking the source code and trying #print the proof of some samples proved by grind, I found Poly uses Int for its "constant" and "coefficient", and when grind deals with ring, parts other than NatCast will keep invariant, corresponding to Poly.var?

[Junyan Xu]

Could grind replace ring and even run faster than it? And field_simp as well (I just saw the new PR #25697)

[Henrik Böving]

ring yes, ring_nf not necessarily