proposition: Lemma StateWhile_Realise l : (forall l, pM l ⊨ R l) -> StateWhile l ⊨ StateWhile_Rel l.
proof: Proof. intros HRel. hnf in HRel; hnf. intros t k; revert t l. apply complete_induction with (x := k); clear k; intros k IH. intros tin l c3 HLoop. unfold loopM in HLoop. cbn in *. rewrite lift_init in HLoop. apply StateWhile_split in HLoop as (c2&HLoop). destruct (projT2 (pM l) (cstate c2)) as [l1|l2] eqn:E. - destruct HLoop as (k1&k2&HLoop1&HLoop2&Hk). apply HRel in HLoop1. rewrite E in HLoop1. rewrite <- lift_init in HLoop2. eapply startState_irrelevant in HLoop2. specialize IH with (2 := HLoop2). spec_assert IH by lia. econstructor 1; eauto. - destruct HLoop as (HLoop&->). apply HRel in HLoop. rewrite E in *. constructor 2; auto. cbn. unfold StateWhile_part. cbn. now rewrite E. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts