WIP: coe_to_fun domain codomain #1838
Conversation
| class has_coe_to_fun (a : Sort u) : Sort (max u (v+1)) := | ||
| (F : a → Sort v) (coe : Π x, F x) | ||
| class has_coe_to_fun (a : Sort u) : Sort (max u (v+1) (w+1)) := | ||
| (domain : a → Sort v) (codomain : Π {x}, domain x → Sort w) (coe : Π x, Π (m : domain x), codomain m) |
There was a problem hiding this comment.
Issue 1: I can't make domain and codomain implicit, despite them being inferrable much of the time, because then I can't nicely specify them when they aren't inferrable. Why can't we specify implicit fields?
| @@ -488,7 +488,8 @@ meta def add_coinductive_predicate | |||
| let (bs, eqs) := compact_relation r.loc_args $ pd.locals.zip r.insts, | |||
| eqs ← eqs.mmap (λ⟨l, i⟩, do | |||
| sort u ← infer_type l.local_type, | |||
| return $ (const `eq [u] : expr) l.local_type i l), | |||
| let final : expr tt := (const `eq [u] : expr) l.local_type i l, | |||
There was a problem hiding this comment.
Issue 2: Despite the relevant has_coe_to_fun instance being found and in principle completely reducible, it's only with this type annotation that the type of this expression actually gets reduced. Why?
| @@ -1,6 +1,7 @@ | |||
| ⇑f 0 1 : ℕ | |||
| f 0 1 : ℕ | |||
| ⇑f 0 1 : ℕ | |||
| @coe_fn.{1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f (@has_zero.zero.{0} nat nat.has_zero) | |||
| @coe_fn.{1 1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f | |||
| (@has_zero.zero.{0} (@has_coe_to_fun.domain.{1 1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f) nat.has_zero) | |||
There was a problem hiding this comment.
Issue 3: How can I tell the pretty printer to please reduce has_coe_to_fun.domain etc.?
tests/lean/run/coe_to_fn.lean
Outdated
| @@ -21,6 +21,6 @@ local postfix `⁻¹` := equiv.inv | |||
| def equiv.trans (f : α ≃ β) (g : β ≃ γ) : α ≃ γ := | |||
| ⟨g ∘ f, f⁻¹ ∘ g⁻¹⟩ | |||
|
|
|||
| example (f : α ≃ β) := function.bijective f | |||
| example (f : α ≃ β) := function.bijective.{u+1 v+1} f | |||
There was a problem hiding this comment.
Issue 4: Why can't lean infer these universes? Or can it, because see:
Issue 5: Why can't lean unify Π (m : has_coe_to_fun.domain f), has_coe_to_fun.codomain m with ?m_1 → ?m_2, when the domain and codomain functions are readily known to be constants and reduce in this context to α and β, respectively?
|
I think #1402 is related to (at least) issue 5. Coercion resolution is not great right now, and more information is currently needed than (hopefully) in the future. Currently it's required that the type you are coercion from doesn't contain any metavariables, and that might include the universe metavariables |
|
@fpvandoorn Hmm, when I turn on implicit pretty-printing I get: type mismatch at application
@function.bijective ?m_1 ?m_2 ⇑f
term
⇑f
has type
Π (m : @has_coe_to_fun.domain (α ≃ β) (@equiv.has_coe_to_fun α β) f),
@has_coe_to_fun.codomain (α ≃ β) (@equiv.has_coe_to_fun α β) f m
but is expected to have type
?m_1 → ?m_2which suggests to me that the coercion and typeclass has fully been resolved? |
|
Anyway explicitly specifying alpha and beta and removing the universe levels works. Pretty annoying though. |
shlevy
force-pushed
the
has_coe_to_fun-domain-codomain
branch
from
ad19353
to
69e7ca3
Compare
There was a problem hiding this comment.
Issue 7: in u_eq_max_u_v.lean, the proof of semigroup_morphism_composition fails to go through, despite the coercion apparently being resolved:
u_eq_max_u_v.lean:49:6: error: simplify tactic failed to simplify
state:
α β γ δ : Type u,
s_f : semigroup.{u} α,
s_g : semigroup.{u} β,
t_f : semigroup.{u} γ,
t_g : semigroup.{u} δ,
f : semigroup_morphism.{u} s_f t_f,
g : semigroup_morphism.{u} s_g t_g,
x y : α × β
⊢ (f.map ((x * y).fst), g.map ((x * y).snd)) = (f.map (x.fst) * f.map (y.fst), g.map (x.snd) * g.map (y.snd))| @@ -21,6 +21,6 @@ local postfix `⁻¹` := equiv.inv | |||
| def equiv.trans (f : α ≃ β) (g : β ≃ γ) : α ≃ γ := | |||
| ⟨g ∘ f, f⁻¹ ∘ g⁻¹⟩ | |||
|
|
|||
| example (f : α ≃ β) := function.bijective f | |||
| example (f : α ≃ β) := @function.bijective α β f | |||
There was a problem hiding this comment.
Issue 6: Why do I need to fill these in explicitly? If I don't I get an error that seems to be related to the lack of reduction of domain and codomain
|
Made a bit more progress. Still having issues, many of which seem to stem from this lack of reduction. |
|
|
I will not merge this PR. As pointed above, we have an open issue for coercion resolution. Moreover, the redundant information that this PR tries to remove is a workaround. I don't have time to discuss why the workaround is need nor help with the PR. Please see: https://github.com/leanprover/lean/blob/master/.github/CONTRIBUTING.md#opening-pull-requests I will close the other PR related with coercion resolution. |
|
Hi @leodemoura, what is the best way to determine if some feature is wanted or not? For reference, the other PR was discussed in the gitter chat before I opened it. |
The best way is to open an issue and describe your plan.
When I wrote |
|
I see. While I have no strong attachment to this specific feature, and of course you're free to run your project however you like, I feel I should point out that the way this was handled and the policies you have make me much less inclined to contribute to lean or become an active member of the community, and in general I would expect this approach to stifle the growth and longer-term viability of the project. There are ways to decline contributions, and ensure your time is respected, without turning away new contributors. |
Similar to #1837 , but for
coe_to_fun. WIP as I work through remaining issues.