semantics of description logics: binary representation of...

Stream: general

[Yakov Pechersky]

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

[Alexandre Rademaker]

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.

[Bryan Gin-ge Chen]

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) : ℕ

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

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?

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Which is a form of evaluation of nat.cast.

[Mario Carneiro]

yes, like I said

[Mario Carneiro]

don't evaluate nat.cast in the VM

[Mario Carneiro]

but you can use it to prove things

[Mario Carneiro]

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

[Alexandre Rademaker]

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.

[Alexandre Rademaker]

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.

[Mario Carneiro]

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

[Alexandre Rademaker]

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

[Mario Carneiro]

That's not true though

[Mario Carneiro]

2 also has that property, because 2 has no children

[Mario Carneiro]

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

[Alexandre Rademaker]

Oh.. you are right. I got it.

[Mario Carneiro]

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

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

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.

[Alexandre Rademaker]

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}

[Mario Carneiro]

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

[Mario Carneiro]

The goals shouldn't look anything like that

[Mario Carneiro]

What does your version look like

[Alexandre Rademaker]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

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