[Merged by Bors] - feat(Mathlib/Tactic/TypeCheck): add type_check tactic

[j-loreaux]

Lean 3 version: https://github.com/leanprover-community/lean/blob/master/library/init/meta/interactive.lean#L1664

[arthurpaulino]

Gotta add it to the Mathlib.lean import list 👍🏼

[digama0]

Suggested change

	example : True := by {
	type_check Nat; -- Type
	type_check Bool.true; -- Bool
	type_check nat_lit 1; -- Nat
	type_check (1 : Nat); -- Nat
	type_check (True : _); -- Prop
	type_check ∀ x y : Nat, x = y; -- Prop
	type_check fun x : Nat => 2 * x + 1; -- Nat -> Nat
	exact True.intro }
	example : True := by
	type_check Nat -- Type
	type_check Bool.true -- Bool
	type_check nat_lit 1 -- Nat
	type_check (1 : Nat) -- Nat
	type_check (True : _) -- Prop
	type_check ∀ x y : Nat, x = y -- Prop
	type_check fun x : Nat => 2 * x + 1 -- Nat -> Nat
	trivial

[digama0]

This needs some type check error tests as well, using fail_if_success.

[semorrison]

Marking as unresolved, as we still need to error tests.

[j-loreaux]

I'm not sure I understand, can you explain in more detail what we need?

[digama0]

e.g. fail_if_success type_check 2 + "hi"

[semorrison]

#334 has an alternative expect_failure tactic which should give you what you want here. We'll try to merge that soon?

[semorrison]

Oh dear, type_check 2 + "hi" fails correctly with failed to synthesize instance HAdd Nat String ?m.160, but expect_failure type_check 2 + "hi" (after merging master into this PR) claims tactic sequence succeeded.

@digama0 or @gebner, could you suggest how we should be testing this?

[digama0]

This is a bug in fail_if_success/success_if_fail/expect_failure (the synonyms keep piling up...), not type_check. As mentioned in the zulip thread, these tactics need to be wrapped in withoutRecover (or possibly we need a ! variant of the tactic that uses this).

[arthurpaulino]

@digama0 expect_failure already uses withoutRecover

[gebner]

could you suggest how we should be testing this?

I'm not 100% sure what type_check is supposed to do, but I guess it's supposed to find bugs in proofs produced by tactics. So I would suggest to test a tactic or elaborator that produces a term which does not type check. Such as this one:

/-- A term where `inferType` returns `Prop`, but which does not type check. -/
elab "wrong" : term =>
  return Lean.mkApp2 (.const ``id [.zero]) (.sort .zero) (.app (.sort .zero) (.sort .zero))

I have committed this elaborator and a failing test case.

[gebner]

Thank!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build