proposition: Lemma invariant_update p z st g : invariant st g -> in_state p z st -> invariant (update_anti_literals p z (rm_state p st)) (update p z g).
proof: Proof. move=> [Hs Hpos Hanti Hi [His1 His2]] Hin. case: (Hpos)=> _ _ /(_ _ _ Hin) => Hz. case: (Hpos) => _ /(_ _ (in_state_spos Hin)) => Hp. split. - by rewrite size_update. - by apply: valid_state_update_anti_literals. - move=> p1 Bp1. rewrite (perm_mem (perm_spos_update_anti_literals _ _ _)). rewrite spos_rm_state. case: (p1 =P p) => /= [->|/eqP p1Dp]. by rewrite update_get. by rewrite update_diff_get // Hanti. move=> p1 p2. case: (p1 =P p) => [->|/eqP p1Dp]; case: (p2 =P p) => [->|/eqP p2Dp] Hp1 Hp2. - by rewrite !update_get // notin_anti_literals. - rewrite update_get // update_diff_get //. by move=> Hx Hg2; rewrite His1. - rewrite update_get // update_diff_get //. move=> Hg1 _; apply: anti_literals_nswap => //. by apply: His1. by rewrite !update_diff_get //; apply: Hi. split. move=> p1 p2 z1. rewrite in_state_update_anti; last first. by have [] := valid_state_rm_state p Hpos. case: (p2 =P p) => [->|/eqP p2Dp]. rewrite update_get //. by move=> Hp1 Hp2 _ _ /andP[Hna _]. move=> Hp1 Hp2 Hz1. rewrite update_diff_get // => Hg2 /andP[H1 H2]. apply: His1 => //. by apply: in_state_rm H2. move=> p1 z1 Hp1 Hz1. case: (p1 =P p) => [->|/eqP p1Dp]. by rewrite update_get // Hz. rewrite update_diff_get //. rewrite in_state_update_anti; last first. by have [] := valid_state_rm_state p Hpos. rewrite negb_and negbK => Hg1 /orP[Han|HNi]; last first. case: (His2 p1 z1) => //. by apply: notin_state_rm HNi. move=> p2 [H1p2 H2p2 H3p2]. have p2Dp : p2 != p. apply/eqP=> p2Ep. have : p \in spos st by apply: in_state_spos Hin. have := (Hanti p Hp). by rewrite -p2Ep H2p2; case: (_ \in _). by exists p2; rewrite update_diff_get. by exists p; rewrite update_get. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)