Zulip Chat Archive

Stream: general

Topic: non empty set in a structure


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

view this post on Zulip Mario Carneiro (Feb 17 2021 at 22:05):

Are you saying that every concept is a nonempty set?

view this post on Zulip Mario Carneiro (Feb 17 2021 at 22:05):

Or only that the universe delta is nonempty

view this post on Zulip Mario Carneiro (Feb 17 2021 at 22:06):

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

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

view this post on Zulip Yakov Pechersky (Feb 17 2021 at 23:41):

example : nonempty  := 0

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 23:46):

you misspelt 37

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

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

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

view this post on Zulip Alexandre Rademaker (Feb 18 2021 at 02:09):

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

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

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

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

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

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