Yiming Xu (Oct 14 2024 at 06:50): Yiming Xu (Oct 14 2024 at 06:50):I want to prove a termination, and Isabelle wants me to do it by hand, I got the following goal after "apply auto"
1. length x = length fl ⟹ R m (w # x) ⟹ size (fl ! xa) < Suc (size_list size fl)
The lemma "size_list_estimation" seems to be helpful
?x ∈ list.set ?xs ⟹ ?y < ?f ?x ⟹ ?y < size_list ?f ?xs
I typed sledgehammer(size_list_estimation) and it does not find any proof. It should be straightforward. How do people usually do with this (it seems to me that such a pattern is quite typical)?
Mathias Fleury (Oct 14 2024 at 06:57):You probably want sledgehammer(add: size_list_estimation)
Mathias Fleury (Oct 14 2024 at 06:57):otherwise you are asking Sledgehammer to find a proof with only that theorem
Mathias Fleury (Oct 14 2024 at 06:58):But the general solution is to... write a proof by hand
Yiming Xu (Oct 14 2024 at 06:59):Thanks a lot! Yes I was wrong with that. I tried and it still does not give me a proof. Maybe it does require me to write it out.
Mathias Fleury (Oct 14 2024 at 06:59):to prove termination you can open a proof block
Yiming Xu (Oct 14 2024 at 06:59):termination proof (relation "measure (λ(a,b,c,d) ⇒ size d)", goal_cases)
case 1
then show ?case by auto
next
case (2 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (3 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (4 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (5 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (6 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (7 τ Φ W R V w f1 f2)
then show ?case by auto
next
case (8 τ Φ W R V w f)
then show ?case by auto
next
case (9 τ Φ W R V w m fl x xa)
find_theorems size_list
then show ?case apply auto sledgehammer(add: size_list_estimation)
next
case (10 τ Φ W R V w m fl x z yb)
then show ?case sorry
qed
That is what I am currently writing. I am try to fill the sorries now. I would appreciate if you remind me about something that already looks bad in that proof!
Yiming Xu (Oct 14 2024 at 07:06):Oh what is wrong is that the goal is bad.
Yiming Xu (Oct 14 2024 at 07:06):It is not the goal I expected.
The corresponding clause is:
"satis (τ,Φ) (W,R,V) w (BOX m fl) ⟷
(m ∈ fst τ ∧ (snd τ) m = length fl ∧
w ∈ W ∧ (∀vl. length vl = length fl ∧ R m (w # vl) ⟶
(∃i. i < length vl ∧
satis (τ,Φ) (W,R,V) (vl ! i) (fl ! i))))"
I have the assumption that i < length vl.
Yiming Xu (Oct 14 2024 at 07:07):But in the goal, it asks me to prove
⋀τ Φ W R V w m fl x xa.
length x = length fl ∧ R m (w # x) ⟹
(((τ, Φ), (W, R, V), x ! xa, fl ! xa), (τ, Φ), (W, R, V), w, □m fl) ∈ measure (λx. case x of (a, b, c, d) ⇒ size d)
There is no assumption on xa saying that xa < length fl or xa < length vl.
Yiming Xu (Oct 14 2024 at 07:09):Why does Isabelle refuse to give me such an assumption, and how should I get it? Yesterday Yong Kiam taught me to make the recursion on list more obvious to Isabelle. But here I am overwhelm about what to try.
Yiming Xu (Oct 14 2024 at 07:12):I expect if we have something called "list.exists", means exists a list member that does something, that might help. But I did not find one.
Last updated: Oct 31 2025 at 08:28 UTC