# Zulip Chat Archive

## 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⟩
```

#### Kevin Buzzard (Feb 17 2021 at 23:46):

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