aux appearing in instance

Stream: new members

[Hannah Fechtner]

Could someone explain (or point me to an explanation) of the role of aux as used in instances?

For example, in List.Lex.isAsymm :

instance isAsymm (r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Lex r) where
  asymm := aux where
    aux
    | _, _, Lex.rel h₁, Lex.rel h₂ => asymm h₁ h₂
    | _, _, Lex.rel h₁, Lex.cons _ => asymm h₁ h₁
    | _, _, Lex.cons _, Lex.rel h₂ => asymm h₂ h₂
    | _, _, Lex.cons h₁, Lex.cons h₂ => aux _ _ h₁ h₂

Context: I am working on an order on lists (the shortlex order, PR#20310), which is similar to List.Lex. I see this showing up in List.Lex and I want to understand it to see if I should use a similar structure for shortlex

Now, playing around with aux, I have the following two ways to prove this theorem:

theorem foo {α : Type*} {r : α → α → Prop} [IsAsymm α r] {a b : List α} (h1 : List.Lex r a b) :
    ¬ List.Lex r b a := sorry

The first uses aux:

theorem foo {α : Type*} {r : α → α → Prop} [IsAsymm α r] {a b : List α} (h1 : List.Lex r a b) :
    ¬ List.Lex r b a := by
  intro h2
  --apply? gives me the below
  exact Lex.isAsymm.aux r a b h1 h2

or I can just use asymm directly:

theorem foo {α : Type*} {r : α → α → Prop} [IsAsymm α r] {a b : List α} (h1 : List.Lex r a b) :
    ¬ List.Lex r b a := by
  intro h2
  exact asymm h1 h2

Or even more simply, I can do this (this part makes sense to me based on the logical definition of asymm; I'm just including it for completeness)

theorem foo {α : Type*} {r : α → α → Prop} [IsAsymm α r] {a b : List α} (h1 : List.Lex r a b) :
    ¬ List.Lex r b a := IsAsymm.asymm a b h1

[Yaël Dillies]

Don't have Lean open right now, but I suspect aux is needed here because it's proved by induction on the lists. The alternative

instance isAsymm (r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Lex r) where
  asymm := fun
    | _, _, Lex.rel h₁, Lex.rel h₂ => asymm h₁ h₂
    | _, _, Lex.rel h₁, Lex.cons _ => asymm h₁ h₁
    | _, _, Lex.cons _, Lex.rel h₂ => asymm h₂ h₂
    | _, _, Lex.cons h₁, Lex.cons h₂ => asymm _ _ h₁ h₂

(hopefully I got the syntax right) shouldn't work because the fourth asymm will look for an instance of IsAsymm (List α) (Lex r) which is not yet available

[Hannah Fechtner]

makes sense, thanks! so just to summarize: it's an alternate way of writing it, instead of explicitly using induction. Is there anything further to it in terms of, say, user usability? at the moment all of my shortlex proofs use induction

[Yaël Dillies]

No, I think it makes no difference to usability, especially because IsAsymm is Prop-valued