Port Order/OrderIsoNat

Stream: mathlib4

[zbatt]

I got started with the OrderIsoNat and it's almost done bar one proof. It's pretty high up in the port status priority list and I don't think I'll be able to finish tonight so I'm just posting in case anyone wants to wrap it up

https://github.com/leanprover-community/mathlib4/pull/1753#issue-1551911732

[zbatt]

It's at a point where everything is done except for one lemma which won't simp away properly

[zbatt]

does anyone know why simp isn't working for Subtype.orderIsoOfNat_apply like it did in Lean3

[Kevin Buzzard]

Some initial remarks for problems of this nature:
1) Check that the statement looks the same in mathlib4 and mathlib3
2) Use squeeze_simp in mathlib3 and see what it's using; does the (appropriately capitalized) output work in mathlib4?
3) You can look at simp logs with set_option trace.Meta.Tactic.simp true in mathlib4 and something like set_option trace.simplify.rewrite true (that last from memory so might not quite be right) in mathlib3.

[zbatt]

The issue is that refl is failing the unify fun a => Classical.propDecidable (a ∈ s) with (fun a => DecidablePred fun x => x ∈ s) a

[zbatt]

that being said I'm not sure how to get these to unify

[James Gallicchio]

Do those two terms have the same type? :thinking:

[zbatt]

The former has type (a : Nat) -> Decidable (a in s) and the latter has type (a : Nat) -> Decidable ((fun x => (x in s)) a). I would assume Lean considers these the same, but I could be wrong

[zbatt]

tbh I'm a bit confused how this worked in lean3. In particular, order_embedding_of_set required that x in s be decidable. But I don't see where its decalred for that to be true in later theorems that have order_embedding_of_setas part of their definition

[zbatt]

for the port, I put [DecidablePred (· ∈ s)] under the declaration of s which solved that requirement, but it could be the cause of this simp not working properly.

[James Gallicchio]

I think at some point in the chain classical sneaks into the axioms and then everything is decidable

[James Gallicchio]

Oh, I see what you mean o.O weird

[James Gallicchio]

zbatt said:

that being said I'm not sure how to get these to unify

RE: this, what's the output with set_option trace.Meta.isDefEq true?

[zbatt]

do you want me to paste the whole thing? there's a ton

[James Gallicchio]

Just follow the x's until the place where it's clear why it's not unifying :)

[zbatt]

I think this is it? I'm not 100% sure tho

[Meta.isDefEq] ❌ ↑?f
      ?n =?= ↑(RelEmbedding.orderEmbeddingOfLTEmbedding
            (RelEmbedding.natLt (Nat.Subtype.ofNat s)
              (_ : ∀ (n : ℕ), Nat.Subtype.ofNat s n < Nat.Subtype.succ (Nat.Subtype.ofNat s n)))).toEmbedding
      n ▼
  [] ✅ ?F =?= ℕ ↪ ↑s ▶
  [] found messy fun a => (fun x => ?R) a =?= fun a => ↑s
  [] ✅ ?f =?= (RelEmbedding.orderEmbeddingOfLTEmbedding
          (RelEmbedding.natLt (Nat.Subtype.ofNat s)
            (_ : ∀ (n : ℕ), Nat.Subtype.ofNat s n < Nat.Subtype.succ (Nat.Subtype.ofNat s n)))).toEmbedding ▶
  [] ✅ ?n =?= n ▶
  [] ✅ ℕ =?= ℕ
  [] ❌ MulHomClass.toFunLike =?= EmbeddingLike.toFunLike ▶
  [onFailure] ❌ ↑?f
        ?n =?= ↑(RelEmbedding.orderEmbeddingOfLTEmbedding
              (RelEmbedding.natLt (Nat.Subtype.ofNat s)
                (_ : ∀ (n : ℕ), Nat.Subtype.ofNat s n < Nat.Subtype.succ (Nat.Subtype.ofNat s n)))).toEmbedding
        n
  [onFailure] ❌ ↑?f
        ?n =?= ↑(RelEmbedding.orderEmbeddingOfLTEmbedding
              (RelEmbedding.natLt (Nat.Subtype.ofNat s)
                (_ : ∀ (n : ℕ), Nat.Subtype.ofNat s n < Nat.Subtype.succ (Nat.Subtype.ofNat s n)))).toEmbedding
        n

[James Gallicchio]

I've never seen it say "found messy ...", no clue what that means

[zbatt]

(deleted)

[zbatt]

I think I was wrong about why this is failing, simp is able to unify fun a => Classical.propDecidable (a ∈ s)) = (fun a => dP a) where [dP : DecidablePred (· ∈ s)] but its still not working

[zbatt]

nvm I'm wrong, that was the issue

[zbatt]

in any case this solves it lol

[zbatt]

theorem Subtype.orderIsoOfNat_apply {n : ℕ} : Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by
  simp [Subtype.orderIsoOfNat]
  suffices (fun a => Classical.propDecidable (a ∈ s)) =  (fun a => dP a) by
    rw [this]
  simp [eq_iff_true_of_subsingleton]