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

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