Email Gateway (Aug 22 2022 at 14:39): Email Gateway (Aug 22 2022 at 14:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear list, dear Ondrej and Andrei,
I've tried out the new Types_To_Set and I find it very convenient to clean my proofs from
unnecessary invariants. However, I am a bit unsatisfied with the level of proof
automation. In the ITP2016 paper, it says that the transfer "tool is able to perform the
relativization completely automatically". So I was wondering what I am doing wrong.
My typical use case looks like in the following example. Let's define a while loop
operator on subprobability mass functions (import HOL-Probability for this to work) and
prove a lemma about probabilistic termination and parametricity of the constants involved:
locale loop_spmf =
fixes guard :: "'a ⇒ bool"
and body :: "'a ⇒ 'a spmf"
begin
partial_function (spmf) while :: "'a ⇒ 'a spmf" where
"while s = (if guard s then bind_spmf (body s) while else return_spmf s)"
lemma termination_0_1:
assumes p: "⋀s. guard s ⟹ spmf (map_spmf guard (body s)) False ≥ p"
and p_pos: "0 < p"
and lossless: "⋀s. guard s ⟹ lossless_spmf (body s)"
shows "lossless_spmf (while s)"
sorry
end
context includes lifting_syntax begin
lemma lossless_spmf_parametric [transfer_rule]:
"(rel_spmf A ===> op =) lossless_spmf lossless_spmf"
sorry
lemma while_spmf_parametric [transfer_rule]:
"((S ===> op =) ===> (S ===> rel_spmf S) ===> S ===> rel_spmf S)
loop_spmf.while loop_spmf.while"
sorry
end
lemma loop_spmf_while_cong:
"⟦ guard = guard'; ⋀s. guard' s ⟹ body s = body' s ⟧
⟹ loop_spmf.while guard body = loop_spmf.while guard' body'"
sorry
Now, I would like to add an invariant I on the state of the loop in the termination lemma.
At the moment, my proof looks as shown below. I would not call this completely automatic,
so I am wondering what I am doing wrong. Can I improve this somehow?
I use this scheme to add invariants to a bunch of lemmas about loops. At the moment, I
just copy-paste the setup script and have it all over the place. Does anyone have an idea
how to make this more concise and possibly abstract over it?
lemma termination_0_1_invar:
fixes I :: "'s ⇒ bool"
assumes p: "⋀s. ⟦ guard s; I s ⟧ ⟹ spmf (map_spmf guard (body s)) False ≥ p"
and p_pos: "0 < p"
and lossless: "⋀s. ⟦ guard s; I s ⟧ ⟹ lossless_spmf (body s)"
and invar: "⋀s s'. ⟦ s' ∈ set_spmf (body s); I s; guard s ⟧ ⟹ I s'"
and I: "I s"
shows "lossless_spmf (loop_spmf.while guard body s)"
including lifting_syntax
proof -
{ assume "∃(Rep :: 's' ⇒ 's) Abs. type_definition Rep Abs {s. I s}"
then obtain Rep :: "'s' ⇒ 's" and Abs where td: "type_definition Rep Abs {s. I s}"
by blast
then interpret td: type_definition Rep Abs "{s. I s}" .
def cr ≡ "λx y. x = Rep y"
have [transfer_rule]: "bi_unique cr" "right_total cr" using td cr_def
by(rule typedef_bi_unique typedef_right_total)+
have [transfer_domain_rule]: "Domainp cr = I"
using type_definition_Domainp[OF td cr_def] by simp
def guard' ≡ "(Rep ---> id) guard"
have [transfer_rule]: "(cr ===> op =) guard guard'"
by(simp add: rel_fun_def cr_def guard'_def)
def body1 ≡ "λs. if guard s then body s else return_pmf None"
def body1' ≡ "(Rep ---> map_spmf Abs) body1"
have [transfer_rule]: "(cr ===> rel_spmf cr) body1 body1'"
by(auto simp add: rel_fun_def body1'_def body1_def cr_def spmf_rel_map
td.Rep[simplified] invar td.Abs_inverse intro!: rel_spmf_reflI)
def s' ≡ "Abs s"
have [transfer_rule]: "cr s s'" by(simp add: s'_def cr_def I td.Abs_inverse)
have "⋀s. guard' s ⟹ p ≤ spmf (map_spmf guard' (body1' s)) False"
by(transfer fixing: p)(simp add: body1_def p)
moreover note p_pos
moreover have "⋀s. guard' s ⟹ lossless_spmf (body1' s)"
by transfer(simp add: lossless body1_def)
ultimately have "lossless_spmf (loop_spmf.while guard' body1' s')"
by(rule loop_spmf.termination_0_1_immediate)
hence "lossless_spmf (loop_spmf.while guard body1 s)" by transfer }
from this[cancel_type_definition] I show ?thesis by(auto cong: loop_spmf_while_cong)
qed
Thanks,
Andreas
Email Gateway (Aug 22 2022 at 14:46):From: Makarius <makarius@sketis.net>
At ITP / Nancy I have actually encouraged Ondrej and Andrei to put this
experiment into shape for the Isabelle2016-1.
So far the release branch has nothing else than the "initial commit"
https://bitbucket.org/isabelle_project/isabelle-release/commits/ae53f4d901a3
without any official description in NEWS whatsoever.
This is OK, but it should be made clear that it is just a
proof-of-concept that accompanies the very first conference paper
introducing the ideas behind it (I have myself looked at the paper only
for 2h: from 3am to 5am one summer night at Nancy).
Makarius
Last updated: Apr 24 2024 at 08:20 UTC