Solution for Rules.ExamplePrograms.triple_succ_using_incr
intros. applys triple_app_fun. { reflexivity. } simpl.
applys triple_let.
{ apply triple_ref. }
intros r. simpl.
apply triple_hexists. intros p.
apply triple_hpure. intros ->.
applys triple_seq.
{ applys triple_conseq_frame.
{ applys triple_incr. }
{ xsimpl. }
{ xsimpl. } }
applys triple_let.
{ apply triple_get. }
intros x. simpl.
apply triple_hpure. intros ->.
applys triple_seq.
{ applys triple_conseq_frame.
{ applys triple_free. }
{ xsimpl. }
{ xsimpl. } }
applys triple_val.
xsimpl. auto.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
