Zulip Chat Archive

Stream: general

Topic: more defeq among foundational types


Junyan Xu (Nov 03 2022 at 21:47):

The duplication between psigma and sigma in this PR has prompted me to think about making docs#sigma a reducible def in terms of docs#psigma, so everything proven about psigma will be immediately applicable to sigma, without needing to write any tactic to transport between them. Presumably the same could be done for docs#psum and docs#sum, docs#pprod and docs#prod, though pprod isn't used much AFAIK.

Today I came up with another idea: if we make docs#and a reducible def in terms of docs#exists, then src#exists_prop would be iff.rfl, so ∃ x ∈ s, p x would be the same as ∃ x, x ∈ s ∧ p x. Maybe people can come up with other examples for which this could lead to potential simplifications? I expect such changes won't break many things because it doesn't break any defeq, only makes more things defeq, but most of these are so fundamental that they're in core, and I'm not sure about the prospects of such changes to be accepted, especially considering that the transition to Lean 4 is near, and Lean 4 core isn't a lean-community fork but under official development.

Examples:

universes u v
@[reducible] def sigma' {α : Type u} (β : α  Type v) : Type (max u v) := psigma β

@[reducible] def and' (p q : Prop) : Prop :=  h : p, q
lemma and'.left {p q} : and' p q  p := λ hp, _⟩, hp
lemma and'.right {p q} : and' p q  q := λ _, hq⟩, hq

Notification Bot (Nov 03 2022 at 21:51):

A message was moved here from #general > empty definition by Junyan Xu.

Eric Wieser (Nov 03 2022 at 22:08):

Note that we recently changed the definition of fin to not be defeq to subtype

Eric Wieser (Nov 03 2022 at 22:09):

I think there's a good argument to do this for psigma/sigma + pprod/prod where the semantics really are the same, but I don't think aliasing and and exists is obviously a good idea.

Yaël Dillies (Nov 04 2022 at 06:05):

and possibly docs#pempty, docs#empty, docs#false?

Yaël Dillies (Nov 04 2022 at 06:56):

Oh sorry, I see my original message was moved to this topic.


Last updated: Dec 20 2023 at 11:08 UTC