# Zulip Chat Archive

## Stream: general

### Topic: reasoning with strings

#### Alexandre Rademaker (Feb 10 2021 at 13:02):

I can't make progress with the following goals, maybe I am missing something to reason with strings. Any idea?

```
5 goals
n : i.δ,
h1 : ∀ (b : ℕ), (n, b) ∈ ∅ → b ∈ ∅
⊢ n ∈ {1}
n : i.δ,
h1 : ∀ (b : ℕ), (n, b) ∈ ir {id := "hasChild"} → b ∈ ∅
⊢ ¬"hasChild" = "hasChild"
n : i.δ,
h1 : ∀ (b : ℕ), (n, b) ∈ ir {id := "hasChild"} → b ∈ ic {id := "man"}
⊢ ¬"man" = "woman"
n : i.δ,
h1 : ∀ (b : ℕ), (n, b) ∈ ir {id := "hasChild"} → b ∈ ic {id := "man"}
⊢ ¬"man" = "man"a
n : i.δ
⊢ n ∈ {1} → n ∈ interp i (Every (Role.Atomic {id := "hasChild"}) (Atomic {id := "man"}))
```

I am trying to formalize the basic idea of the interpretation of a description logic called ALC. Complete code at https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L100

#### Rob Lewis (Feb 10 2021 at 14:11):

`dec_trivial`

will prove things like `¬"man" = "woman"`

. Unless you're redefined negation, I hope you can't prove `¬"hasChild" = "hasChild"`

!

#### Bryan Gin-ge Chen (Feb 10 2021 at 14:27):

`h1`

before that goal looks like it could provide `b ∈ ∅`

which is false, so it may be provable after all.

#### Alexandre Rademaker (Feb 10 2021 at 15:26):

I changed my code for using inductive types instead of strings. With this new formalization, I made some progress. But I am now in a situation that may suggest the interpretation of concepts should be changed... My current open goal is below. It is clear that for n=1 and b=2, hypothesis h1 is true. I can even instantiate h1 to h2 with the right number. But now I have a true hypothesis that doesn't depend on the `n=1`

...

```
n : ℕ,
h1 : ∀ (b : ℕ), (n, b) ∈ {(1, 2), (4, 3)} → b ∈ {2, 4},
h2 : (n, 2) ∈ {(1, 2), (4, 3)} → 2 ∈ {2, 4}
⊢ n = 1
```

https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L106 is the open goal. Another question is how `finish`

magically solves the goal below in https://github.com/arademaker/alc-lean/blob/master/src/alc.lean#L117

```
n n2 : i.δ,
h1 : n = 1,
hb : 1 = 4 ∧ n2 = 3,
hb1 : 1 = 4
⊢ false
```

#### Eric Wieser (Feb 10 2021 at 15:52):

Your second question can be answered with `show_term`

:

```
example (h : 1 = 4) : false := begin
show_term {finish}
end
```

#### Eric Wieser (Feb 10 2021 at 15:53):

Looking at that messy output, it turns out that `exact nat.one_ne_bit0 _ h`

is the short proof (docs#nat.one_ne_bit0)

#### Alexandre Rademaker (Feb 10 2021 at 16:01):

Thank you @Eric Wieser , but quite unnatural, right?

#### Eric Wieser (Feb 10 2021 at 16:02):

Well, you could also prove it by repeatedly subtracting until you have succ_ne_zero. as:

```
nat.succ_ne_zero _ (nat.succ_injective h).symm
```

I'm not sure what you mean by unnatural.

#### Rob Lewis (Feb 10 2021 at 16:11):

For your first question: `h2`

is trivially true and the goal isn't provable, e.g. evaluate it at `n = 3`

. For your second question: `norm_num at hb1`

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

Also, #mwe?

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

oh there's a link at the end

#### Mario Carneiro (Feb 10 2021 at 16:29):

```
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 16:30):

However this probably isn't the theorem you wanted to prove

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

but I don't know enough about your description logic to suggest fixes

#### Mario Carneiro (Feb 10 2021 at 16:33):

Also you have too many things marked `reducible`

. None of those definitions should be reducible; definitions by pattern matching should never be reducible

#### Eric Wieser (Feb 10 2021 at 16:39):

None of those definitions should be reducible; definitions by pattern matching should never be reducible

Why's that?

#### Mario Carneiro (Feb 10 2021 at 16:39):

Because the only thing it can reduce to is an equation compiler mess

#### Mario Carneiro (Feb 10 2021 at 16:42):

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)

#### Alexandre Rademaker (Feb 10 2021 at 16:46):

Hi @Eric Wieser I don't understand the `bit0`

, I didn't find any documentation about it. Besides that, it seems that the fact that 1=4 is also should not depend on a bit representation of naturals. In other words, the second proof you suggest is entirely in the level of abstraction that I would expect: naturals, successor, the fact that succ is injective etc.

BTW, what is `succ.inj`

in the theorem `succ_injective`

? I didn't find the definition of it (go to definition didn't find it). But yes, thank you so much for helping me to make sense of this (now obvious!) proof:

```
example (h : 1 = 4) : false :=
begin
-- if succ 0 = succ 3 then 0 = 3 because succ is injective
have h1 := (nat.succ_injective h),
apply nat.succ_ne_zero _ h1.symm,
end
```

#### Eric Wieser (Feb 10 2021 at 16:47):

docs#bit0 has a "> equations" toggle you can expand

#### Gabriel Ebner (Feb 10 2021 at 16:48):

Mario Carneiro said:

Because the only thing it can reduce to is an equation compiler mess

Is this really true? I still remember the time when unification produced brec_on, but this has been fixed a long long time ago now.

#### Eric Wieser (Feb 10 2021 at 16:48):

`succ.inj`

is autogenerated - all inductive type constructors are axiomatically injective (I think?)

#### Eric Wieser (Feb 10 2021 at 16:49):

it seems that the fact that 1=4 is also should not depend on a bit representation of naturals.

Lean is proof-irrelevant - facts are never dependent on how you choose to prove them

#### Eric Wieser (Feb 10 2021 at 16:50):

But if you choose to prove equality of naturals using bit0/bit1 instead of zero/succ, you only need `log2 n`

steps instead of `n`

steps to do so

#### Mario Carneiro (Feb 10 2021 at 16:54):

Gabriel Ebner said:

Mario Carneiro said:

Because the only thing it can reduce to is an equation compiler mess

Is this really true? I still remember the time when unification produced brec_on, but this has been fixed a long long time ago now.

Not really, it seems that lean will just ignore the `@[reducible]`

marker in this case instead of providing a brec_on

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

my point is mostly that the annotation does not make any sense

#### Mario Carneiro (Feb 10 2021 at 16:57):

I will reiterate Rob Lewis 's point that the correct way to prove `1 != 4`

is `norm_num`

. it handles all this bit0 stuff for you and doesn't suffer from any exponential time issues like `dec_trivial`

#### Mario Carneiro (Feb 10 2021 at 16:58):

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

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

Eric Wieser said:

But if you choose to prove equality of naturals using bit0/bit1 instead of zero/succ, you only need

`log2 n`

steps instead of`n`

steps to do so

Interesting, I saw the equations, but still, they don't make sense for me. Maybe I am missing the context. How/Why/When they are used.

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

It's expensive to express numerals in a unary system: `4 = 1 + 1 + 1 + 1`

. It is more efficient to say that `4 = bit0 (bit1 0)`

`4 = bit0 (bit0 1)`

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

actually `bit0 (bit0 1)`

Last updated: May 16 2021 at 21:11 UTC