partial_fixpoint_monotone does not add the lemma to database

Stream: general

[Michael Sammler]

Hi, I am trying to define a CCPO for a custom type, but somehow my monotone lemmas do not get added to the monotonicity database and partial_fixpoint is not able to prove that my functions are monotone. The following code illustrates the problem:

import Lean
open Lean.Order

def MyType : Type := sorry

def myfun : MyType → MyType := sorry

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

instance : CCPO MyType where
  has_csup := sorry

@[partial_fixpoint_monotone]
theorem myfun_mono : monotone myfun := by sorry

def works : MyType := works
partial_fixpoint

set_option trace.Elab.Tactic.monotonicity true in
/--
error: Could not prove 'doesnt_work' to be monotone in its recursive calls:
  Cannot eliminate recursive call `doesnt_work` enclosed in
    myfun doesnt_work

---
trace: [Elab.Tactic.monotonicity] monotonicity at
    ⊢ monotone fun f => myfun f
[Elab.Tactic.monotonicity] Found monoThms: []
-/
#guard_msgs in
def doesnt_work : MyType := myfun doesnt_work
partial_fixpoint

Particularly note the Found monoThms: [] eventhough the matching lemma should be in the database. What is going wrong here?

[Jakub Nowak]

This works

import Lean
open Lean.Order

set_option trace.Elab.Tactic.monotonicity true

def MyType : Type := sorry

def myfun : MyType → MyType := sorry

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

instance : CCPO MyType where
  has_csup := sorry

@[partial_fixpoint_monotone]
theorem myfun_mono : ∀ {α} [PartialOrder α] (f : α → MyType), monotone f → monotone (fun x => myfun (f x)) := by sorry

def works' : MyType := myfun works'
partial_fixpoint

[Michael Sammler]

Thanks! This works indeed!