proposition: Lemma rt_closure_star: forall f Hwf size, (forall i, below i size -> setbelow (f i) size) -> (mx_bool tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (f (sn i)))) # == (mx_bool tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (@rt_closure f Hwf size (sn i)))).
proof: Proof. intros f Hwf size Hbounded. apply leq_antisym. apply algebraic_rt_closure; mx_intros i j Hi Hj; simpl; fold_regex; fold_leq. nat_analyse; fold_regex; auto with algebra. subst. type_view StateSet.mem; auto with algebra. elim n. rewrite <- rt_closure_spec by num_lia. constructor 1. apply sum_leq. intros k _ Hk. type_view StateSet.mem. 2: simpl; fold_regex; semiring_reflexivity. type_view StateSet.mem. 2: simpl; fold_regex; semiring_reflexivity. type_view StateSet.mem. simpl; fold_regex; semiring_reflexivity. elim n. rewrite <- rt_closure_spec by num_lia. apply trans_rt1n. constructor 3 with (sn k); apply rt1n_trans; apply <- rt_closure_spec; eauto; unfold below; num_lia. type_view StateSet.mem. 2: simpl; fold_regex; semiring_reflexivity. type_view StateSet.mem. simpl; fold_regex; semiring_reflexivity. elim n. rewrite <- rt_closure_spec by num_lia. constructor 2 with (sn j). apply StateSet.mem_1 in i0. assumption. constructor 1. mx_intros i j Hi Hj. simpl. fold_regex; fold_leq. set (m := mx_bool Datatypes.tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (f (sn i)))). type_view StateSet.mem; auto with algebra. rename i0 into Hij. rewrite <- rt_closure_spec in Hij by num_lia. revert Hi Hj. rewrite <- (id_nat i), <- (id_nat j). revert Hij. generalize (sn j) as j'. generalize (sn i) as i'. clear - Hbounded. intros i j ij. induction ij; intros Hi Hj. transitivity (!(1+m*m#) (ns x) (ns x)). simpl; fold_regex; fold_leq. nat_analyse. auto with algebra. apply equal_leq. refine (star_make_right m _ _ Hi Hj). transitivity (!(1+m*m#) (ns x) (ns z)). simpl; fold_regex; fold_leq. rewrite <- plus_make_right. assert (ns y < ns size). rewrite <- lt_nat_spec in Hi. apply Hbounded in Hi. rewrite <- lt_nat_spec. apply Hi. apply StateSet.mem_2, H. apply leq_sum. exists (ns y); repeat split; auto with arith. rewrite 2id_num. rewrite H. rewrite <- IHij by assumption. unfold xif. semiring_reflexivity. apply equal_leq. refine (star_make_right m _ _ Hi Hj). 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(Utils_WF) Coq(Relations) Coq(Eqdep_dec)