Simplifying the type of a term easily?

Stream: new members

[Fernando Chu]

I often find myself writing something like

import Mathlib

axiom x : ℕ
axiom y : ℕ

@[simp]
lemma foo : x = y := sorry

def bar (P : ℕ → Type) : P y := by
  let baz : P x := sorry -- This is usually a small term mode term
  simp at baz
  exact baz

Is there an easier way to just use baz and convince Lean that it has the right type in one line?

[Henrik Böving]

foo ▸ baz maybe?

[Fernando Chu]

Thanks, trying to do this with (by simp) ▸ baz this does not work. Is there a way to make it work? The simp proof actually uses a decent number of lemmas.

[Henrik Böving]

have h : x = y := by simp
h ▸ baz

[Fernando Chu]

Sadly both x and y are horrible, but I understand that this is a pretty idiomatic solution, thanks.

[Fernando Chu]

Wondering if Mathlib would like an exact_by x p that takes any x : A and a p : A = Goal, importantly p can be by simp.

[Aaron Liu]

Fernando Chu said:

Wondering if Mathlib would like an exact_by x p that takes any x : A and a p : A = Goal, importantly p can be by simp.

Try convert x

[Fernando Chu]

Aaron Liu said:
Try convert x

This is what I was looking for, great, thank you!

[Aaron Liu]

You shouldn't be using tactics to construct data, though

[Fernando Chu]

why not?

[Aaron Liu]

because presumably you care about which data gets constructed and many tactics don't give you control of that

[Kyle Miller]

When in doubt "don't use tactics to construct data" is a very good rule of thumb.

There are some exceptions when you know exactly what you need the data for and/or if you know exactly what the tactics are doing. The main reason for the rule is that tactics such as simp/convert/rw and the triangle operator insert casts (Eq recursors) to change types, and these are not friendly for definitional equality. (What Aaron said.)

Even cases inserts casts as part of its normal operation.

What you see are definitions in the library like docs#decidable_of_iff to be able to modify types of data in a controlled way. If your P is a specific type outside of this #mwe, then I'd suggest creating similar cast functions. You can find examples in the library as MyType.cast or MyType.copy, for reference.

[Fernando Chu]

Thanks for the indepth explanation!