## Stream: new members

### Topic: Reasoning about types within/before lemma parameter

#### Daan van Gent (Sep 19 2020 at 19:31):

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 (Sep 19 2020 at 19:35):

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

#### Johan Commelin (Sep 19 2020 at 19:35):

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 (Sep 19 2020 at 19:36):

I would recommend the later approach.

#### Kyle Miller (Sep 19 2020 at 19:43):

Johan Commelin said:

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

#### Daan van Gent (Sep 19 2020 at 19:57):

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 (Sep 19 2020 at 21:40):

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 (Sep 19 2020 at 21:48):

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 (Sep 19 2020 at 21:56):

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 (Sep 19 2020 at 22:02):

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

#### Kenny Lau (Sep 19 2020 at 22:04):

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

Last updated: May 13 2021 at 17:42 UTC