Reasoning about types within/before lemma parameter

Stream: new members

[Daan van Gent]

Say I have the following 'lemma':

lemma mwe (α β : Type*) (h : α = β) (a : α) (b : β) (h' : a = b) : Prop := true

Lean will not accept this, because it does not realize at h' that a and b have the same type due to h.
One way to fix this is to remove h and replace all occurrences of β with α.
However, is there a way to reason before or inside the definition of h' that it type-checks?

[Johan Commelin]

You can either use heq instead of = for h', which is regarded evil, or you turn h into an equiv.

[Johan Commelin]

If you say that \a and \b are equivalent types, then you can push a through the equivalence and assert (in h') that its image is equal to b.

[Johan Commelin]

I would recommend the later approach.

[Kyle Miller]

Johan Commelin said:

You can either use heq instead of = for h', which is regarded evil, or you turn h into an equiv.

(Perhaps see also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20alternative/near/210378730 which is a really great trick.)

[Daan van Gent]

The fact that the first solution is regarded evil is due to equality of types being evil, right?
Either way, thanks for the suggestions! I will be trying Kyle/Reid's trick first, it looks very interesting.

[Daan van Gent]

I still got stuck on this, maybe one of you can help. This is what I want to define, written in terms of heq:

def lift_on' {α : Type*} [s : setoid α]
{t : α → Type*} {ht : ∀ a b : α, a ≈ b → t a = t b}
(f : ∀ a : α, t a) (hf : ∀ a b : α, a ≈ b → f a == f b) : ∀ q : quotient s, quot.lift_on q t ht

My best attempt

begin
  intro q,
  induction q with a a b h,
  exact f a,
  specialize ht a b h,
  specialize hf a b h,
  let fa := f a,
  let fb := f b,
  have hf' : fa == fb := hf,
  rw ← ht at fb,
  let hf'' : fa = fb := eq_of_heq hf',
end

arrives at the not very useful error:

type mismatch at application
  eq_of_heq hf'
term
  hf'
has type
  @heq (t a) fa (t b) fb
but is expected to have type
  @heq (t a) fa (t a) fb

[Kyle Miller]

def lift_on' {α : Type*} [s : setoid α]
  {t : α → Type*} {ht : ∀ a b : α, a ≈ b → t a = t b}
  (f : ∀ a : α, t a) (hf : ∀ a b : α, a ≈ b → f a == f b) :
  Π q : quotient s, quot.lift_on q t ht :=
begin
  intro q,
  refine quotient.hrec_on q f _,
  intros a b p,
  exact hf a b p,
end

[Kyle Miller]

I guess it's pretty much just quotient.hrec_on:

def lift_on' {α : Type*} [s : setoid α]
  {t : α → Type*} {ht : ∀ a b : α, a ≈ b → t a = t b}
  (f : ∀ a : α, t a) (hf : ∀ a b : α, a ≈ b → f a == f b) :
  Π q : quotient s, quot.lift_on q t ht :=
λ q, quotient.hrec_on q f hf

[Daan van Gent]

Oh wow! I didn't realize it was already in mathlib.
I guess that was to be expected.
Thanks again!

[Kenny Lau]

Daan van Gent said:

Say I have the following 'lemma':

lemma mwe (α β : Type*) (h : α = β) (a : α) (b : β) (h' : a = b) : Prop := true

Lean will not accept this, because it does not realize at h' that a and b have the same type due to h.
One way to fix this is to remove h and replace all occurrences of β with α.
However, is there a way to reason before or inside the definition of h' that it type-checks?

#xy