How to define CCPO with module system enabled?

Stream: general

[Michael Sammler]

I defined a CCPO for a custom type and I am trying to port the code to use the module system. However, this does not work at the moment since is_sup and chain are not exposed and I don't see any lemmas for them. The following code illustrates the problem. Is there a way to define a custom CCPO with the module system enabled?

module

import Lean
open Lean.Order

def MyType : Type := sorry

instance : PartialOrder MyType where
  rel := sorry
  rel_refl := sorry
  rel_trans := sorry
  rel_antisymm := sorry


/--
error: Tactic `unfold` failed to unfold `is_sup` in
  is_sup c ?w
-/
#guard_msgs in
instance : CCPO MyType where
  has_csup := by
    intros c hc
    constructor
    -- how to proceed? the following fails
    unfold is_sup

/--
error: Tactic `unfold` failed to unfold `chain` in
  chain c
-/
#guard_msgs in
instance : CCPO MyType where
  has_csup := by
    intros c hc
   -- how to use hc? the following fails
    unfold chain at hc

[Kim Morrison]

@Sebastian Graf, I think this question is for you!

[Sebastian Graf]

I think @Sebastian Ullrich is in a better position to answer :)

[Sebastian Ullrich]

I think it would be up to @Joachim Breitner to make that call for his API! But given the simplicity of the definitions, I don't see a reason not to.

[Robin Arnez]

Yeah, you could just import all Init.Internal.Order.Basic in the meantime but @[expose]ing the relevant definitions would probably also be a good idea

[Joachim Breitner]

Thanks for being “early adoptor” for defining your own CCPO.

Just to confirm: @Michael Sammler , you are instantiating this type class for the purpose of partial_fixpoint, and not because you want to do general domain theory, right?

But yes, I admit I didn't think about this use case too much when writing the file. Anyone here interested in writing a PR to identify and expose the relevant bits? (there is also a test or two in the lean repo instantiating CCPO, so maybe make that a module as part of the PR)

[Michael Sammler]

Thank you all for the quick responses!

Joachim Breitner said:

Just to confirm: Michael Sammler , you are instantiating this type class for the purpose of partial_fixpoint, and not because you want to do general domain theory, right?

Yes. I have a custom library for co-inductive types in Lean and by defining a custom CCPO instance one can write recursive definitions of these co-inductive types in a very nice way. I think partial_fixpoint is a really cool feature of Lean and it would be sad to lose it by the switch to the module system.

Joachim Breitner said:

But yes, I admit I didn't think about this use case too much when writing the file. Anyone here interested in writing a PR to identify and expose the relevant bits? (there is also a test or two in the lean repo instantiating CCPO, so maybe make that a module as part of the PR)

If nobody beats me to it, I would be happy to create this PR.

[Joachim Breitner]

Thanks! Ping me on it and I’ll review it.

[Michael Sammler]

Done in https://github.com/leanprover/lean4/pull/12311