reasoning with strings

Stream: general

[Alexandre Rademaker]

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]

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]

h1 before that goal looks like it could provide b ∈ ∅ which is false, so it may be provable after all.

[Alexandre Rademaker]

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]

Your second question can be answered with show_term:

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

Also, #mwe?

[Mario Carneiro]

oh there's a link at the end

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

Why's that?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Gabriel Ebner]

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]

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

[Eric Wieser]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

actually bit0 (bit0 1)