proposition: Lemma eval_reachP (M : fmodel) : ((forall s (w:M), reflect (eval s w) (evalb s w))* (forall p (w v : M), reflect (reach p w v) (reachb p w v)%type)).
proof: Proof. apply: form_prog_rect => [?|? ?|s IHs t IHt w|p IHp s IHs w|? ? ?|p IHp q IHq w v|p IHp q IHq w v|||] /=. - by constructor. - exact: idP. - apply: (iffP implyP); rewrite -(rwP (IHs _)) -(rwP (IHt _)); tauto. - apply: (iffP forall_inP); move => H v /IHp ?; apply/IHs; by auto. - exact: idP. - apply: (iffP orP); rewrite -(rwP (IHp _ _)) -(rwP (IHq _ _)); tauto. - apply: (iffP exists_inP); move => [u ? ?]; exists u; by [apply/IHp|apply/IHq]. - move => p IHp w v. apply: (iffP connectP) => [[ps]|]. + elim: ps w v => //= [? ? _ -> |u us IH w v]; first by constructor. case/andP => /IHp A B ->. apply: StarL A _. exact: IH. + elim => {w v} => [w|w v u A _ [ps B C]]; first by exists [::]. exists (u::ps) => //=. rewrite B andbT. exact/IHp. - move => s IHs w v. apply: (iffP andP); rewrite (rwP eqP) (rwP (IHs _)); tauto. - move => p IHp w v. exact: IHp. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)