[isabelle] Proof automation for Types_To_Sets



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.