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: Dec 20 2023 at 11:08 UTC