Zulip Chat Archive

Stream: general

Topic: semantics of description logics: binary representation of...


view this post on Zulip Yakov Pechersky (Feb 10 2021 at 17:22):

Imagine having to prove that 35 \ne 31, you'd have to undo 30 succ to show that these terms are not the same.

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:26):

Nice! I got it @Yakov Pechersky ... So bit0 is define for all types instances of has_add. bit0 is the double of a value. the name bit0 is not obvious.

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 17:27):

This is implicit in what others have said above but I didn't see it stated explicitly in this thread: numerals like 4 in Lean are just notation for things built out of bit0 and bit1 from 0 and 1 (which Lean gets from the has_zero and has_one typeclasses):

set_option pp.numerals false
#check 4 -- bit0 (bit0 has_one.one) : ℕ

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 17:27):

I think of it is 4 is 100 in binary, so read right to left, it is bit0 (bit0 1)

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:28):

The point is that if you have a term written with bit0 and bit1, like bit1 $ bit0 $ bit1 $ bit0 $ bit0 1 then when you read it backwards you get the binary representation of the value, in this case 0b100101

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:29):

Mario Carneiro said:

Yes you can prove it directly using nat.one_ne_bit0 but that's just what norm_num uses under the hood, users shouldn't need to interact with numerals on this level of abstraction

That was my point above. The level of abstraction is important. It doesn't make sense having to deal with bit representation to prove that 1=4 is false. What about finish. Does it calls norm_num? Or I should really use norm_num?

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 17:29):

Now, what's brutal is that the default cast in Lean of anything that has addition to nat is unary! There is a better nat.bin_cast. But unless the thing you're adding has nice properties (add_monoid or a subset of them depending on what you're adding), it's not provable that nat.cast x = nat.bin_cast x

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:30):

That doesn't really matter though unless you use #eval on nat.cast

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:31):

You can prove (nat.cast 37 : real) = 37 in log n theorem applications

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 17:31):

Mario Carneiro said:

That doesn't really matter though unless you use #eval on nat.cast

https://github.com/leanprover-community/mathlib/pull/5462#discussion_r553226279

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 17:31):

Which is a form of evaluation of nat.cast.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:31):

yes, like I said

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:31):

don't evaluate nat.cast in the VM

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:31):

but you can use it to prove things

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:33):

In the PR you linked though, you are parsing decimal strings, so the obvious approach would be to look for 0-9 and evaluate 10*n+a for each digit

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:37):

Bryan Gin-ge Chen said:

This is implicit in what others have said above but I didn't see it stated explicitly in this thread: numerals like 4 in Lean are just notation for things built out of bit0 and bit1 from 0 and 1 (which Lean gets from the has_zero and has_one typeclasses):

set_option pp.numerals false
#check 4 -- bit0 (bit0 has_one.one) : ℕ

I see now, but they are not defined over 1 and 0 only, which was my initial difficulty. bit0 1 reduces to 2 and reduce bit0 2 reduces to 4, certainly because 2 first reduces to bit0 1 then bit0 2 is bit0 $ bit0 1..

BTW, in Emacs and Lean 3 (last version). The option you gave me shows nat.zero.succ.succ for bit0 1.

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:49):

Mario Carneiro said:

Actually, looking at your definitions, it seems like this result is correct: Every hasChild man seems to mean the collection of all people such that every child of theirs is a man, and since the men are 2,4, the women are 1,3 and 2 is a child of 1 and 3 a child of 4, the only person for which the predicate fails is 4 (all the nonbinaries at >4 have no children so the concept is also satisfied for them)

Hi @Mario Carneiro , Indeed, this is the right interpretation of description logic. At the end of my file, I point to https://arxiv.org/pdf/1201.4089v3.pdf, a good introduction to the language. Basically, the interpretation of forall R.C means {x | all I(R)-successors of x are in I(C)}. I believe my formalization capture this in https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L53-L54. But I may be missing something in the translations of sets to propositions.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:50):

So then the only problem was in your statement of the theorem: that example doesn't evaluate to {1}, it evaluates to {4}^c

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:52):

No, the only one that has ALL fillers of type Man is {1}

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:52):

That's not true though

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:52):

2 also has that property, because 2 has no children

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:53):

see also https://en.wikipedia.org/wiki/Vacuous_truth

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:53):

Oh.. you are right. I got it.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 17:55):

You should try replacing Every with Some and prove that it evaluates to {1}

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 17:56):

So Every hasChild Man should evaluate to {1,2,3}. sorry, as you said above, the complement of {4}.

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 18:08):

Thank you @Mario Carneiro , that was so obvious that I am embarrassed!

example :
 interp i (Some (Role.Atomic ar.hasChild) (Concept.Atomic ac.man)) = ({1} : set ) :=
begin
 ext n,
 apply iff.intro,
 { intro h1,
   dsimp [interp,r_interp,i] at h1,
   rw [ic,ir] at h1,
   simp at *,
   apply (exists.elim h1),
   simp, intros a h,
   finish,
 },

 { intros h1,
   dsimp [interp,r_interp,i],
   rw [ic,ir],
   norm_num at h1,
   rw h1,
   apply exists.intro 2,
   finish,
 }
end

view this post on Zulip Mario Carneiro (Feb 10 2021 at 18:09):

you should start the proof off with simp [interp, r_interp, ir], like I did, it makes the rest of the proof a lot easier

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 18:23):

Thank you, yes, it makes sense. The finish in the first branch is doing a lot of work (i saw with show_term{ finish }). I am always curious about how to the steps explicit.

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 21:10):

Hi @Mario Carneiro , your proof above didn't work for me. I need to change the first branch to

{ rintro h,
    have h2 := h (3 : ),
    revert h2,
    finish,
  }

The second branch uses rintro, creating the goals with terms like (1.add 0).succ. I can't even reduce these terms with #reduce...

2 goals
h : 1  {4},
 : (1, (1.add 0).succ) = (1, 2)
 (1.add 0).succ  {2, 4}

h : (2.add (1.add 0)).succ  {4},
 : ((2.add (1.add 0)).succ, (2.add 0).succ)  {(4, 3)}
 (2.add 0).succ  {2, 4}

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:12):

You used this proof exactly as written?

example :
  interp i (Every (Role.Atomic ar.hasChild) (Concept.Atomic ac.man)) = ({4} : set ) :=
begin
  ext n,
  simp [interp, r_interp, ir],
  split,
  { rintro H rfl,
    have := H 3, revert this,
    norm_num },
  { rintro h _ (⟨rfl, rfl|rfl, rfl⟩), {norm_num},
    cases h rfl },
end

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:12):

The goals shouldn't look anything like that

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:13):

What does your version look like

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 21:17):

I am getting the error in H 3 with 3 in red underline.

failed to synthesize type class instance for
H :  (b : i.δ), (4, b)  i.atom_R ar.hasChild  b  i.atom_C ac.man
 has_one i.δ
state:
H :  (b : i.δ), (4, b)  i.atom_R ar.hasChild  b  i.atom_C ac.man
 false

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:19):

Ah, it's probably because you removed the @[reducible] on i

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:21):

Here's a version that works even if i is not reducible

example :
  interp i (Every (Role.Atomic ar.hasChild) (Concept.Atomic ac.man)) = ({4} : set ) :=
begin
  dsimp [i, interp],
  ext n,
  simp [r_interp, ir],
  split,
  { rintro H rfl,
    have := H 3, revert this,
    norm_num },
  { rintro h _ (⟨rfl, rfl|rfl, rfl⟩), {norm_num},
    cases h rfl },
end

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 21:50):

thank you. yes I have removed the @[reducible]! It is all clear now.


Last updated: May 13 2021 at 06:15 UTC