Experimenting with leanchecker

Stream: general

[Donald Sebastian Leung]

So I've just been experimenting with the -E option of lean and leanchecker, and came across the following error which I do not understand.

Suppose I am working on a Lean project with the following three files:

Preloaded.lean:

-- Task 1: no axioms required
def task_1 := ∀ n m : ℕ, n + m = n + m

-- Task 2: using `simp` introduces `propext`
def task_2 := ∀ n m : ℕ, n + m = m + n

-- Task 3: requires all 3 core axioms
def task_3 := ∀ p : Prop, p ∨ ¬p

-- Task 4: unprovable
def task_4 := 1 + 1 = 3

-- Boilerplate code for bundling all tasks into one
def SUBMISSION := task_1 ∧ task_2 ∧ task_3 ∧ task_4
notation `SUBMISSION` := SUBMISSION -- to prevent cheating

Solution.lean:

import Preloaded
open classical

-- Task 1: Prove that n + m = n + m
theorem immediate : ∀ n m : ℕ, n + m = n + m :=
begin
  intros,
  refl,
end

-- Task 2: Prove that n + m = m + n
theorem plus_comm : ∀ n m : ℕ, n + m = m + n :=
begin
  intros,
  simp,
end

-- Task 3: Prove excluded middle
theorem excluded_middle : ∀ p : Prop, p ∨ ¬p := em

-- Task 4: Prove that 1 + 1 = 3
theorem one_plus_one_is_three : 1 + 1 = 3 := sorry

-- Do NOT modify this section
theorem solution : SUBMISSION := ⟨
  immediate,
  plus_comm,
  excluded_middle,
  one_plus_one_is_three
⟩

SolutionTest.lean:

import Preloaded
import Solution

theorem submission : SUBMISSION := solution

When I compile the files using lean SolutionTest.lean, I get a few warnings regarding the usage of sorry but nothing more (which I assume is a success). However, if I compile the files using lean SolutionTest.lean -E SolutionTest.out, I get <unknown>:1:1: error: failed to expand macro on top of the warnings about sorry. When I then run leanchecker SolutionTest.out submission to check the axioms used in submission, I get unknown declaration 'submission'.

Any hints on how to fix this would be much appreciated :smile:

[Gabriel Ebner]

The text export (i.e. lean -E) fails if there are sorrys in the lean file. This is by design: the export is intended for proof checkers, and sorrys are never valid proofs. An easy workaround is to change theorem one_plus_one_is_three to axiom one_plus_one_is_three.

[Kevin Buzzard]

An easy workaround is to change theorem one_plus_one_is_three to axiom one_plus_one_is_three.

I might tell some of my colleagues in the maths department about this trick

[Donald Sebastian Leung]

Gabriel Ebner said:

The text export (i.e. lean -E) fails if there are sorrys in the lean file. This is by design: the export is intended for proof checkers, and sorrys are never valid proofs. An easy workaround is to change theorem one_plus_one_is_three to axiom one_plus_one_is_three.

Thanks - I changed it to an axiom and the export + leanchecker worked as intended.