proposition: Theorem demo_eval s b c : (s, b) \in val c -> eval (interp (s, b)) c.
proof: Proof. Proof with discharge_with ssrlia using cnf_S. move: s b c. apply: (nat_size_ind (f := sizef)) => s IH b. case: s b IH => [|x|s t|p s] [|] IH c; try by rewrite /= ?(LCF (ssvalP c)); auto. - move => /= nx. rewrite /Mlabel. case: (LCF (ssvalP c)) => /= _ H px. move: (H x). by rewrite px nx. - case/hint_imp_pos ; first by case: c => C; exact: demoD0. move/IH => //=... tauto. move/IH => /=... by auto. - case/hint_imp_neg; first by case: c => C; exact: demoD0. move/IH => /=... move => Hs /IH => /=... by auto. - move => H d cRd. apply: (IH s _ true) => /=; first by ssrlia. apply: model_reach_pos cRd => // t e A. apply: IH => //=. by ssrlia. - move => inC /=. apply: ex_not_not_all. have /hasP CD: [some D in S , reach_demo S p (val c) D && (s^- \in D)] by apply: (demoD1 (ssvalP c)). case: CD => D DinS /andP [cRD inD]. exists (SeqSub D DinS). case/(_ _)/Wrap. + apply: demo2reach => // t e A. apply IH => //; by ssrlia. + rewrite -/(not _). apply: (IH s _ false) => //=. by ssrlia. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CPDL(PDL_def)