# Zulip Chat Archive

## Stream: general

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

#### 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.

#### 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.

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

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

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

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

?

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

#### Mario Carneiro (Feb 10 2021 at 17:30):

That doesn't really matter though unless you use `#eval`

on `nat.cast`

#### Mario Carneiro (Feb 10 2021 at 17:31):

You can prove `(nat.cast 37 : real) = 37`

in log n theorem applications

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

#### Yakov Pechersky (Feb 10 2021 at 17:31):

Which is a form of evaluation of `nat.cast`

.

#### Mario Carneiro (Feb 10 2021 at 17:31):

yes, like I said

#### Mario Carneiro (Feb 10 2021 at 17:31):

don't evaluate `nat.cast`

in the VM

#### Mario Carneiro (Feb 10 2021 at 17:31):

but you can use it to prove things

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

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

.

#### 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.

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

#### Alexandre Rademaker (Feb 10 2021 at 17:52):

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

#### Mario Carneiro (Feb 10 2021 at 17:52):

That's not true though

#### Mario Carneiro (Feb 10 2021 at 17:52):

2 also has that property, because 2 has no children

#### Mario Carneiro (Feb 10 2021 at 17:53):

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

#### Alexandre Rademaker (Feb 10 2021 at 17:53):

Oh.. you are right. I got it.

#### Mario Carneiro (Feb 10 2021 at 17:55):

You should try replacing `Every`

with `Some`

and prove that it evaluates to `{1}`

#### 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}.

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

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

#### 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.

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

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

#### Mario Carneiro (Feb 10 2021 at 21:12):

The goals shouldn't look anything like that

#### Mario Carneiro (Feb 10 2021 at 21:13):

What does your version look like

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

#### Mario Carneiro (Feb 10 2021 at 21:19):

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

on `i`

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

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