Stream: Beginner Questions

Topic: Why sledgehammer refuses to give me this?

Yiming Xu (Feb 08 2025 at 18:39):

I want to prove:

proof (prove)
using this:
u = ul ! j
(u, u') ∈ set (zip ul ul')
j < length ul
length ul = length ul'

goal (1 subgoal):

1. u' = ul' ! j

sledgehammer gives nothing, which is surprising. What is wrong here?

Yiming Xu (Feb 08 2025 at 19:19):

I think I see what is wrong. All my bad! Never minds.

Mathias Fleury (Feb 08 2025 at 20:35):

ul = replicate 250 1
ul' = [0..<250]
u = 1
j=1

Mathias Fleury (Feb 08 2025 at 20:35):

u' = 249

Mathias Fleury (Feb 08 2025 at 20:36):

lemma
  assumes "u = ul ! j"
assumes "(u, u') ∈ set (zip ul ul')"
assumes "j < length ul"
assumes "length ul = length ul'"
shows "u' = ul' ! j"
nitpick
(*
Nitpicking formula...
Nitpick found a counterexample for card 'a = 3 and card 'b = 3:
  Free variables:
    j = 0
    u = a⇩1
    u' = b⇩1
    ul = [a⇩1, a⇩1]
    ul' = [b⇩2, b⇩1]
*)

Mathias Fleury (Feb 08 2025 at 20:38):

with distinct it works

lemma
  assumes "u = ul ! j" "distinct ul"
assumes "(u, u') ∈ set (zip ul ul')"
assumes "j < length ul"
assumes "length ul = length ul'"
shows "u' = ul' ! j"
  using assms
  apply auto
  (*thank you sledgehammer*)
  by (smt (verit) Pair_inject in_set_conv_nth length_zip min.idem nth_eq_iff_index_eq nth_zip)

Yiming Xu (Feb 08 2025 at 21:07):

Thanks! Eventually I remember to use nitpick for the thing that confuses me...

Mathias Fleury (Feb 08 2025 at 21:08):

For simple list theorems, I always assume that sledgehammer will either prove it or the theorem is incorrect

Yiming Xu (Feb 08 2025 at 21:13):

So the important question is what is a "simple list theorem..."

Mathias Fleury (Feb 08 2025 at 21:13):

everything that does only involves list operator from HOL.List or your own definitions

Mathias Fleury (Feb 08 2025 at 21:13):

(HOL.List is nearly all useful functions)

Yiming Xu (Feb 08 2025 at 21:14):

I see. I should not under estimate sledgehammer.

Mathias Fleury (Feb 08 2025 at 21:19):

It is more: you should not underestimate the amount of hours users have put into writing all the useful theorems

Yiming Xu (Feb 08 2025 at 21:20):

Surely I am not. But I fail to find useful thms on iterated zips... I hope it just indicates I should not ever need them...

Last updated: Mar 09 2025 at 12:28 UTC