Require Import kleene boolean sups matrix.
Set Implicit Arguments.

Notation bmx := (mx_ops bool_ops bool_tt).

Fixpoint bmx_str n: bmx n n → bmx n n :=
  match n with
    | O ⇒ fun M ⇒ M
    | S n ⇒ fun M ⇒
      let b := sub01_mx (n1:=1) (m1:=1) M in
      let c := sub10_mx (n1:=1) (m1:=1) M in
      let d := bmx_str (sub11_mx (n1:=1) (m1:=1) M) in
      blk_mx 1 (b⋅d) (d⋅c) (d+d⋅c⋅(b⋅d))
  end.

Lemma bmx_top_1: top ≡ (1: bmx 1%nat 1%nat).
Proof. intros i j. now setoid_rewrite ord0_unique. Qed.

Lemma bmx_str_str n (M: bmx n n): M^* ≡ bmx_str M.
Proof.
  induction n as [|n IHn]. intro i. elim (ord_0_empty i).
  change (M^*) with (mx_str _ _ _ M).
  simpl mx_str. simpl bmx_str. unfold mx_str_build.
  ra_fold (mx_ops bool_ops bool_tt). rewrite bmx_top_1.
  now rewrite IHn, dot1x, dotx1.
Qed.

Inductive rt_clot n (M: bmx n n): ord n → ord n → Prop :=
| clot_nil: ∀ i, rt_clot M i i
| clot_cons: ∀ i j k, M i j → rt_clot M j k → rt_clot M i k.

Lemma clot_app n (M: bmx n n): ∀ i j k, rt_clot M i j → rt_clot M j k → rt_clot M i k.
Proof. induction 1; eauto using clot_cons. Qed.

Lemma clot_snoc n (M: bmx n n): ∀ i j k, rt_clot M i j → M j k → rt_clot M i k.
Proof. intros. eapply clot_app. eassumption. eapply clot_cons. eassumption. constructor. Qed.

Lemma rt_clot_S_S n (M: bmx (1+n)%nat (1+n)%nat): ∀ i j,
  rt_clot (sub11_mx M) i j → rt_clot M (rshift i) (rshift j).
Proof. induction 1. constructor. eapply clot_cons; eassumption. Qed.

Theorem bmx_str_clot n (M: bmx n n) i j: M^* i j ↔ rt_clot M i j.
Proof.
split.
- assert (M^* i j ≡ bmx_str M i j).   apply bmx_str_str. rewrite H. clear H. revert i j.
  induction n as [|n IH]; intros i' j'.
   simpl. intro. eapply clot_cons. eassumption. constructor.
  unfold bmx_str; fold (@bmx_str n). set (M' := sub11_mx (n1:=1) (m1:=1) M).
  specialize (IH M'). unfold blk_mx, row_mx, col_mx.
  case ordinal.split_spec; intros i ->; case ordinal.split_spec; intros j → Hij.
  + setoid_rewrite ord0_unique. constructor.
  + setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]].
    apply Bool.andb_true_iff in Hk as [Hik Hkj].
    apply IH in Hkj. unfold M' in Hkj.
    eapply clot_cons. eassumption. now apply rt_clot_S_S.
  + setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]].
    apply Bool.andb_true_iff in Hk as [Hik Hkj].
    apply IH in Hik. unfold M' in Hik.
    eapply clot_snoc. apply rt_clot_S_S; eassumption. assumption.
  + setoid_rewrite Bool.orb_true_iff in Hij. destruct Hij as [Hij|Hij].
     apply IH in Hij. now apply rt_clot_S_S.
    setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]].
    apply Bool.andb_true_iff in Hk as [Hik Hkj].
    setoid_rewrite is_true_sup in Hik. destruct Hik as [i' [_ Hi']].
    apply Bool.andb_true_iff in Hi' as [Hii' Hi'k].
    setoid_rewrite is_true_sup in Hkj. destruct Hkj as [j' [_ Hj']].
    apply Bool.andb_true_iff in Hj' as [Hkj' Hj'j].
    apply IH in Hii'. apply IH in Hj'j.
    eapply clot_app. apply rt_clot_S_S, Hii'.
    eapply clot_cons. apply Hi'k.
    eapply clot_cons. apply Hkj'.
    apply rt_clot_S_S, Hj'j.
- induction 1 as [i|i j k Hij Hjk IH].
  + pose proof (str_refl (X:=bmx) M i i). simpl in H.
    apply H. unfold mx_one. now rewrite eqb_refl.
  + pose proof (str_cons (X:=bmx) M i k). simpl in H.
    apply H. clear H.
    unfold mx_dot. rewrite is_true_sup. eexists. split. apply in_seq.
    apply Bool.andb_true_iff. split; eassumption.
Qed.