Zulip Chat Archive

Stream: new members

Topic: Reasoning about types within/before lemma parameter


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 19 2020 at 19:36):

I would recommend the later approach.

view this post on Zulip 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.

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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