From c460583a910abbc1733156942899173d11d95d23 Mon Sep 17 00:00:00 2001 From: Joachim Breitner <mail@joachim-breitner.de> Date: Wed, 15 Nov 2023 11:48:36 +0100 Subject: [PATCH 1/2] Add a test case about overriding the prelude Probably not unexpected but without further protection against the `prelude` command, one can easily prove unsound things, as this test demonstrates. It seems that either `lean4checker` should somehow ensure that only an official prelude is used, or else the kernel (which implements `Nat.add` differently) should check that the definition is indeed as expected. I had to restructure the tests into their own library with a `glob`, as _importing_ this file from another file that also imports the normal prelude seems to fail with ``` ./././Lean4CheckerTests.lean:1:0: error: import Lean4CheckerTests.OverridenPrelude failed, environment already contains 'Eq.refl' from Init.Prelude ``` --- Lean4CheckerTests/OverridenPrelude.lean | 22 ++++++++++++++++++++++ test.sh | 8 ++++++++ 2 files changed, 30 insertions(+) create mode 100644 Lean4CheckerTests/OverridenPrelude.lean diff --git a/Lean4CheckerTests/OverridenPrelude.lean b/Lean4CheckerTests/OverridenPrelude.lean new file mode 100644 index 0000000..b1232f9 --- /dev/null +++ b/Lean4CheckerTests/OverridenPrelude.lean @@ -0,0 +1,22 @@ +prelude + +set_option autoImplicit false + +universe u +variable {α : Type u} + +inductive Eq : α → α → Prop where + | refl (a : α) : Eq a a + +inductive Nat where + | zero : Nat + | succ (n : Nat) : Nat + +-- The kernel has a hard-coded interpretation for this function +def Nat.add : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero +-- But not this function +def Nat.add2 : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero + +theorem eq1 (x : Nat ): Eq (Nat.add x Nat.zero) (Nat.add2 x Nat.zero) := Eq.refl _ +theorem eq2 : Eq (Nat.add .zero .zero) (Nat.add2 .zero .zero) := eq1 _ +theorem eq3 : Eq (Nat.zero) (.succ .zero) := eq2 diff --git a/test.sh b/test.sh index a1f6049..cb1e843 100755 --- a/test.sh +++ b/test.sh @@ -1,6 +1,12 @@ #!/usr/bin/env bash +<<<<<<< HEAD lake build +======= +# Because `Lean4CheckerTests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time), +# we just keep rebuilding until it works! +until lake build > /dev/null 2>&1; do :; done +>>>>>>> 8a73e92 (Add a test case about overriding the prelude) check_command() { local cmd="$1" @@ -38,4 +44,6 @@ rm -f .lean4checker.tmp check_command "lake exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'" rm -f .lean4checker.tmp +check_command "lake exe lean4checker Lean4CheckerTests.OverridenPrelude" "TODO" + echo "All commands produced the expected errors." From 09aea165845db3a67da2a7828bee09ea57abd24b Mon Sep 17 00:00:00 2001 From: Joachim Breitner <mail@joachim-breitner.de> Date: Wed, 15 Nov 2023 13:55:48 +0100 Subject: [PATCH 2/2] Nicer counter-example --- Lean4CheckerTests/OverridenPrelude.lean | 23 ++++++++++++----------- test.sh | 6 ------ 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/Lean4CheckerTests/OverridenPrelude.lean b/Lean4CheckerTests/OverridenPrelude.lean index b1232f9..6d0f4a1 100644 --- a/Lean4CheckerTests/OverridenPrelude.lean +++ b/Lean4CheckerTests/OverridenPrelude.lean @@ -2,21 +2,22 @@ prelude set_option autoImplicit false -universe u -variable {α : Type u} - -inductive Eq : α → α → Prop where - | refl (a : α) : Eq a a - inductive Nat where | zero : Nat | succ (n : Nat) : Nat -- The kernel has a hard-coded interpretation for this function +-- which differs from the one we give here def Nat.add : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero --- But not this function -def Nat.add2 : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero -theorem eq1 (x : Nat ): Eq (Nat.add x Nat.zero) (Nat.add2 x Nat.zero) := Eq.refl _ -theorem eq2 : Eq (Nat.add .zero .zero) (Nat.add2 .zero .zero) := eq1 _ -theorem eq3 : Eq (Nat.zero) (.succ .zero) := eq2 +inductive Empty : Type +structure Unit : Type + +def T (n : Nat) : Type := + Nat.rec Empty (fun _ _ => Unit) n + +def test (n : Nat) : T (Nat.add n .zero) := Unit.mk +def test0 : T (Nat.add .zero .zero) := test .zero +def empty : Empty := test0 + +theorem boom (P : Prop) : P := Empty.rec empty diff --git a/test.sh b/test.sh index cb1e843..049238c 100755 --- a/test.sh +++ b/test.sh @@ -1,12 +1,6 @@ #!/usr/bin/env bash -<<<<<<< HEAD lake build -======= -# Because `Lean4CheckerTests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time), -# we just keep rebuilding until it works! -until lake build > /dev/null 2>&1; do :; done ->>>>>>> 8a73e92 (Add a test case about overriding the prelude) check_command() { local cmd="$1"