## Stream: new members

### Topic: Question about instance, notation and pattern matching

#### Joao Bregunci (Feb 24 2021 at 15:18):

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 (Feb 24 2021 at 15:24):

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

#### Eric Wieser (Feb 24 2021 at 15:25):

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

#### Joao Bregunci (Feb 24 2021 at 15:33):

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 (Feb 24 2021 at 16:24):

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

#### Eric Wieser (Feb 24 2021 at 17:12):

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

#### Alexandre Rademaker (Feb 24 2021 at 20:34):

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 (Feb 24 2021 at 20:39):

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

Last updated: May 11 2021 at 00:31 UTC