Constructor distintion

Stream: new members

[lorã]

Hi, this is my first post here :P. So i where trying to do this

namespace MyList

inductive Nat : Type
  | O : Nat
  | S : Nat → Nat

open Nat

inductive List (α : Type) : Type
  | Nil  : List α
  | Cons : α → List α → List α
  deriving Repr

open List

def take {α : Type} : Nat → List α → List α
  | _, Nil              => Nil
  | O, _                => Nil
  | S n, Cons x xs => Cons x (take n xs)

def drop {α : Type} : Nat → List α → List α
  | _, Nil           => Nil
  | O, xs            => xs
  | S n, Cons _ xs => drop n xs

#check id

def concat : List α → List α → List α
  | Nil, ys    => ys
  | Cons x xs, ys => Cons x (concat xs ys)

#eval concat (Cons 3 Nil) (Cons 1 (Cons 2 Nil))

theorem concat_take_drop {α : Type} : ∀(xs : List α), ∀(n : Nat),
  concat (take n xs) (drop n xs) = xs :=
by
  intro xs
  induction xs with
  | Nil =>
    intro n
    rw [take]
    rw [drop]
    rw [concat]

  | Cons k ks HI =>
      intro n
      match n with
      | O =>
        rw [take]
        rw [drop]
        rw [concat]
        PROBLEM
       ...

But instead of solve, my goal became ⊢ Cons k ks = Nil → False, what doesnt make so much sense for me rn... have i did something wrong? How do i solve it? My constructors are diferents, wheres the problem?

[Kyle Miller]

That's fine. You can probably do simp here. The simp tactic knows about constructors being distinct.

If you want to do it slightly more manually, you can do intro h followed by cases h. The cases tactic can reason about distinct constructors too.

[Kyle Miller]

The goal Cons k ks = Nil → False can be read as "an impossible situation implies a contradiction." If you use one of these tactics to prove the impossible situation cannot happen, then you're good.

[lorã]

If you want to do it slightly more manually, you can do intro h followed by cases h. The cases tactic can reason about distinct constructors too.

Yeah, and thats the main problem here. The intro h followed by cases h didnt work and i cant use simp because it's considered a bit cheating by my professor

[lorã]

The goal Cons k ks = Nil → False can be read as "an impossible situation implies a contradiction." If you use one of these tactics to prove the impossible situation cannot happen, then you're good.

Thats so weird, btw

[Edward van de Meent]

From reading the new language reference, i think what you need is List.NoConfusion or something like that (i dont remember the exact name)

[Edward van de Meent]

This gets automatically generated for non-Prop inductives

[Edward van de Meent]

And it allows you to prove that indeed, different constructors give different values

[Edward van de Meent]

See this reference

[Kyle Miller]

Thats so weird, btw

Mathematics uses material implication: https://en.wikipedia.org/wiki/Material_implication_(rule_of_inference)

The statement p -> q is true if p is false.

[Kyle Miller]

draell said:

The intro h followed by cases h didnt work

Works for me:

theorem concat_take_drop {α : Type} : ∀(xs : List α), ∀(n : Nat),
  concat (take n xs) (drop n xs) = xs :=
by
  intro xs
  induction xs with
  | Nil =>
    intro n
    rw [take]
    rw [drop]
    rw [concat]

  | Cons k ks HI =>
      intro n
      match n with
      | O =>
        rw [take]
        rw [drop]
        rw [concat]
        intro h
        cases h
        intro h
        cases h
       | S _ => sorry

[lorã]

```
intro h
cases h
intro h
cases h

thats sooooooooooo weird o.O

[Kyle Miller]

The same goal appears twice -- is that why you were thinking intro h; cases h didn't work?

[lorã]

The same goal appears twice -- is that why you were thinking intro h; cases h didn't work?

Yes, thats not what was happening? (im not very good at eng, but for me it phrase sounds a bit grouss, but i dont really know how to improve it, so, if i sound rude itsnt intencional, im just bad srry)

[lorã]

Oh, one goal has closed first. I see

[lorã]

the cases doesnt sound a bit weird here?

[Kyle Miller]

Yes, it sounds weird, but it makes sense if you understand that Eq is an inductive type too. It is doing cases on Eq. The only constructor of Eq is Eq.refl, and doing cases h causes Lean to see how Cons k ks = Nil could be constructed by Eq.refl. But, cases can see that this is impossible because Cons and Nil are different constructors.

[lorã]

(deleted)

[lorã]

But, cases can see that this is impossible because Cons and Nil are different constructors.

So it cause to explode?

[Kyle Miller]

Yes (assuming you mean the principal of explosion and not :explosion: or :explosive:)

[Kyle Miller]

Another solution is what Edward was suggesting:

intro h
exact List.noConfusion h

This is what cases does automatically.

[lorã]

But Lean4 will see that it have a habitant of Eq which has not been constructed by any of the only one constructor, so what? I mean: im trying to understand the way trhout that goes

[Kyle Miller]

It's in the process of trying to see how it could be one of the constructors that it uses List.noConfusion and is able to invoke the principal of explosion. The process is called "dependent elimination".

[lorã]

Another solution is what Edward was suggesting:

It goes to "unknown tactic" (i've forgout the exact)

[Kyle Miller]

theorem concat_take_drop {α : Type} : ∀(xs : List α), ∀(n : Nat),
  concat (take n xs) (drop n xs) = xs :=
by
  intro xs
  induction xs with
  | Nil =>
    intro n
    rw [take]
    rw [drop]
    rw [concat]

  | Cons k ks HI =>
      intro n
      match n with
      | O =>
        rw [take]
        rw [drop]
        rw [concat]
        intro h
        exact List.noConfusion h
        intro h
        exact List.noConfusion h
       | S _ => sorry

[Kyle Miller]

Or for short

      match n with
      | O =>
        rw [take]
        rw [drop]
        rw [concat]
        exact List.noConfusion
        exact List.noConfusion
       | S _ => sorry

[Kyle Miller]

In case it's educational, a while back I worked through how Nat.noConfusion works and simplified it: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20noConfusion.20in.20apply/near/437151497

[Kyle Miller]

There's an example of Nat.zero = Nat.succ n -> False being proven using it.

[Edward van de Meent]

Reading that conversation, apparently simply contradiction also works if this hypothesis is in context?

[Kyle Miller]

Of course it depends on what your definition of "simple" is. One of the many steps of the contradiction tactic is to look for an equality hypothesis with different constructors on each side and apply noConfusion.

[Kyle Miller]

https://github.com/leanprover/lean4/blob/1315266dd3faeaf28d1263668cb88f2f3f5e530c/src/Lean/Meta/Tactic/Contradiction.lean#L172-L178

[Edward van de Meent]

In this case, using contradiction appeals to me because it clearly announces what our reasoning would be, while still being 'general' enough that it doesn't go into internals.

[Kyle Miller]

That's fair, but the word "simply" (like "just") is one that easily hides away important details, like what criteria you are evaluating it with. I like simp for this myself, since it can already handle this reasoning, but in this thread draell already mentioned that their professor calls it "cheating".

[Edward van de Meent]

Yea, that makes sense