Zulip Chat Archive

Stream: new members

Topic: Question about instance, notation and pattern matching


view this post on Zulip 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?).

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:25):

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

view this post on Zulip 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?

view this post on Zulip Joao Bregunci (Feb 24 2021 at 16:24):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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