Question about instance, notation and pattern matching

Stream: new members

[Joao Bregunci]

My code currenly goes as following

import data.set
open set

/-!
# Goal
We want to proof that the SC defined in the thesis is sound and
complete. In this file, ACL syntax and semantics are defined.
-/

namespace ALC

inductive Role (AtomicRole : Type) : Type
  | Atomic : AtomicRole → Role

inductive Concept (AtomicConcept AtomicRole : Type) : Type
  | TopConcept    : Concept
  | BottomConcept : Concept
  | Atomic        : AtomicConcept → Concept
  | Negation      : Concept → Concept
  | Intersection  : Concept → Concept → Concept
  | Union         : Concept → Concept → Concept
  | Some          : (Role AtomicRole) → Concept → Concept
  | Every         : (Role AtomicRole) → Concept → Concept

open Concept Role

notation        `⊤` := Concept.TopConcept    -- \top
notation        `⊥` := Concept.BottomConcept -- \bot
prefix          `¬ₐ` : 55 := Concept.Negation

--instance concept_has_inf (AtomicConcept AtomicRole : Type) :
-- has_inf (Concept AtomicConcept AtomicRole) := ⟨ Concept.Intersection ⟩
local infix      `⊓` : 55 := Concept.Intersection   -- ◾\sqcap
instance concept_has_sup (AtomicConcept AtomicRole : Type) :
 has_sup (Concept AtomicConcept AtomicRole) := ⟨ Concept.Union ⟩
--local infix      `⊔` : 55 := Concept.Union         -- \sqcup

notation `∃ₐ` R `.ₐ` C := Concept.Some R C -- (it would be nice to use `∃ R. C`)
notation `∀ₐ` R `.ₐ` C := Concept.Every R C -- (it would be nice to use `∀ R. C`)

-- interpretation structure
structure Interpretation (AtomicConcept AtomicRole : Type) :=
mk :: (δ : Type)
      [nonempty : nonempty δ]
      (atom_C   : AtomicConcept → set δ)
      (atom_R   : AtomicRole → set (δ × δ))

variables {AtomicConcept AtomicRole : Type}

-- role interpretation
definition r_interp (I : Interpretation AtomicConcept AtomicRole) : Role AtomicRole → set (I.δ × I.δ)
  | (Role.Atomic R) := I.atom_R R


-- concept interpretation
definition interp (I : Interpretation AtomicConcept AtomicRole) : Concept AtomicConcept AtomicRole → set I.δ
 | ⊤            := univ
 | ⊥            := ∅
 | (Atomic C)   := I.atom_C C
 | (¬ₐ C)       := compl (interp C)
 | (C1 ⊓ C2) := (interp C1) ∩ (interp C2)
 | (Union C1 C2):= (interp C1) ∪ (interp C2)
 | (Some R C)   := { a: I.δ | ∃ b : I.δ,
                     (a, b) ∈ (r_interp I R) ∧ b ∈ (interp C) }
 | (Every R C)  := { a: I.δ | ∀ b : I.δ,
                     (a, b) ∈ (r_interp I R) → b ∈ (interp C) }

My problem is about the following.

--instance concept_has_inf (AtomicConcept AtomicRole : Type) :
-- has_inf (Concept AtomicConcept AtomicRole) := ⟨ Concept.Intersection ⟩
local infix      `⊓` : 55 := Concept.Intersection   -- ◾\sqcap

If I use the local infix there is no problem if I instead try to create a polymorphic instance for the operator ⊓, Lean launches

/-
 failed to prove recursive application is decreasing, well founded relation
   @has_well_founded.r (Concept AtomicConcept AtomicRole)
     (@has_well_founded_of_has_sizeof (Concept AtomicConcept AtomicRole)
        (@Concept.has_sizeof_inst AtomicConcept AtomicRole (default_has_sizeof AtomicConcept)
           (default_has_sizeof AtomicRole)))

There are a few suggestions concerning using_well_founded at the end of my proof, but I didn't understand what this means (am I not simply doing a pattern match?).

[Eric Wieser]

You need attribute [pattern] has_sup.sup has_inf.inf I think, to allow the notation to be used in pattern matching

[Eric Wieser]

You'll probably want to use has_top and has_bot instead of your notation too

[Joao Bregunci]

Perfect, exactly what I needed. Just out of curiosity now. This will apply the attribute for all polymorphic options of my operator, not only for my type Concept? Can I do this only for the Concept case?

[Joao Bregunci]

And thanks, I am also going to use now has_top and has_bot.

[Eric Wieser]

You can use local attribute [pattern] ... to just enable the pattern within your file, otherwise yes it is global

[Alexandre Rademaker]

This attribute [pattern] is only mentioned in https://leanprover.github.io/reference/declarations.html#inductive-types. Where/How can we find more about the attributes defined and their uses?

[Bryan Gin-ge Chen]

We have a page documenting some custom attributes, but it doesn't include many of the attributes defined in core Lean yet.