Zulip Chat Archive

Stream: general

Topic: quotient.lift_on elaboration


view this post on Zulip Kenny Lau (Jul 06 2019 at 04:23):

import data.set.basic

-- works
example {α β : Type*} [setoid α] (s : set β) [setoid s]
  (f : α  β) (hf1 :  x, f x  s) (hf2 :  x y, x  y  (f x, hf1 x : s)  f y, hf1 y) :
  quotient _inst_1  quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, (f r, hf1 r : s)) $ λ x y hxy, quotient.sound $ hf2 x y hxy

/-
invalid constructor ⟨...⟩, expected type is not an inductive type
  ?m_1
-/
example {α β : Type*} [setoid α] (s : set β) [setoid s]
  (f : α  β) (hf1 :  x, f x  s) (hf2 :  x y, x  y  (f x, hf1 x : s)  f y, hf1 y) :
  quotient _inst_1  quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, f r, hf1 r) $ λ x y hxy, quotient.sound $ hf2 x y hxy

view this post on Zulip Kenny Lau (Jul 06 2019 at 04:24):

why does it fail when I have an inductive type?

view this post on Zulip Mario Carneiro (Jul 06 2019 at 04:54):

it's an elaboration order problem. Anonymous constructors must resolve to an inductive type straight away, but I guess the other stuff is getting elaborated before lean knows what the target type is of the function


Last updated: May 18 2021 at 16:25 UTC