## Stream: general

### Topic: non empty set in a structure

#### Alexandre Rademaker (Feb 17 2021 at 22:01):

An interpretation in description logics should have a domain as a non-empty set and mappings from atomic symbols to subsets of the domain or subset of the cartesian product of the domain. Using

structure Interpretation (AtomicConcept AtomicRole : Type) :=
mk :: (δ : Type)
(atom_C : AtomicConcept → set δ)
(atom_R : AtomicRole → set (δ × δ))


is not enough, how to make the domain an explicit nonempty set of set δ? The nonempty δ is a proposition, not a type constructor like set...

#### Mario Carneiro (Feb 17 2021 at 22:05):

Are you saying that every concept is a nonempty set?

#### Mario Carneiro (Feb 17 2021 at 22:05):

Or only that the universe delta is nonempty

#### Mario Carneiro (Feb 17 2021 at 22:06):

if the latter, you just need a field (nonemp : nonempty δ) in the structure

#### Alexandre Rademaker (Feb 17 2021 at 23:33):

I see. Now to create a concrete interpretation, I have to provide a proof that NAT is non-empty. With the help of show_term and using norm_num in:

def i := Interpretation.mk ℕ begin show_term { norm_num, } end ic ir


I got a quite unexpected complicated term (id (propext (λ {α : Type} [_inst_1 : inhabited α], iff_true_intro nonempty_of_inhabited))).mpr. Is that the simplest form to proof that NAT is nonempty?

#### Yakov Pechersky (Feb 17 2021 at 23:41):

example : nonempty ℕ := ⟨0⟩


you misspelt 37

#### Mario Carneiro (Feb 17 2021 at 23:53):

MWE:

structure Interpretation (AtomicConcept AtomicRole : Type) :=
(δ : Type)
(nonemp : nonempty δ)
(atom_C : AtomicConcept → set δ)
(atom_R : AtomicRole → set (δ × δ))

def C : Type := sorry
def R : Type := sorry
def ic : C → set ℕ := sorry
def ir : R → set (ℕ × ℕ) := sorry
def i : Interpretation C R := ⟨ℕ, ⟨0⟩, ic, ir⟩


#### Mario Carneiro (Feb 17 2021 at 23:54):

BTW it's generally not recommended to make single letter definitions like this, because they tend to overlap with local variables which leads to confusion

#### Mario Carneiro (Feb 17 2021 at 23:56):

Since nonempty is a typeclass, you can put it in square brackets and then lean will go find the proof that nat is nonempty for you

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

def C : Type := sorry
def R : Type := sorry
def ic : C → set ℕ := sorry
def ir : R → set (ℕ × ℕ) := sorry
def i : Interpretation C R := ⟨ℕ, ic, ir⟩


#### Alexandre Rademaker (Feb 18 2021 at 02:09):

Sorry, I didn't understand the joke about 37!

#### Alexandre Rademaker (Feb 18 2021 at 02:23):

Thank you @Mario Carneiro, I was able to complete the proof. But my first option failed with a mysterious error in the line https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L224

failed to synthesize type class instance for
a b : Type,
C : Concept a b,
i : Interpretation a b,
h : univ = ∅
⊢ nonempty i.δ
state:
a b : Type,
C : Concept a b,
i : Interpretation a b,
h : univ = ∅
⊢ false


Line https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L227 is fine but not explicit. Lines https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L233-L235 may be too explicit. I suspect the necessity of passing the implicit arguments in https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L230 has something to do with the error in line 224.

#### Yakov Pechersky (Feb 18 2021 at 02:25):

For data, make sure you use let or set. have i : Interpretation a b := ... throws the actual data away

#### Alexandre Rademaker (Feb 18 2021 at 02:28):

Wow!! I didn't know that!! Thank you @Yakov Pechersky! Where should I have read about it?

#### Yakov Pechersky (Feb 18 2021 at 02:30):

I don't think the tactic documentation says this explicitly. But have is for Prop and let / set is for things with data content. In your case, you have the structure (data) that you made, and you're trying to get the nonempty record of it.

#### Alexandre Rademaker (Feb 18 2021 at 02:33):

yes yes! I thought that let and have would have the same behavior! Thank you very much. now all my alternatives make much more sense.

Last updated: May 12 2021 at 23:13 UTC