PR summary 7c885dc01c

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

a) Do you really, really, really need unbundled relations for what you're doing? Forcibly turning a bundled predicate into an unbundled one is certainly the opposite of what we should be doing. If the issue is that you need both a normal ordering and a well-ordering on the same type, might I suggest a type alias?

b) This seems a bit similar to StrictMono.id_le. Can you reprove one using the other?

a) I'm accepting an arbitrary type α and an arbitrary well-order on it. Using instances such as LE/LT means that users will have to use type-aliases to use different orders. I even have a theorem with ∃ (r : α → α → Prop) (hr : IsWellOrder α r), ... and I don't see how it makes sense with bundled relations. The only thing I can think of is to add something like WithLT α r to Mathlib as a type-alias with instance LT (WithLT α r) := ⟨r⟩ and instance LT (WithLE α r) := ⟨¬r · ·⟩.

b) Yeah but it doesn't work for an arbitrary lower-set, and also I need monotonicity to use StrictMono.id_le in either direction, which I don't have.

The only thing I can think of is to add something like WithLT α r to Mathlib as a type-alias with instance LT (WithLT α r) := ⟨r⟩ and instance LT (WithLE α r) := ⟨¬r · ·⟩.

My idea was to create a WellOrdered α type alias, which is in bijection with α but has a well-ordered < relation. Surely that's enough for what you're doing?

By "has a well-ordered < relation" do you mean to use WellOrderingRel?

How would you spell IsFoo α ↔ ∃ (r : α → α → Prop) (hr : IsWellOrder α r), IsBar α using WellOrdered α?

I wouldn't spell it out directly, it'd be implied by the equivalence to WellOrder \a.