proposition: Lemma try_mono (e1 e2 : ST A) (k1 k2 : A -> ST B) (h1 h2 : exn -> ST B) : e1 <== e2 -> k1 <== k2 -> h1 <== h2 -> (try e1 k1 h1 : ST B) <== try e2 k2 h2.
proof: Proof. move=>[H1 H2] pf2 pf3. have pf: try_pre e2 k2 h2 <== try_pre e1 k1 h1. - move=>h [Vh][Pi] [Hk Hn]. exists Vh, (H1 _ Pi); split. - move=>x m /H2/Hk H'. by case: (pf2 x)=>+ _; apply. move=>ex m /H2/Hn H'. by case: (pf3 ex)=>+ _; apply. exists pf =>i Vi /[dup][[Vi'][Pi'][Pk0 Ph0]] Pi x h. case; case=>[a|e][h0][Ph][Ph'] H. - exists (Val a), h0. move: (H2 i Vi (try_pre_proj Pi))=>H'. rewrite (pf_irr (H1 i (try_pre_proj Pi)) (try_pre_proj (pf i Pi))) in H'. have Ph1 := (H' _ _ Ph); exists Ph1. move: (Pk0 a h0); rewrite (pf_irr Vi' Vi) (pf_irr Pi' (try_pre_proj Pi))=>H''. exists (H'' Ph1); case: (pf2 a)=>Pr; apply. by rewrite (pf_irr (dstr_valid Ph1) (dstr_valid Ph)) (pf_irr (Pr h0 (H'' Ph1)) Ph'). exists (Exn e), h0. move: (H2 i Vi (try_pre_proj Pi))=>H'. rewrite (pf_irr (H1 i (try_pre_proj Pi)) (try_pre_proj (pf i Pi))) in H'. have Ph1 := (H' _ _ Ph); exists Ph1. move: (Ph0 e h0); rewrite (pf_irr Vi' Vi) (pf_irr Pi' (try_pre_proj Pi))=>H''. exists (H'' Ph1); case: (pf3 e)=>Pr; apply. by rewrite (pf_irr (dstr_valid Ph1) (dstr_valid Ph)) (pf_irr (Pr h0 (H'' Ph1)) Ph'). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)