【corres_underlying】How to use corres_underlying to prove the correspondence between two whileLoops's nondet_monad?

[noneGMJ]

Dear，

I want to use predicate corres_underlying to prove the correspondence between two whileLoop or two whileLoopE, but I have not found the relevant lemma in the file corresponding_UL.thy. Does it exist in other files? Is there any good way?

Many Thanks
Gao.

[lsf37]

I don't think there is one in the master branch yet, but there is a pull request (#147) that has a commit c02ecd9 which introduces the rule for corres_underlying. You should be able to cherry-pick that commit without the rest of the PR (which isn't finished yet), and use the rule.

[noneGMJ]

Thank you！That's very useful information.

I have another question:
do we have a corres_underlying lemma that can prove the correspondence between monad with exception and monads without exception？To give a less appropriate example:
corres_underlying sr nf nf' r P P' A >>= B and C >>=E D
or
corres_underlying sr nf nf' r P P' do .. od and doE .. odE

Many Thanks
Gao.

[lsf37]

Those two monads generally do not correspond, because they behave differently -- one can return errors and the other not. Usually there is something like a liftE on the error monad side to lift it into the normal nondeterministic state monad. But on the outer level the types should usually agree.

The Query panel in jEdit and the find_theorems command are often fairly useful to find combinations, e.g find_theorems corres_underlying bindE returns some results (but nothing that also mentionsbind).

It is possible for such statements to correspond, if the parts of the error monad can never throw an error, for instance, but in that case it is usually better to use rewriting on the error monad part first to eliminate the error handling. If that is too hard, then such a corres rules could be written, I think, but I'd recommend that only as last resort.

[noneGMJ]

Many Thanks!
I am now trying to write some proofs between normal monads and monads with exceptions.

[noneGMJ]

Now I can use lemma corresponding_whileLoop in the lib/ExtraCorres.thy to prove the correspondence of two WhileLoops without exceptions, which is a huge help for me.
But I did not find a lemma that can prove correspondence between two WhileLoopE with exceptions. Do we have a solution?

Many Thanks!

[lsf37]

We don't have an exception version yet, sorry. You'll have to prove one yourself, but we'd be happy to take a pull request to add it to the library.

[noneGMJ]

Hello, I performed a proof of consistency between whileLoopE based on the corres_whileLoop rule during my study, and the proof code is as follows.

lemma corres_whileLoopE:
 "⟦ ⋀r r' s s'. ⟦(f⊕rrel) r r'; (s, s') ∈ srel; P s; P' s'⟧ ⟹   case r of
        Inl e ⇒  (∃e'. r' = Inl e') |
        Inr a ⇒ (∃a'. r' =  Inr a' ∧  C a s = C' a' s' );
    ⋀r r'. rrel r r'    ⟹ corres_underlying srel False nf' (f⊕rrel) (P and C r) (P' and C' r') (B r) (B' r');
    ⋀r. ⦃P and C r⦄ B r ⦃λ_. P⦄;
    ⋀r'. ⦃P' and C' r'⦄ B' r' ⦃λ_. P'⦄;
    rrel r r';
    ⋀r'. no_fail (P' and C' r') (B' r');
    ⋀r' s'. P' s' ⟹ whileLoop_terminatesE C' B' r' s'⟧ ⟹
   corres_underlying srel False nf' (f⊕rrel) P P' (whileLoopE C B r) (whileLoopE C' B' r' )"
  apply (auto simp: whileLoopE_def validE_def)
  apply (rule corres_whileLoop)
  subgoal for ra r'a s s' 
    apply(case_tac ra)  apply auto[1]
    apply(case_tac r'a) apply auto[1]
    by (smt old.sum.simps(6)) 
  subgoal for ra r'a  apply(case_tac ra) by auto
  subgoal for ra  apply(case_tac ra) by auto 
  subgoal for r'a
    apply(case_tac r'a) by auto 
    apply simp
   apply (smt no_fail_def old.sum.simps(6) pred_conj_app snd_lift)
  subgoal for r'a s'
    unfolding whileLoop_terminatesE_def 
    apply(case_tac r'a) apply auto
    by (simp add: whileLoop_terminates.intros(1))
  done 

I don't know if you have finished the proof, if not you can see if my proof code is correct, I hope it can provide some help to you.

[lsf37]

Thanks @noneGMJ, it looks like with a bit more fine-tuning we could include that in the library.

[noneGMJ]

Haha ok, I've seen the new whileLoop rules on the rt branch and will make changes to whileLoopE after I finish my graduation design recently.
I also submitted a request #399 for some decomposition rules that I built during my graduation design, it looks relatively simple and I hope it will be of some small help to you.