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"