more defeq among foundational types

Stream: general

[Junyan Xu]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Yaël Dillies]

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