non empty set in a structure

Stream: general

[Alexandre Rademaker]

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]

Are you saying that every concept is a nonempty set?

[Mario Carneiro]

Or only that the universe delta is nonempty

[Mario Carneiro]

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

[Alexandre Rademaker]

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]

example : nonempty ℕ := ⟨0⟩

[Kevin Buzzard]

you misspelt 37

[Mario Carneiro]

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]

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]

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]

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

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

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

[Yakov Pechersky]

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]

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.