proposition: Lemma loop_correct : forall n w t t' x y, measure t < n -> invariant t -> below x size -> below y size -> loop A n w t x y = inl t' -> correct_ind t t' x y /\ invariant t'.
proof: Proof. induction n. intros. lia_false. intros w tarjan tar' x y Hsize Hstat Hx Hy. simpl loop. rewrite DS.test_and_unify_eq. case_eq (DS.equiv tarjan x y). intros [|] u Hn; simpl. intro H'; injection H'; intros; subst; clear H'. split. apply correct_ind_idem; trivial. rewrite <- DS.sameclass_equiv, Hn. reflexivity. apply invariant_idem; trivial. rewrite <- DS.sameclass_equiv, Hn. reflexivity. bool_analyse. 2: discriminate. assert (IH: forall tar, fold_num_sum (fun a tar => loop A n (a :: w) tar (delta a x) (delta a y)) ml tar = inl tar' -> {{tar}} x y -> measure tar < n -> invariant tar -> correct_fold_ind tar tar' x y ml /\ invariant tar'). clear u Hn tarjan Hstat Hsize. induction ml as [|a IHa] using num_peano_rec; [setoid_rewrite fold_num_sum_O|setoid_rewrite fold_num_sum_S]; simpl; intros tar Htar Hxy Hsize Htar'. dependent destruction Htar. split; auto. constructor; auto. reflexivity. revert Htar. num_simpl. simpl. num_simpl. case_eq (loop A n (a :: w) tar (delta a x) (delta a y)); intros tar'' Htar'' Htar. 2: discriminate. apply IHn in Htar''; auto using bounded_delta. destruct Htar'' as [Htar'' Htar''i]. clear IHn. apply IHa in Htar; auto. clear IHa. split. constructor. intros l Hl. apply Htar. rewrite <- add_lists_S. apply Htar''. assumption. apply (ci_sameclass Htar''). transitivity tar''. apply Htar''. apply Htar. apply Nat.le_trans with (measure tar''). apply Htar. apply Htar''. apply Htar. apply Htar'', Hxy. eapply Nat.le_lt_trans. apply Htar''. apply Hsize. clear IHn. intro Hr. destruct (IH _ Hr) as [IH1 IH2]; clear Hr IH. apply in_union. apply (measure_union_strict (size:=size)) in Hn; auto; num_lia. apply invariant_prog; assumption. split; auto. constructor. intros l Hl. simpl; simpl in Hl. apply IH1. apply diag_ok; ti_auto. transitivity (DS.union tarjan x y). apply DSUtils.le_union. apply IH1. apply Nat.le_trans with (measure (DS.union tarjan x y)). apply IH1. apply (measure_union_strict (size:=size)) in Hn; auto using Nat.lt_le_incl; num_lia. apply IH1. apply in_union. 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(Utils_WF) Coq(Relations) Coq(List)