Stream: Beginner Questions

Topic: induction with "obtains"

Artem Khovanov (Aug 31 2022 at 17:26):

I'm having trouble setting up an induction when the goal is an obtains. Here is the simple lemma about lists that I am trying to prove:

theory Untitled-1
imports Main
begin

lemma test:
  assumes "l1 ≠ l2" "length l1 = length l2"
  obtains k where "l1 ! k ≠ l2 ! k" "drop (Suc k) l1 = drop (Suc k) l2"
using assms proof (induction l1 arbitrary: l2)
  case Nil
  thus ?case by simp
next
  case (Cons a l)
  thus ?case sorry
qed

end

The Cons case introduces the following state:

(⋀k. l ! k ≠ ?l2.0 ! k ⟹ drop (Suc k) l = drop (Suc k) ?l2.0 ⟹ thesis) ⟹ l ≠ ?l2.0 ⟹ length l = length ?l2.0 ⟹ thesis
(a # l) ! ?k ≠ l2 ! ?k ⟹ drop (Suc ?k) (a # l) = drop (Suc ?k) l2 ⟹ thesis
a # l ≠ l2
length (a # l) = length l2

The first hypothesis is not a helpful induction hypothesis: I would like something like the following:

l ≠ ?l2.0 ⟹ length l = length ?l2.0 ⟹ (⋀k. l ! k ≠ ?l2.0 ! k ⟹ drop (Suc k) l = drop (Suc k) ?l2.0 ⟹ thesis)

(i.e. I want to conclude existence of such a k by induction, rather than having to prove it from nothing).

When I change to an existential conclusion (shows "∃k. l1 ! k ≠ l2 ! k ∧ drop (Suc k) l1 = drop (Suc k) l2"), the induction is set up correctly (albeit more messily). Am I doing something wrong, or is this a limitation of obtains?

Wenda Li (Sep 01 2022 at 00:35):

Personally, I usually prefer to induct on shows "∃k. l1 ! k ≠ l2 ! k ∧ drop (Suc k) l1 = drop (Suc k) l2" rather than on obtains...

Artem Khovanov (Sep 01 2022 at 00:57):

Yes, this works, but the induction is messier. I was wondering if you can use obtains properly somehow.

Last updated: Apr 26 2024 at 16:20 UTC