66bc9ae177
This PR deprecates `levelZero` in favor of `Level.zero` and `levelOne`
in favor of the new `Level.one`, and updates all usages throughout the
codebase. The `levelZero` alias was previously required for computed
field `data` to work, but this is no longer needed.
🤖 Prepared with Claude Code
111 lines
3.2 KiB
Text
111 lines
3.2 KiB
Text
import Lean
|
|
/-!
|
|
# The kernel does not allow primitive projections on propositions
|
|
|
|
This test is adapted from the test introduced in commits
|
|
7920db952116e838b31c6f59f17bde0af01df545 and 3746005f5fc35d030d26ced2f7bcaabc295224c2,
|
|
and which was removed in #8986 because the elaborator is better at rejecting them.
|
|
In this version, we do direct tests of the kernel.
|
|
-/
|
|
|
|
open Lean Meta
|
|
|
|
set_option pp.proofs true
|
|
|
|
/-!
|
|
Projection to the witness should be rejected.
|
|
|
|
This test is creating the declaration
|
|
```
|
|
def test.witness : Nat := (Exists.intro 0 True.intro : ∃ x : Nat, True).1
|
|
```
|
|
-/
|
|
/--
|
|
error: (kernel) invalid projection
|
|
(Exists.intro Nat.zero True.intro).1
|
|
-/
|
|
#guard_msgs in
|
|
#eval do
|
|
addDecl <| .defnDecl {
|
|
name := `test.witness
|
|
levelParams := []
|
|
type := mkConst `Nat
|
|
hints := .abbrev
|
|
safety := .safe
|
|
value :=
|
|
mkProj ``Exists 0 <|
|
|
mkApp4 (mkConst ``Exists.intro [Level.one])
|
|
(mkConst ``Nat)
|
|
(mkLambda `x .default (mkConst ``Nat) (mkConst ``True))
|
|
(mkConst ``Nat.zero)
|
|
(mkConst ``True.intro)
|
|
}
|
|
|
|
/-!
|
|
`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.)
|
|
-/
|
|
#guard_msgs in
|
|
#eval do
|
|
addDecl <| .defnDecl {
|
|
name := `test.witness'
|
|
levelParams := []
|
|
type := mkConst `Nat
|
|
hints := .abbrev
|
|
safety := .safe
|
|
value :=
|
|
mkProj ``Subtype 0 <|
|
|
mkApp4 (mkConst ``Subtype.mk [Level.one])
|
|
(mkConst ``Nat)
|
|
(mkLambda `x .default (mkConst ``Nat) (mkConst ``True))
|
|
(mkConst ``Nat.zero)
|
|
(mkConst ``True.intro)
|
|
}
|
|
|
|
/-!
|
|
Projection to the property should be rejected as well (it could contain the witness projection).
|
|
|
|
This test is creating the declaration
|
|
```
|
|
theorem test.witness_eq (h : ∃ x : Nat, True) : h.2 = h.2 := rfl
|
|
```
|
|
-/
|
|
/--
|
|
error: (kernel) invalid projection
|
|
h.2
|
|
-/
|
|
#guard_msgs in
|
|
#eval do
|
|
addDecl <| .thmDecl {
|
|
name := `test.witness_eq
|
|
levelParams := []
|
|
type :=
|
|
mkForall `h .default
|
|
(mkApp2 (mkConst ``Exists [Level.one]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
|
|
(mkApp3 (mkConst ``Eq [Level.zero])
|
|
(mkConst ``True)
|
|
(mkProj ``Exists 1 (mkBVar 0))
|
|
(mkProj ``Exists 1 (mkBVar 0)))
|
|
value := mkLambda `h .default
|
|
(mkApp2 (mkConst ``Exists [Level.one]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
|
|
(mkApp2 (mkConst ``Eq.refl [Level.zero]) (mkConst ``True) (mkProj ``Exists 1 (mkBVar 0)))
|
|
}
|
|
|
|
/-!
|
|
`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.)
|
|
-/
|
|
#guard_msgs in
|
|
#eval do
|
|
addDecl <| .thmDecl {
|
|
name := `test.witness_eq'
|
|
levelParams := []
|
|
type :=
|
|
mkForall `h .default
|
|
(mkApp2 (mkConst ``Subtype [Level.one]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
|
|
(mkApp3 (mkConst ``Eq [Level.zero])
|
|
(mkConst ``True)
|
|
(mkProj ``Subtype 1 (mkBVar 0))
|
|
(mkProj ``Subtype 1 (mkBVar 0)))
|
|
value := mkLambda `h .default
|
|
(mkApp2 (mkConst ``Subtype [Level.one]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
|
|
(mkApp2 (mkConst ``Eq.refl [Level.zero]) (mkConst ``True) (mkProj ``Subtype 1 (mkBVar 0)))
|
|
}
|