magical witness

Stream: lean4

[Michael Jam]

Good morning, if I'm not mistaken, Lean should not be able to compute this function:

def witness : Nat := (⟨1, Nat.le_refl _⟩ : ∃ x, x ≥ 1).1
#eval witness -- displays a mysterious 0
#reduce witness -- displays 1
#print axioms witness -- surprisingly doesn't require choice

Even if you parameterize the existential statement with a predicate, it compiles by magic. I'm using nightly 2022-02-24

[Johan Commelin]

For reference, this is what I need in recent Lean 3:

import data.nat.basic

noncomputable
def witness : ℕ := (⟨1, le_refl _⟩ : ∃ x, x ≥ 1).some
#eval witness -- code generation failed, VM does not have code for 'witness'
#reduce witness -- (classical.choice _).val
#print axioms witness -- classical.choice propext

[Gabriel Ebner]

This reminds me of: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Getting.20witnesses.20used.20in.20existential.20proofs.3F (it's not the same thing though)

[Mario Carneiro]

Oh, that's bad, I think this is unsound

[Gabriel Ebner]

@Michael Jam What you're probably seeing here is that the compiler simplifies the code by reducing the terms. And Exists.rec .. Exists.intro reduces to the witness.

[Gabriel Ebner]

@Mario Carneiro I'm not sure I would call it unsound (since it doesn't compromise consistency), but it is certainly unsafe since it most likely allows you to break referential transparency.

[Mario Carneiro]

No, it works in rfl proofs too. Proof of false coming up

[Gabriel Ebner]

Wait what?!?

[Gabriel Ebner]

I didn't realize that this reduced in the kernel. You can write theorem foo : witness = 1 := rfl. :fear:

[Mario Carneiro]

def witness : Nat := (⟨0, trivial⟩ : ∃ x, True).1
def witness2 : Nat := (⟨1, trivial⟩ : ∃ x, True).1
theorem t1 : witness = 0 := rfl
theorem t2 : witness2 = 1 := rfl
def foo (h : ∃ x:Nat, True) := h.1
theorem t3 : foo ⟨0, trivial⟩ = witness := rfl
theorem t4 : foo ⟨1, trivial⟩ = witness2 := rfl
theorem t5 (h1 h2) : foo h1 = foo h2 := rfl
theorem contradiction : False := by
  have : witness = witness2 := t3.symm.trans ((t5 _ _).trans t4)
  have : 0 = 1 := this
  have h : 0 ≠ 1 := by decide
  exact h this

[Michael Jam]

You were faster, than me :) I couldn't figure out how to exploit it

[Mario Carneiro]

minimized

def foo (h : ∃ x: Nat, True) := h.1
theorem contradiction : False :=
  (by decide : 0 ≠ 1) (show foo ⟨0, trivial⟩ = foo ⟨1, trivial⟩ from rfl)

[Mario Carneiro]

The issue is the primitive projections. These should not exist for small eliminating types (i.e. h.1 should not typecheck on a thing of type Exists p)

[Gabriel Ebner]

This bug goes way back, at least until a year ago.

[Patrick Massot]

But it's not in Lean 3, right?

[Mario Carneiro]

(These did not exist in lean 3 BTW, this was one of the kernel changes)

[Patrick Massot]

Is it clear what changed in the kernel and causes this?

[Mario Carneiro]

Lean 3 does have partial support for projections as kind-of-magic but they were at least nominally given a definition in terms of rec

[Patrick Massot]

Is it a change we needed for something else?

[Gabriel Ebner]

We did have similar projection (macro)s in Lean 3, but a) I don't think they had that bug, and b) we're running an external type checker on mathlib which would have caught this bug.

[Mario Carneiro]

When I try

def foo (h : True ∨ True) := h.1

I get

invalid projection, structure expected
  h
has type
  True ∨ True

so there is some structure check going on, but Exists is being erroneously considered a structure for this purpose

[Mario Carneiro]

There needs to be an extra check around here to assert that the inductive is large eliminating. There doesn't seem to be a convenient accessor for this in the inductive_val or recursor_val (there is is_K but this is a slightly different thing), but you can check if the recursor has the same number of universe levels as the inductive type. cc: @Leonardo de Moura

[Michael Jam]

Being able to do .1 / .2 on an Exists is useful, but it should be nothing more than a shortcut for Classical.choose / Classical.choose_spec as I see it

[Leonardo de Moura]

Thanks for reporting this serious issue. I just pushed a fix for it.
https://github.com/leanprover/lean4/commit/db38bc404388b6b7ea2fe4589f417265a988eb95