Lean accepts {! !} within proofs leading to inconsistent type-checking.

[spolu]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean accepts {! !} within proofs leading to inconsistent type-checking.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Question.20about.20.7B!.20!.7D

Steps to Reproduce

import data.finset.basic
import data.nat.interval

example
  (vertices : finset ℕ)
  (diagonals : finset (finset ℕ))
  (h₀ : vertices = finset.Icc 1 5)
  (h₁ : ∀ (m n : ℕ), ({m,n} : finset ℕ) ∈ diagonals ↔
    {m,n} ⊂ vertices ∧ m ≠ n ∧ m ≠ n + 1 ∧ m ≠ n - 1 ∧ {m,n} ≠ ({1,5} : finset ℕ)) :
  diagonals.card = 5 :=
begin
  have h₂ : diagonals = {! {2,4}, {1,3}, {3,5} !}, {
    dec_trivial!,
  },
  rw h₂,
  dec_trivial!,
end

Expected behavior:

Errors

Actual behavior:

Gladly accepts the proof

Reproduces how often:

100%

Versions

Lean (version 3.42.1, commit 68455b0, Release)

[spolu]

Actually interpreted as a sorry and reported as a warning at build. Closing

[gebner]

Gladly accepts the proof

I'm getting a warning here:

/home/gebner/mathlib/725.lean:4:0: warning: declaration '[anonymous]' uses sorry

There's a whole bunch of tactics which don't fail immediately but ultimately result in an invalid proof. Here's some archetypical ones from the top of my head:

example : false := by tactic.set_goals []
example : false := by exact undefined
example : false := by exact sorry

example : false :=
begin
  tactic.add_decl (declaration.ax `very.clever [] `(false)),
  exact very.clever,
end

The last one doesn't even produce a warning. In general, the whole trust model of Lean depends on the kernel type checker. Tactics will occasionally produce invalid proof terms due to bugs.