Zulip Chat Archive

Stream: mathlib4

Topic: Port Order/OrderIsoNat


zbatt (Jan 21 2023 at 22:25):

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 (Jan 21 2023 at 23:46):

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

zbatt (Jan 22 2023 at 00:10):

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

Kevin Buzzard (Jan 22 2023 at 00:13):

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 (Jan 22 2023 at 00:28):

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 (Jan 22 2023 at 00:28):

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

James Gallicchio (Jan 22 2023 at 12:48):

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

zbatt (Jan 22 2023 at 13:28):

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 (Jan 22 2023 at 13:38):

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 (Jan 22 2023 at 13:39):

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 (Jan 22 2023 at 13:58):

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

James Gallicchio (Jan 22 2023 at 14:01):

Oh, I see what you mean o.O weird

James Gallicchio (Jan 22 2023 at 14:02):

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 (Jan 22 2023 at 14:03):

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

James Gallicchio (Jan 22 2023 at 14:04):

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

zbatt (Jan 22 2023 at 14:05):

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 (Jan 22 2023 at 14:08):

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

zbatt (Jan 22 2023 at 14:11):

(deleted)

zbatt (Jan 22 2023 at 17:16):

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 (Jan 22 2023 at 17:17):

nvm I'm wrong, that was the issue

zbatt (Jan 22 2023 at 17:17):

in any case this solves it lol

zbatt (Jan 22 2023 at 17:18):

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]

Last updated: Dec 20 2023 at 11:08 UTC