解けた！

2020年5月18日 03:27

５月１７日日曜日、晴れ

やった！
ついに「チャレンジ問題：バブルアップ」が証明できたっ！！

そうか〜、そこが足りなかったのか〜！
納得。 pic.twitter.com/YObjPJ2nyk
— いけべ (@ikb) May 17, 2020

i を挟んで二つの部分ができること。このそれぞれが整列していることを不変条件としていた。だけれどもう一つ、 i を挟んだ前後の関係が必要だった。

ところでこれ、コードを見る限り配列 v の中身が保存されているように見える。しかし事後条件だけを意地悪くみると、例えば v の中身をすべて 0 で書き換えても成立する。

これを防ぐには事前条件は配列 v の 0 番目を除いて整列されていること、事後条件は配列 v 全体を整列したものであることを書けばよさそう。
Isabelle で「整列されていること」を示す述語は、まず間違いなくあるとおもう。これはどうやって探すのだろうかなあ？

＊　＊　＊

夕飯はナスの煮浸し、ポテトフライ、そして牛丼。

煮浸しと牛丼は『白ごはん.com』のレシピを利用。便利ですね、ここ。