Conditional instance of a type class

Stream: new members

[Elias Castegren]

I have a structure with a well-formedness definition that requires a relation derived from that structure to be a partial order. I saw that there is an IsPartialOrder which seems to be the type class for partial orders. What I would like to do is something like the following:

def thing_wf (t : Thing) : Prop :=
  IsPartialOrder Nat (derived_relation t)

but when I try to prove that a particular instance of Thing is well-formed I can't seem to deconstruct the IsPartialOrder in my goal. My guess is that this is because it is a type class and not just a structure containing the laws required of a partial order, but maybe I am missing some tactic? My current workaround is just defining my own is_partial_order but it would feel better to reuse what is in the standard library (or Mathlib). Maybe there is another definition I should be using?

Minimal example:

inductive Thing where
| mk : (a : Nat) → Thing

def derived_relation (t : Thing) : Nat -> Nat → Prop :=
  match t with
  | Thing.mk a => fun x y => x = a ∧ y = a

def thing_wf (t : Thing) : Prop :=
  IsPartialOrder Nat (derived_relation t)

example : thing_wf (Thing.mk 0) :=
  by
    simp [thing_wf, derived_relation]
    show IsPartialOrder Nat (fun x y => x = 0 ∧ y = 0)
    -- constructor?
    -- apply IsPartialOrder.mk?

[Sebastian Miele]

I do not know enough about Mathlib or Lean to know how it usually would be done. But the following works and should give enough hints about how such can be accomplished in general:

import Mathlib.Order.Defs.Unbundled

inductive Thing where
| mk : (a : Nat) → Thing

def derived_relation (t : Thing) : Nat -> Nat → Prop :=
  match t with
  | Thing.mk a => fun x y => x = a ∧ y = a

abbrev thing_wf (t : Thing) : Prop :=
  IsPartialOrder Nat (derived_relation t)

instance : thing_wf (Thing.mk 0) where
  refl := sorry
  trans := sorry
  antisymm := sorry

#synth IsPartialOrder Nat (derived_relation ⟨0⟩)
#synth thing_wf ⟨0⟩

example : thing_wf (Thing.mk 0) := inferInstance
example : thing_wf (Thing.mk 0) where

Note that thing_wf now is an abbrev which makes it transparent for the synthesis of typeclass instances.

Just

example : thing_wf (Thing.mk 0) where
  refl := sorry
  trans := sorry
  antisymm := sorry

instead of instance: thing_wf ... is possible, too.

[Elias Castegren]

Thanks, this works for concrete instances (which is what I did ask about), but in practice I'm going to have a theorem like \all t t', thing_wf t -> thing_eval t t' -> thing_wf t', so it's not a single instance but a procedure for generating such instances I guess. But this gives me a good start, thanks again!