proposition: Lemma steps_correct: forall i (s: Store) p np, (power size - s%s < i)%nat -> invariant s -> StateSetMap.MapsTo p np s%t -> extends s (steps i s p np) /\ forall P, defined s (fun n a => P n a \/ n=np) -> defined (steps i s p np) P.
proof: Proof. induction i; intros s p np Hsize H Hp; simpl. lia_false. cut (forall a: num, extends s (fold_labels (step' (steps i) p np) a s) /\ forall P, defined s (fun n b => P n b \/ n = np /\ b < a) -> defined (fold_labels (step' (steps i) p np) a s) P). intro G. split. eapply G. intros P HP. eapply G. intros n b Hn Hb. specialize (HP _ _ Hn Hb). tauto. intro a. revert s Hsize H Hp. induction a using num_peano_rec; intros [[t d] n] Hsize H Hp. rewrite fold_num_O. split. apply reflexive_extends. assumption. intros P HP m b Hm Hb. specialize (HP m b Hm Hb). intuition auto. num_lia_false. rewrite fold_num_S. simpl. StateSetMapProps.find_analyse. assert (H': invariant (t, StateLabelMap.add (np, a) x d, n)). constructor; try apply H. intros nq b nq'. simpl. StateLabelMapProps.map_iff. intuition subst. apply StateLabel.P.reflect in H1. injection H1; intros; subst; clear H1. exists p; auto with map. destruct (i_delta H H3) as [q ?]. exists q; auto with map. split. rewrite <- (fun s Hsize Hs Hn => proj1 (IHa s Hsize Hs Hn)); simpl; auto with map. constructor; auto with map. reflexivity. intros P HP. eapply IHa; simpl; auto with map. intros m' b Hm Hb. specialize (HP _ b Hm Hb). simpl in *. intuition subst; auto with map. destruct (eq_spec a b). subst. auto with map. num_lia. set (s' := (StateSetMap.add (delta_set a p) n t, StateLabelMap.add (np: NumOTA.t, a) n d, S n)). assert (H': invariant s'). constructor; simpl. intros q nq. StateSetMapProps.map_iff. intuition subst. intros x Hx. rewrite <- H1 in Hx. eapply bounded_delta_set, Hx. num_lia. apply (i_table_wf H H3). specialize (i_table_wf H H3). simpl. num_lia. intros q q' nq. StateSetMapProps.map_iff. intuition subst. StateSetProps.setdec. exfalso. specialize (i_table_wf H H5). simpl. num_lia. exfalso. specialize (i_table_wf H H4). simpl. num_lia. apply (i_table_inj H H4 H5). intros m Hm. destruct (eq_num_dec m n). subst. eauto with map. destruct (@i_table_surj _ H m) as [q ?]. simpl. num_lia. exists q. apply StateSetMap.add_2; trivial. intro F. rewrite <- F in H1. elim H0. exists m; assumption. erewrite StateSetMapProps.cardinal_2; eauto. apply i_table_size in H. simpl in H. rewrite H. num_lia. intro; reflexivity. intros nq b nq'. StateLabelMapProps.map_iff. intuition subst. apply StateLabel.P.reflect in H1. injection H1; intros; subst; clear H1. exists p; auto with map. apply StateSetMap.add_2; trivial. intro F. rewrite F in H0. elim H0. exists nq; assumption. destruct (i_delta H H3) as [q ?]. exists q. apply StateSetMap.add_2; trivial. intro F. rewrite F in H0. elim H0. exists nq; assumption. apply StateSetMap.add_2; trivial. intro F. rewrite F in H0. elim H0. exists nq'; assumption. specialize (IHi s' (delta_set a p) n). simpl in IHi. destruct IHi as [IHi1 IHi2]; auto with map. clear - Hsize H Hp H0 H'. subst s'. simpl in *. apply store_size_bound in H'. simpl in *. pose proof (power_positive size). num_lia. specialize (IHa (steps i s' (delta_set a p) n)). simpl in IHa. destruct IHa as [IHa1 IHa2]. clear IHi2. subst s'. apply e_next in IHi1. simpl in *. num_lia. apply IHi1. apply IHi1. simpl. apply StateSetMap.add_2; trivial. intro F. rewrite F in H0. elim H0. exists np. assumption. split. subst s'. rewrite <- IHa1. rewrite <- IHi1. constructor; simpl; auto. intros q nq Hq. apply StateSetMap.add_2; trivial. intro F. rewrite <- F in Hq. elim H0. exists nq. assumption. num_lia. intros P HP. apply IHa2. apply IHi2. unfold s' in *. clear - Hp HP. intros m b Hm Hb. simpl in *. destruct (eq_num_dec m n). subst. auto. destruct (HP m b) as [[y ?]|[ ?|[? ?]]]; subst; simpl in *; auto with map. num_lia. clear - H. eauto with map. destruct (eq_spec a b). subst. auto with map. num_lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)