text:
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
Import uPred.

Definition CG_StackType τ :=
  TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).

(* Coarse-grained push *)
Definition CG_push (st : expr) : expr :=
  Lam (Store (st.[ren (+1)]) (Fold (InjR (Pair (Var 0) (Load st.[ren (+ 1)]))))).

Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l.
Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l.

Definition CG_pop (st : expr) : expr :=
  Lam (Case (Unfold (Load st.[ren (+ 1)]))
            (InjL Unit)
            (
              Seq
                (Store st.[ren (+ 2)] (Snd (Var 0)))
                (InjR (Fst (Var 0)))
            )
      ).

Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l.
Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l.

Definition CG_snap (st l : expr) :=  with_lock (Lam (Load st.[ren (+1)])) l.
Definition CG_snapV (st l : expr) : val := with_lockV (Lam (Load st.[ren (+1)])) l.

Definition CG_iter (f : expr) : expr :=
  Rec (Case (Unfold (Var 1))
            Unit
            (
              Seq
                (App f.[ren (+3)] (Fst (Var 0)))
                (App (Var 1) (Snd (Var 0)))
            )
      ).

Definition CG_iterV (f : expr) : val :=
  RecV (Case (Unfold (Var 1))
            Unit
            (
              Seq
                (App f.[ren (+3)] (Fst (Var 0)))
                (App (Var 1) (Snd (Var 0)))
            )
      ).

Definition CG_snap_iter (st l : expr) : expr :=
  Lam (App (CG_iter (Var 0)) (App (CG_snap st.[ren (+1)] l.[ren (+1)]) Unit)).

Definition CG_stack_body (st l : expr) : expr :=
  Pair (Pair (CG_locked_push st l) (CG_locked_pop st l))
       (CG_snap_iter st l).

Definition CG_stack : expr :=
  TLam (
      LetIn
        newlock
        (LetIn
           (Alloc (Fold (InjL Unit)))
           (CG_stack_body (Var 0) (Var 1)))).

Section CG_Stack.
  Context `{heapIG Σ, cfgSG Σ}.

  Lemma CG_push_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ (CG_push st) (TArrow τ TUnit).
  Proof.
    intros H1. repeat econstructor.
    eapply (context_weakening [_]); eauto.
    repeat constructor; asimpl; trivial.
    eapply (context_weakening [_]); eauto.
  Qed.

  Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
  Proof. unfold CG_push; asimpl; trivial. Qed.

  Hint Rewrite CG_push_subst : autosubst.

  Lemma steps_CG_push E j K st v w :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ v ∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w))
    ⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (step_load _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
            with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    simpl.
    iMod (step_store _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    { rewrite /= !to_of_val //. }
    iModIntro. by iFrame.
  Qed.

  Typeclasses Opaque CG_push.
  Global Opaque CG_push.

  Lemma CG_locked_push_to_val st l :
    to_val (CG_locked_push st l) = Some (CG_locked_pushV st l).
  Proof. trivial. Qed.

  Lemma CG_locked_push_of_val st l :
    of_val (CG_locked_pushV st l) = CG_locked_push st l.
  Proof. trivial. Qed.

  Global Opaque CG_locked_pushV.
  Lemma CG_locked_push_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ l LockType →
    typed Γ (CG_locked_push st l) (TArrow τ TUnit).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; auto using CG_push_type.
  Qed.

  Lemma CG_locked_push_subst (st l : expr) f :
    (CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f].
  Proof. by rewrite /CG_locked_push; asimpl. Qed.

  Hint Rewrite CG_locked_push_subst : autosubst.

  Lemma steps_CG_locked_push E j K st w v l :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false)
      ∗ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
    ⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]")
      as "Hj"; auto.
    iIntros (K') "[#Hspec Hxj]".
    iApply steps_CG_push; first done. by iFrame.
  Qed.

  Typeclasses Opaque CG_locked_push.
  Global Opaque CG_locked_push.

  (* Coarse-grained pop *)
  Lemma CG_pop_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ (CG_pop st) (TArrow TUnit (TSum TUnit τ)).
  Proof.
    intros H1.
    econstructor.
    eapply (Case_typed _ _ _ _ TUnit); eauto using typed.
    - replace (TSum TUnit (TProd τ (CG_StackType τ))) with
          ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
        by (by asimpl).
      repeat econstructor.
      eapply (context_weakening [_]); eauto.
    - econstructor; eauto using typed.
      econstructor; eauto using typed.
      eapply (context_weakening [_; _]); eauto.
  Qed.

  Lemma CG_pop_subst (st : expr) f :
    (CG_pop st).[f] = CG_pop st.[f].
  Proof. by rewrite /CG_pop; asimpl. Qed.

  Hint Rewrite CG_pop_subst : autosubst.

  Lemma steps_CG_pop_suc E j K st v w :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗
               j ⤇ fill K (App (CG_pop (Loc st)) Unit)
      ⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v.
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K)  with "[$Hj $Hx]")
      as "[Hj Hx]"; eauto.
    simpl.
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K)
            with "[$Hj]") as "Hj"; eauto.
    simpl.
    iMod (step_store _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]";
      eauto using to_of_val.
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iMod (do_step_pure _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto.
    simpl.
    by iFrame "Hj Hx".
  Qed.

  Lemma steps_CG_pop_fail E j K st :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ FoldV (InjLV UnitV) ∗
               j ⤇ fill K (App (CG_pop (Loc st)) Unit)
      ⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV).
  Proof.
    iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (step_load _ j (UnfoldCtx :: CaseCtx _ _ :: K)
                    _ _ _ with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    by iFrame "Hj Hx"; trivial.
  Qed.

  Typeclasses Opaque CG_pop.
  Global Opaque CG_pop.

  Lemma CG_locked_pop_to_val st l :
    to_val (CG_locked_pop st l) = Some (CG_locked_popV st l).
  Proof. trivial. Qed.

  Lemma CG_locked_pop_of_val st l :
    of_val (CG_locked_popV st l) = CG_locked_pop st l.
  Proof. trivial. Qed.

  Global Opaque CG_locked_popV.

  Lemma CG_locked_pop_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ l LockType →
    typed Γ (CG_locked_pop st l) (TArrow TUnit (TSum TUnit τ)).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; auto using CG_pop_type.
  Qed.

  Lemma CG_locked_pop_subst (st l : expr) f :
    (CG_locked_pop st l).[f] = CG_locked_pop st.[f] l.[f].
  Proof. by rewrite /CG_locked_pop; asimpl. Qed.

  Hint Rewrite CG_locked_pop_subst : autosubst.

  Lemma steps_CG_locked_pop_suc E j K st v w l :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false)
               ∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
      ⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
                          _ (InjRV w) UnitV
            with "[$Hj $Hx $Hl]") as "Hj"; eauto.
    iIntros (K') "[#Hspec Hxj]".
    iApply steps_CG_pop_suc; eauto.
  Qed.

  Lemma steps_CG_locked_pop_fail E j K st l :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false)
               ∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
      ⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _
                          (InjLV UnitV) UnitV
          with "[$Hj $Hx $Hl]") as "Hj"; eauto.
    iIntros (K') "[#Hspec Hxj] /=".
      iApply steps_CG_pop_fail; eauto.
  Qed.

  Typeclasses Opaque CG_locked_pop.
  Global Opaque CG_locked_pop.

  Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l).
  Proof. trivial. Qed.

  Lemma CG_snap_of_val st l : of_val (CG_snapV st l) = CG_snap st l.
  Proof. trivial. Qed.

  Typeclasses Opaque CG_snapV.
  Global Opaque CG_snapV.

  Lemma CG_snap_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ l LockType →
    typed Γ (CG_snap st l) (TArrow TUnit (CG_StackType τ)).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; trivial. do 2 constructor.
    eapply (context_weakening [_]); eauto.
  Qed.

  Lemma CG_snap_subst (st l : expr) f :
    (CG_snap st l).[f] = CG_snap st.[f] l.[f].
  Proof. by unfold CG_snap; asimpl. Qed.

  Hint Rewrite CG_snap_subst : autosubst.

  Lemma steps_CG_snap E j K st v l :
    nclose specN ⊆ E →
    spec_ctx ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false)
               ∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit)
      ⊢ |={E}=> j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV
          with "[$Hj $Hx $Hl]") as "Hj"; eauto.
    iIntros (K') "[#Hspec [Hx Hj]]".
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (step_load with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    by iFrame.
  Qed.

  Typeclasses Opaque CG_snap.
  Global Opaque CG_snap.

  (* Coarse-grained iter *)
  Lemma CG_iter_folding (f : expr) :
    CG_iter f =
    Rec (Case (Unfold (Var 1))
              Unit
              (
                Seq
                  (App f.[ren (+3)] (Fst (Var 0)))
                  (App (Var 1) (Snd (Var 0)))
              )
        ).
  Proof. trivial. Qed.

  Lemma CG_iter_type f Γ τ :
    typed Γ f (TArrow τ TUnit) →
    typed Γ (CG_iter f) (TArrow (CG_StackType τ) TUnit).
  Proof.
    intros ?. econstructor.
    eapply (Case_typed _ _ _ _ TUnit); eauto using typed.
    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
      by (by asimpl).
    repeat econstructor.
    repeat econstructor; simpl; eauto using typed.
    eapply (context_weakening [_; _; _]); eauto.
  Qed.

  Lemma CG_iter_to_val f : to_val (CG_iter f) = Some (CG_iterV f).
  Proof. trivial. Qed.

  Lemma CG_iter_of_val f : of_val (CG_iterV f) = CG_iter f.
  Proof. trivial. Qed.

  Typeclasses Opaque CG_iterV.
  Global Opaque CG_iterV.

  Lemma CG_iter_subst (f : expr) g : (CG_iter f).[g] = CG_iter f.[g].
  Proof. by unfold CG_iter; asimpl. Qed.

  Hint Rewrite CG_iter_subst : autosubst.

  Lemma steps_CG_iter E j K f v w :
    nclose specN ⊆ E →
    spec_ctx
             ∗ j ⤇ fill K (App (CG_iter (of_val f))
                               (Fold (InjR (Pair (of_val w) (of_val v)))))
      ⊢ |={E}=>
    j ⤇ fill K
          (Seq (App (of_val f) (of_val w))
               (App (CG_iter (of_val f)) (Snd (Pair (of_val w) (of_val v))))).
  Proof.
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]")
      as "Hj"; eauto.
  Qed.

  Lemma steps_CG_iter_end E j K f :
    nclose specN ⊆ E →
    spec_ctx ∗ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
      ⊢ |={E}=> j ⤇ fill K Unit.
  Proof.
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
  Qed.

  Typeclasses Opaque CG_iter.
  Global Opaque CG_iter.

  Lemma CG_snap_iter_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ l LockType →
    typed Γ (CG_snap_iter st l) (TArrow (TArrow τ TUnit) TUnit).
  Proof.
    intros H1 H2; repeat econstructor.
    - eapply CG_iter_type; by constructor.
    - eapply CG_snap_type; by eapply (context_weakening [_]).
  Qed.

  Lemma CG_snap_iter_subst (st l : expr) g :
    (CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g].
  Proof. by unfold CG_snap_iter; asimpl. Qed.

  Hint Rewrite CG_snap_iter_subst : autosubst.

  Lemma CG_stack_body_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) →
    typed Γ l LockType →
    typed Γ (CG_stack_body st l)
          (TProd
             (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ)))
             (TArrow (TArrow τ TUnit) TUnit)
          ).
  Proof.
    intros H1 H2.
    repeat (econstructor; eauto using CG_locked_push_type,
                          CG_locked_pop_type, CG_snap_iter_type).
  Qed.

  Typeclasses Opaque CG_snap_iter.
  Global Opaque CG_snap_iter.

  Lemma CG_stack_body_subst (st l : expr) f :
    (CG_stack_body st l).[f] = CG_stack_body st.[f] l.[f].
  Proof. by unfold CG_stack_body; asimpl. Qed.

  Hint Rewrite CG_stack_body_subst : autosubst.

  Lemma CG_stack_type Γ :
    typed Γ CG_stack
          (TForall
             (TProd
                (TProd
                   (TArrow (TVar 0) TUnit)
                   (TArrow TUnit (TSum TUnit (TVar 0)))
                )
                (TArrow (TArrow (TVar 0) TUnit) TUnit)
          )).
  Proof.
    repeat econstructor;
      eauto 10 using newlock_type, CG_locked_push_type, CG_locked_pop_type,
      CG_snap_iter_type, typed.
    asimpl; repeat constructor.
  Qed.

  Lemma CG_stack_closed f : CG_stack.[f] = CG_stack.
  Proof. by unfold CG_stack; asimpl. Qed.

End CG_Stack.

Hint Rewrite CG_push_subst : autosubst.
Hint Rewrite CG_locked_push_subst : autosubst.
Hint Rewrite CG_locked_pop_subst : autosubst.
Hint Rewrite CG_pop_subst : autosubst.
Hint Rewrite CG_locked_pop_subst : autosubst.
Hint Rewrite CG_snap_subst : autosubst.
Hint Rewrite CG_iter_subst : autosubst.
Hint Rewrite CG_snap_iter_subst : autosubst.
Hint Rewrite CG_stack_body_subst : autosubst.
Hint Rewrite CG_stack_closed : autosubst.

author: anemoneflower

repo: IRIS-study


text:
From discprob.basic Require Import base order nify.
From discprob.prob Require Import prob countable finite stochastic_order uniform.
From discprob.monad.finite Require Import monad permutation.
From discprob.monad.finite Require quicksort quicksort_cost.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
From mathcomp Require Import tuple finfun bigop prime binomial finset.
From Coq Require Import Omega Psatz Program.Wf MSets.MSetInterface MSets.MSetGenTree Structures.OrdersEx.
Local Open Scope nat_scope.

(* The Coq standard library includes a generic implementation of
   binary search trees, parametrized by a generic "information" type
   that is stored in each node. This library is used in the
   implementation of Red-Black and AVL trees, in which the information
   stored is the color/height. Obviously, insertion cannot be
   generically defined, because these self-balancing trees do
   different things when inserting. However, the operations that do
   not build or alter the tree can be defined generically since they
   do not make use of the information field.

   Since we are going to analyze non-balancing binary search trees,
   we do not need to track any extra information, so we will just
   instantiate this generic machinery taking the information type
   to be unit. *)

Module unit.
  Definition t := unit.
End unit.

Include MSetGenTree.Ops Nat_as_OT unit.
Include MSetGenTree.Props Nat_as_OT unit.

Scheme tree_rect := Induction for tree Sort Type.

(* The notion of tree equality in the MSetGenTree library is actually about equivalence as sets,
   not them being literally equal. So, to make trees into an eqType we need our own decidable
   equality routine *)
Fixpoint tree_eq_bool (t1 t2 : tree) : bool :=
  match t1, t2 with
    | Leaf, Leaf => true
    | Node _ t1l v1 t1r, Node _ t2l v2 t2r =>
      (v1 == v2) && (tree_eq_bool t1l t2l) && (tree_eq_bool t1r t2r)
    | _, _ => false
  end.
Lemma eq_tree : Equality.axiom tree_eq_bool.
Proof.
  move=> t1 t2.
  revert t2. induction t1 using tree_rect => t2.
  { apply: (iffP idP); rewrite /tree_eq_bool //=.
    - destruct t2; auto; try inversion 1.
    - destruct t2; auto; try inversion 1. }
  apply: (iffP idP); rewrite //=.
  - destruct t2; auto; try (inversion 1; done).
    move /andP => [].
    move /andP => [].
    move /eqP => ?; subst.
    move /IHt1_1 => ->. move /IHt1_2 => ->; f_equal. destruct t, t0; done.
  - inversion 1; subst.
    apply /andP; split; auto.
    apply /andP; split; auto.
    * by apply /IHt1_1.
    * by apply /IHt1_2.
Qed.
Canonical tree_eqMixin := EqMixin (@eq_tree).
Canonical tree_eqType := Eval hnf in EqType tree (tree_eqMixin).

Fixpoint height (t: tree) :=
  match t with
    | Leaf => 0
    | Node _ Leaf v Leaf => 0
    | Node _ tl v tr =>
      S (max (height tl) (height tr))
  end.

Fixpoint add (x: nat) (t: tree) :=
  match t with
    | Leaf => Node tt Leaf x Leaf
    | Node _ tl v tr =>
      match (Nat.compare x v) with
        | Eq => t
        | Lt => Node tt (add x tl) v tr
        | Gt => Node tt tl v (add x tr)
      end
  end.

(* We prove the add function satisfies the same properties
   as the add functions for the AVL and RB trees. These proofs
   are not intended to be optimal! *)
Lemma add_spec': ∀ t x y,
    InT y (add x t) ↔ y = x ∨ InT y t.
Proof.
  induction t using tree_ind.
  - rewrite //= => x y; split.
    * inversion 1; subst; auto.
    * destruct 1 as [|Hinl]; subst.
      ** by econstructor.
      ** by inversion Hinl.
  - rewrite //= => x y.
    specialize (Nat.compare_eq x t3).
    destruct (Nat.compare x t3).
    * intros -> => //; split; auto.
      inversion 1; auto. subst. econstructor; done.
    * intros _. split.
      ** inversion 1; subst.
         *** right. econstructor; done.
         *** edestruct (proj1 (IHt1 x y)); eauto. right.
             eapply (InLeft); eauto.
         *** right. eapply (InRight); eauto.
      ** inversion 1 as [Heq|Hin].
         *** subst. apply InLeft; eapply IHt1; firstorder.
         *** inversion Hin; subst.
             **** econstructor; eauto.
             **** apply InLeft. apply IHt1; firstorder.
             **** apply InRight. done.
    * intros _. split.
      ** inversion 1; subst.
         *** right. econstructor; done.
         *** right. eapply (InLeft); eauto.
         *** edestruct (proj1 (IHt2 x y)); eauto. right.
             eapply (InRight); eauto.
      ** inversion 1 as [Heq|Hin].
         *** subst. apply InRight; eapply IHt2; firstorder.
         *** inversion Hin; subst.
             **** econstructor; eauto.
             **** apply InLeft. done.
             **** apply InRight. apply IHt2; firstorder.
Qed.

Lemma add_spec: ∀ t x y `{Ok t},
    InT y (add x t) ↔ y = x ∨ InT y t.
Proof.
  intros; apply add_spec'.
Qed.

Instance add_ok t x `{HOk: Ok t} : Ok (add x t).
Proof.
  induction HOk as [|? v tl tr Hl Hok' Hr ? Hlt Hgt].
  - rewrite //=; econstructor; try (econstructor); eauto;
      rewrite /lt_tree/gt_tree//= => y; inversion 1.
  - rewrite //=. specialize (Nat.compare_spec x v) => Hspec.
    destruct (Nat.compare x v) => //=.
    * intros. econstructor; eauto.
    * intros. econstructor; eauto.
      intros y. rewrite add_spec'. intros [Heq|Hin]; subst.
      ** inversion Hspec; done.
      ** apply Hlt; done.
    * intros. econstructor; eauto.
      intros y. rewrite add_spec'. intros [Heq|Hin]; subst.
      ** inversion Hspec; done.
      ** apply Hgt; done.
Qed.

Module examples.
Definition t1 := (add 7 (add 3 (add 5 (add 2 Leaf)))).
(*
Eval compute in t1.
Eval compute in (height t1).
*)

Definition t2 := (add 9 (add 8 (add 7 (add 6 (add 5 (add 4 (add 3 (add 2 (add 1 Leaf))))))))).
(*
Eval compute in t2.
Eval compute in (height t2).
*)
End examples.

Fixpoint add_list (l: list nat) (t: tree) :=
  match l with
    | [::] => t
    | n :: l => add_list l (add n t)
  end.

Lemma add_list_rec x (l: list nat) (tl tr: tree) :
  add_list l (Node tt tl x tr) =
  Node tt (add_list [seq i <- l | i < x] tl) x (add_list [seq i <- l | i > x] tr).
Proof.
  revert x tl tr.
  induction l as [| a l] => x tl tr.
  - rewrite //=.
  - rewrite //=.
    specialize (Nat.compare_spec a x) => Hspec.
    destruct (a ?= x); inversion Hspec; subst.
    * case: ifP; first (intros; nify; exfalso; omega); auto.
    * do 2 (case: ifP; move /ltP); try (intros; omega); [].
      intros _ _. rewrite IHl; f_equal.
    * do 2 (case: ifP; move /ltP); try (intros; omega); [].
      intros _ _. rewrite IHl; f_equal.
Qed.

Lemma add_list_rec_empty a (l: list nat):
  add_list (a :: l) Leaf =
  Node tt (add_list [seq i <- l | i < a] Leaf) a (add_list [seq i <- l | i > a] Leaf).
Proof.
  rewrite //= add_list_rec //.
Qed.

Definition add_list_random : list nat → tree → ldist tree.
  refine(Fix (measure_wf lt_wf size) (fun _ => tree → ldist tree)
  (fun l add_list_random =>
     λ t,
     match l as l' return (l = l' → ldist tree) with
     | [::] => λ eq, mret t
     | [::a] => λ eq, mret (add a t)
     | (a :: b :: l') => λ eq,
                         p ← draw_next a (b :: l');
                         add_list_random (rem (sval p) (a :: b :: l')) _ (add (sval p) t)
     end (Init.Logic.eq_refl))); rewrite /MR; auto.
  - abstract (destruct p as (x&Hin); rewrite size_rem //; subst; rewrite //=).
Defined.

Lemma alr_unfold_aux l t:
  add_list_random l t =
  match l as l' return (l = l' → ldist tree) with
    | [::] => λ eq, mret t
    | [:: a] => λ eq, mret (add a t)
    | (a :: b :: l') => λ eq,
      p ← draw_next a (b :: l');
      add_list_random (rem (sval p) (a :: b :: l')) (add (sval p) t)
  end (Init.Logic.eq_refl).
Proof. rewrite /add_list_random quicksort.easy_fix_eq; done. Qed.

Lemma alr_unfold l t:
  add_list_random l t =
  (match l with
    | [::] => mret t
    | [::a] => mret (add a t)
    | (a :: l) =>
      p ← draw_next a l;
      add_list_random (rem (sval p) (a :: l)) (add (sval p) t)
  end).
Proof.
  rewrite alr_unfold_aux. destruct l => //. destruct l => //.
Qed.

Import seq.
Lemma size_filter_lt {A: eqType} (l: seq A) (P: pred A):
  (∃ i, i \in l ∧ ~ P i) → (size [seq i <- l | P i] < size l)%nat.
Proof.
  induction l => //=.
  - intros (i&Hin&Hnot). rewrite in_nil in Hin. done.
  - intros Hin. case: ifP.
    * intros HP. rewrite //=.
      assert (size [seq i <- l | P i] < size l)%nat.
      { apply IHl. edestruct Hin as (i&Hin'&?).  exists i. split; auto. rewrite in_cons in Hin'.
        move /orP in Hin'. destruct Hin' as [Heq|?]; auto. move /eqP in Heq; subst; auto.
      }
      nify. omega.
    * intros. rewrite size_filter. specialize (count_size P l). rewrite //=.
Qed.

Lemma size_filter_le {A: eqType} (l: seq A) (P: pred A):
  (size [seq i <- l | P i] <= size l)%coq_nat.
Proof.
  rewrite size_filter.
  specialize (count_size P l). intros; nify. rewrite //=.
Qed.

Lemma alr_rand_perm l t:
  eq_dist (rvar_of_ldist (add_list_random l t))
          (rvar_of_ldist (l' ← rand_perm_list l; mret (add_list l' t))).
Proof.
  remember (size l) as k eqn:Heq.
  revert l t Heq.
  induction k as [k IH] using (well_founded_induction lt_wf) => l t Heq.
  destruct l as [| a l]; last destruct l as [| b l].
  - apply outcomes_eq_dist => //=; repeat f_equal; nra.
  - rewrite alr_unfold; rewrite rand_perm_list_unfold.
    apply outcomes_eq_dist => //=; repeat f_equal; nra.
  - rewrite alr_unfold; rewrite rand_perm_list_unfold.
    rewrite (ldist_assoc (draw_next a (b :: l))).
    apply eq_dist_ldist_bind_ext. intros (x&Hin). rewrite /sval.
    rewrite (ldist_assoc (rand_perm_list _)).
    eapply eq_dist_trans; first eapply IH; try eauto.
    { rewrite size_rem //; subst; rewrite //=. }
    apply eq_dist_ldist_bind_ext. intros l'.
    rewrite ldist_left_id //=.
Qed.

(* Here we give a version that looks closer to the kind of recursion in quicksort,
   and which matches the format needed for the span2 lemma *)
Definition rand_tree_rec : list nat → ldist tree.
  refine(Fix (measure_wf lt_wf size) (fun _ => ldist tree)
  (fun l rand_tree_rec =>
     match l as l' return (l = l' → ldist tree) with
     | [::] => λ eq, mret Leaf
     | [::a] => λ eq, mret (Node tt Leaf a Leaf)
     | (a :: b :: l') => λ eq,
                         p ← draw_next a (b :: l');

                         tl ← rand_tree_rec [seq i <- (a :: b :: l') | (i < sval p)%nat] _;
                         tr ← rand_tree_rec [seq i <- (a :: b :: l') | (i > sval p)%nat] _;
                         mret (Node tt tl (sval p) tr)
     end (Init.Logic.eq_refl))); rewrite /MR; auto.
  - abstract (apply /ltP; subst; apply size_filter_lt;
              exists (sval p); split; destruct p as (?&Hin); auto => //= ?; nify; omega).
  - abstract (apply /ltP; subst; apply size_filter_lt;
              exists (sval p); split; destruct p as (?&Hin); auto => //= ?; nify; omega).
Defined.

Lemma rt_unfold_aux l:
  rand_tree_rec l =
  match l as l' return (l = l' → ldist tree) with
     | [::] => λ eq, mret Leaf
     | [::a] => λ eq, mret (Node tt Leaf a Leaf)
     | (a :: b :: l') => λ eq,
                         p ← draw_next a (b :: l');

                         tl ← rand_tree_rec [seq i <- (a :: b :: l') | (i < sval p)%nat];
                         tr ← rand_tree_rec [seq i <- (a :: b :: l') | (i > sval p)%nat];
                         mret (Node tt tl (sval p) tr)
  end (Init.Logic.eq_refl).
Proof. rewrite /rand_tree_rec quicksort.easy_fix_eq; done. Qed.

Lemma rt_unfold l:
  rand_tree_rec l =
  (match l with
    | [::] => mret Leaf
    | [::a] => mret (Node tt Leaf a Leaf)
    | (a :: l) =>
                         p ← draw_next a l;

                         tl ← rand_tree_rec [seq i <- (a :: l) | (i < sval p)%nat];
                         tr ← rand_tree_rec [seq i <- (a :: l) | (i > sval p)%nat];
                         mret (Node tt tl (sval p) tr)
  end).
Proof.
  rewrite rt_unfold_aux. destruct l => //. destruct l => //.
Qed.

Lemma rt_gen_perm l:
  uniq l →
  eq_dist (rvar_of_ldist (rand_tree_rec l))
          (rvar_of_ldist (l' ← rand_perm_list l; mret (add_list l' Leaf))).
Proof.
  remember (size l) as k eqn:Heq.
  revert l Heq.
  induction k as [k IH] using (well_founded_induction lt_wf) => l Heq Huniq.
  destruct l as [| a l]; last destruct l as [| b l].
  - apply outcomes_eq_dist => //=; repeat f_equal; nra.
  - rewrite rt_unfold; rewrite rand_perm_list_unfold.
    apply outcomes_eq_dist => //=; repeat f_equal; nra.
  - rewrite rt_unfold; rewrite rand_perm_list_unfold.
    rewrite (ldist_assoc (draw_next a (b :: l))).
    apply eq_dist_ldist_bind_ext. intros (x&Hin). rewrite /sval.
    rewrite (ldist_fmap_bind).
    eapply eq_dist_trans; last first.
    { f_equal. eapply eq_dist_ldist_bind_ext => l'.
      rewrite add_list_rec_empty. apply eq_dist_refl.  }
    rewrite -(ldist_fmap_bind _ (λ l, ([seq i <- l | i < x], [seq i <- l | x < i ]))
                              (λ ls, mret (Node tt (add_list (fst ls) Leaf) x
                                                   (add_list (snd ls) Leaf)))).
    eapply eq_dist_trans; last first.
    { eapply eq_dist_ldist_bind_congr; last done.
      apply eq_dist_sym. by eapply rand_perm_list_split, rem_uniq. }
    rewrite ?ldist_assoc.
    eapply eq_dist_trans; last first.
    { eapply eq_dist_ldist_bind_ext => x0.
      rewrite (ldist_fmap_bind _ (λ l2, (x0, l2))).
      rewrite /fst/snd.
      rewrite -(ldist_fmap_bind _ (λ l, add_list l Leaf)
                                 (λ ls, mret (Node tt (add_list x0 Leaf) x ls))).
      eapply eq_dist_ldist_bind_congr.
      eapply IH; eauto.
      * eapply le_lt_trans; first eapply size_filter_le.
        rewrite size_rem //. subst => //=.
      * by apply filter_uniq, rem_uniq.
      * done.
    }
    eapply eq_dist_trans; last first.
    { eapply ldist_bind_swap. }
    eapply eq_dist_trans; last first.
    { eapply eq_dist_ldist_bind_ext => tr.
      rewrite -(ldist_fmap_bind _ (λ l, add_list l Leaf)
                                 (λ tl, mret (Node tt tl x tr))).
      eapply eq_dist_ldist_bind_congr.
      eapply IH; eauto.
      * eapply le_lt_trans; first eapply size_filter_le.
        rewrite size_rem //. subst => //=.
      * by apply filter_uniq, rem_uniq.
      * done.
    }
    eapply eq_dist_trans; last apply ldist_bind_swap.
    rewrite ?filter_rem ?rem_id; first apply eq_dist_refl.
    * rewrite mem_filter. apply /andP. intros (?&?). nify. omega.
    * rewrite mem_filter. apply /andP. intros (?&?). nify. omega.
Qed.

Lemma alr_rt_perm l:
  uniq l →
  eq_dist (rvar_of_ldist (add_list_random l Leaf))
          (rvar_of_ldist (rand_tree_rec l)).
Proof.
  intros Huniq. eapply eq_dist_trans.
  - apply alr_rand_perm.
  - apply eq_dist_sym. apply rt_gen_perm.
  done.
Qed.

author: jtassarotti

repo: coq-proba

save_path: github-repos/coq/jtassarotti-coq-proba


text:
(*
 Copyright 2022 ZhengPu Shi
  This file is part of coq-matrix. It is distributed under the MIT
  "expat license". You should have recieved a LICENSE file with it.

  purpose   : Matrix implemented with Recursive Pair
  author    : ZhengPu Shi
  date      : 2021.12

  remark    :
  1. the definition of vec inspired by Coquelicot.
  2. all definitions are polymorphism.
*)

Require Export ListListExt.

Require Export Arith.   (* minus_plus *)
Require Export Lia.
Require Export FunctionalExtensionality.
Require Export DepPair.Vector.

(** ** Definitions of matrix module, it is implemented as a Vector 2 *)
Section mat.

  Variable T : Type.

  Definition mat (r c : nat) : Type := @vec (@vec T c) r.

  Lemma mat_r0 (c : nat) (m : mat 0 c) : m = tt.
  Proof. destruct m. auto. Qed.

  Lemma mat_rS (r c : nat) (m : mat (S r) c) : {v & {m' | m = (v, m')}}.
  Proof. apply vec_S. Qed.

End mat.

Arguments mat {T}.
Arguments mat_r0 {T c}.
Arguments mat_rS {T r c}.

Example mat_ex1 : mat 2 3 := [[1;2;3];[4;5;6]].
Example mat_ex2 : mat 2 3 := [[7;8;9];[10;11;12]].
Example mat_ex3 : mat 3 2 := [[1;2];[3;4];[5;6]].

(** ** Construct a matrix with a function *)
Section mmake.

  Variable T : Type.

  Definition mmake (r c : nat) (f : nat -> nat -> T) : mat r c :=
    vmake r (fun ic => (vmake c (f ic))).

  Lemma mmake_row_S : forall {r c : nat} (f : nat -> nat -> T),
    mmake (S r) c f = (vmake c (f 0), mmake r c (fun i j => f (S i) j)).
  Proof.
    induction r; intros; simpl.
    - unfold mmake. rewrite vmake_S. auto.
    - rewrite IHr. unfold mmake. rewrite vmake_S. f_equal.
      rewrite vmake_S. auto.
  Qed.

End mmake.

Arguments mmake {T}.

(** ** Get (ir,rc) element of a matrix *)
Section mnth.

  Variable T : Type.
  Variable T0 : T.

  Definition mnth {r c} (m : mat r c) (ir ic : nat) : T :=
    vnth T0 ic (vnth (vrepeat c T0) ir m).

  Lemma mnth_mmake : forall {r c} f i j, i < r -> j < c ->
    mnth (mmake r c f) i j = f i j.
  Proof.
    unfold mnth. unfold mmake. intros. remember (vrepeat c T0).
    rewrite vnth_vmake_valid; auto.
    rewrite vnth_vmake_valid; auto.
  Qed.

End mnth.

Arguments mnth {T} T0 {r c}.

(** ** Construct a matrix with same element *)
Section mrepeat.

  Variable T : Type.

  Definition mrepeat (r c : nat)  (def : T) : mat r c :=
    mmake r c (fun ir ic => def).

  Lemma mrepeat_r0 {c} def : mrepeat 0 c def = tt.
  Proof. compute. auto. Qed.

  Lemma mrepeat_rS {r c} def : mrepeat (S r) c def =
    (vrepeat c def, mrepeat r c def).
  Proof.
    unfold mrepeat. unfold mmake. unfold vmake. simpl. f_equal.
    - induction c; simpl; auto. f_equal. rewrite vmake_aux_S. apply IHc.
    - rewrite vmake_aux_S. auto.
  Qed.

  Lemma mrepeat_c0 {r} def : mrepeat r 0 def = vec0 tt r.
  Proof.
    induction r; simpl; auto.
    unfold mrepeat in *. unfold mmake in *. unfold vmake in *. simpl. f_equal.
    rewrite vmake_aux_S. auto.
  Qed.

  Lemma mat_c0 {r : nat} (m : @mat T r 0) : m = vec0 tt r.
  Proof.
    induction r; destruct m; simpl; auto. destruct v. f_equal. apply IHr.
  Qed.

End mrepeat.

Arguments mrepeat {T}.
Arguments mrepeat_r0 {T c}.
Arguments mrepeat_rS {T r c}.
Arguments mrepeat_c0 {T r}.
Arguments mat_c0 {T r}.

(** ** Zero matrix *)
Section mat0.

  Variable T : Type.
  Variable T0 : T.

  Definition mat0 {r c} : @mat T r c := mmake r c (fun i j => T0).

  Lemma mat0_eq_vec0_vec0 {r c} : mat0 = vec0 (vec0 T0 c) r.
  Proof.
    unfold mat0. unfold mmake.
    rewrite vmake_zero_eq_vec0. rewrite vmake_zero_eq_vec0. auto.
  Qed.

  Lemma mat0_S : forall {r c},
    @mat0 (S r) c = ((vec0 T0 c, @mat0 r c) : mat (S r) c).
  Proof.
    intros. rewrite mat0_eq_vec0_vec0. simpl. f_equal.
    rewrite mat0_eq_vec0_vec0. auto.
  Qed.

End mat0.

Arguments mat0 {T} _ {r c}.

(** ** Mapping matrix to matrix *)
Section mmap.

  Variable T : Type.
  Variable f : T -> T.

  Fixpoint mmap {r c}  : mat r c -> mat r c :=
    match r with
    | O => fun (m : mat 0 _) => tt
    | S r' => fun (m : mat (S r') c) => (vmap f (fst m), mmap (snd m))
    end.

End mmap.

Arguments mmap {T} f {r c}.

(** ** Mapping two matrices to another matrix *)
Section mmap2.

  Variable T : Type.
  Variable f : T -> T -> T.
  Variable f_comm : forall a b, f a b = f b a.
  Variable f_assoc : forall a b c, f (f a b) c = f a (f b c).

  Fixpoint mmap2 {r c}  : mat r c -> mat r c -> mat r c
    := match r with
    | O => fun (m1 m2 : mat 0 _) => tt
    | S r' => fun (m1 m2 : mat (S r') c) =>
      (vmap2 f (fst m1) (fst m2), mmap2 (snd m1) (snd m2))
    end.

  Lemma mmap2_comm {r c} (m1 m2 : mat r c) : mmap2 m1 m2 = mmap2 m2 m1.
  Proof.
    induction r,c; intros; destruct m1,m2; auto; simpl; f_equal; auto.
    f_equal;auto. apply vmap2_comm. auto.
  Qed.

  Lemma mmap2_assoc {r c} (m1 m2 m3 : mat r c) :
    mmap2 (mmap2 m1 m2) m3 = mmap2 m1 (mmap2 m2 m3).
  Proof.
    induction r,c; intros; destruct m1,m2; auto; simpl; f_equal; auto.
    f_equal;auto. apply vmap2_assoc. auto.
  Qed.

End mmap2.

Arguments mmap2 {T} f {r c}.
Arguments mmap2_comm {T} f f_comm {r c}.
Arguments mmap2_assoc {T} f f_assoc {r c}.

(** ** Construct a matrix with a vector and a a matrix *)
Section mcons.

  Variable T : Type.

  (** Construct by row *)
  Definition mconsr {r c} (v : @vec T c) (m : @vec (@vec T c) r)
    : @vec (@vec T c) (S r) :=
    (v, m).

  (** Construct by column *)
  Fixpoint mconsc {r c} : @vec T r -> @vec (@vec T c) r ->
    @vec (@vec T (S c)) r :=
    match r with
    | O => fun (v : vec 0) (m : mat 0 c) => tt
    | S r' => fun (v : vec (S r')) (m : mat (S r') c) =>
        ((fst v, fst m), mconsc (snd v) (snd m))
    end.

  (** Equality of two forms of ConstructByRow *)
  Lemma mconsr_eq {r c} (v : @vec T c) (m : @mat T r c) : mconsr v m = (v, m).
  Proof. unfold mconsr. auto. Qed.

  (** Construct a matrix by rows with the matrix which row number is 0 *)
  Lemma mconsr_mr0 : forall {n} (v : @vec T n) (m : @mat T 0 n),
    mconsr v m = [v].
  Proof. intros. destruct m. unfold mconsr. auto. Qed.

  (** Construct a matrix by rows with the matrix which row column is 0 *)
  Lemma mconsr_mc0 : forall {n} (v : @vec T 0) (m : @mat T n 0),
    mconsr v m = (tt, m).
  Proof. intros. destruct v. unfold mconsr. auto. Qed.

  (** Construct a matrix by columns with the matrix which row number is 0 *)
  Lemma mconsc_mr0 : forall {n} (v : @vec T 0) (m : @vec (@vec T n) 0),
    mconsc v m = tt.
  Proof. intros. destruct m. unfold mconsc. auto. Qed.

  (** Note that, mconsc_mc0 is in another section below, it need v2cm *)

End mcons.

Arguments mconsr {T r c}.
Arguments mconsc {T r c}.
Arguments mconsr_eq {T r c}.
Arguments mconsr_mr0 {T n}.
Arguments mconsr_mc0 {T n}.
Arguments mconsc_mr0 {T n}.

(** ** Get head row, tail rows, head column and tail columns of a matrix *)
Section mhd_mtl.

  Variable T : Type.
  Variable T0 : T.

  (** Get head row of a matrix *)
  Definition mhdr {r c} (m : @mat T (S r) c) : vec c := fst m.

  (** Get tail rows of a matrix *)
  Definition mtlr {r c} (m : @mat T (S r) c) : @mat T r c := snd m.

  (** Get head column of a matrix *)
  Fixpoint mhdc {r c} :  @mat T r (S c) -> vec r :=
    match r with
    | O => fun (m : mat 0 (S c)) => tt
    | S r' => fun (m : mat (S r') (S c)) =>
      (fst (fst m), mhdc (snd m))
    end.

  (** Get tail columns of a matrix *)
  Fixpoint mtlc {r c} : @mat T r (S c) -> @mat T r c :=
    match r with
    | O => fun (m : mat 0 (S c)) => tt
    | S r' => fun (m : mat (S r') (S c)) =>
      (snd (fst m), mtlc (snd m))
    end.

  Lemma mhdr_mtlr {r c} (m : @mat T (S r) c) : m = (mhdr m, mtlr m).
  Proof. destruct m. simpl. auto. Qed.

  Lemma mhdc_mtlc {r c} (m : @mat T r (S c)) : m = mconsc (mhdc m) (mtlc m).
  Proof.
    induction r; destruct m; simpl; auto. destruct v; simpl. f_equal; auto.
  Qed.

  Lemma mhdc_repeat_repeat : forall {r c} a,
    mhdc (vrepeat r (vrepeat (S c) a)) = vrepeat r a.
  Proof.
    induction r; intros; simpl; auto. f_equal.
    rewrite <- (IHr c). f_equal.
  Qed.

  (** Head row of a matrix which constructed by rows *)
  Lemma mhdr_mconsr : forall {r c} (v : @vec T c) (m : @mat T r c),
    mhdr (mconsr v m) = v.
  Proof. induction r; intros; destruct m; simpl; auto. Qed.

  (** Tail rows of a matrix which constructed by rows *)
  Lemma mtlr_mconsr : forall {r c} (v : @vec T c) (m : @mat T r c),
    mtlr (mconsr v m) = m.
  Proof. induction r; intros; destruct m; simpl; auto. Qed.

  (** Head column of a matrix which constructed by columns *)
  Lemma mhdc_mconsc : forall {r c} (v : @vec T r) (m : @mat T r c),
    mhdc (mconsc v m) = v.
  Proof. induction r; intros; destruct m,v; simpl; auto. f_equal. auto. Qed.

  (** Tail columns of a matrix which constructed by columns *)
  Lemma mtlc_mconsc : forall {r c} (v : @vec T r) (m : @mat T r c),
    mtlc (mconsc v m) = m.
  Proof. induction r; intros; destruct m,v; simpl; auto. f_equal. auto. Qed.

  (** mhdr (mat0) = vec0 *)
  Lemma mhdr_mat0 : forall {r c}, mhdr (@mat0 T T0 (S r) c) = vec0 T0 c.
  Proof.
    intros. simpl. rewrite vmake_zero_eq_vec0. auto.
  Qed.

  (** mhdc (mat0) = vec0 *)
  Lemma mhdc_mat0 : forall {r c}, mhdc (@mat0 T T0 r (S c)) = vec0 T0 r.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    rewrite vmake_zero_eq_vec0. rewrite vmake_aux_S.
    rewrite vmake_aux_zero_eq_vec0.
(*     rewrite mat0_eq_vec0_vec0. (* why fail? *) *)
    rewrite <- (IHr c). f_equal.
    rewrite mat0_eq_vec0_vec0. auto.
  Qed.

  (** mtlr (mat0) = mat0 *)
  Lemma mtlr_mat0 : forall {r c}, mtlr (@mat0 T T0 (S r) c) = mat0 T0.
  Proof.
    intros. simpl. rewrite vmake_zero_eq_vec0.
    rewrite vmake_aux_S. rewrite vmake_aux_zero_eq_vec0.
    rewrite mat0_eq_vec0_vec0. auto.
  Qed.

  (** mtlc (mat0) = mat0 *)
  Lemma mtlc_mat0 : forall {r c}, mtlc (@mat0 T T0 r (S c)) = mat0 T0.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    repeat rewrite vmake_aux_S.
    repeat rewrite vmake_zero_eq_vec0.
    repeat rewrite vmake_aux_zero_eq_vec0.
    replace (@mat0 T T0 (S r) c) with (vec0 T0 c, @mat0 T T0 r c).
    - f_equal; auto. rewrite <- (IHr c). f_equal.
      rewrite mat0_eq_vec0_vec0. auto.
    - rewrite mhdr_mtlr. f_equal.
      rewrite mhdr_mat0. auto. rewrite mtlr_mat0. auto.
  Qed.

End mhd_mtl.

Arguments mhdr {T r c}.
Arguments mtlr {T r c}.
Arguments mhdc {T r c}.
Arguments mtlc {T r c}.
Arguments mhdr_mtlr {T r c}.
Arguments mhdc_mtlc {T r c}.
Arguments mhdc_repeat_repeat {T r c}.
Arguments mhdr_mconsr {T r c}.
Arguments mtlr_mconsr {T r c}.
Arguments mhdc_mconsc {T r c}.
Arguments mtlc_mconsc {T r c}.

(** ** Unit matrix *)
Section mat1.

  Variable T : Type.
  Variable T0 T1 : T.

  Fixpoint mat1 n : mat n n :=
    match n with
    | O => let mat' : mat 0 0 := tt in mat'
    | S n' =>
      let row' : vec (S n') := (T1, vrepeat n' T0) in
      let mat' : mat n' n' := mat1 n' in
        mconsr row' (mconsc (vrepeat n' T0) mat')
    end.

  (* 一次实验，函数 vs 结构 *)
  (* 受 mat0 启发，另一种定义方式，说不定证明更加简洁 *)
  Definition mat1' n : mat n n :=
    mmake n n (fun ri ci => if ri =? ci then T1 else T0) .

  Lemma mat1_eq_mat1' : forall n, mat1 n = mat1' n.
  Proof.

    induction n.
    - simpl. unfold mat1'. unfold mmake. auto.
    - simpl. rewrite IHn.
      clear.
      (* a good start point, begin induction *)
      induction n.
      + simpl. auto.
      + simpl. (* ToDo: next time *) Abort.

(*     induction n.
    - simpl. unfold mat1'. unfold mmake. auto.
    - simpl. rewrite IHn.
      clear.
      (* a good start point *)
      unfold mat1' at 2.
      unfold mmake. unfold vmake. simpl.
      rewrite mconsr_eq. f_equal.
      + f_equal. rewrite vmake_aux_S. rewrite vmake_aux_zero_eq_vec0; auto.
      + Abort.

    induction n.
    - simpl. unfold mat1'. unfold mmake. auto.
    - simpl. rewrite IHn.
      clear.
      unfold mat1'.
      remember (fun ri ci : nat => if ri =? ci then T1 else T0) as f.
      unfold mmake. unfold vmake. simpl.
      rewrite mconsr_eq. f_equal.
      + f_equal. rewrite Heqf. auto. rewrite vmake_aux_S.
        rewrite <- vec0_eq_vrepeat0.
        replace (fun j : nat => f 0 (S j)) with (fun (_ : nat) => T0).
        * rewrite vmake_aux_zero_eq_vec0; auto.
        * apply functional_extensionality.
          intros. rewrite Heqf. auto.
      + rewrite vmake_aux_S.
        Abort. *)
End mat1.

Arguments mat1 {T}.
Arguments mat1' {T}.

(** ** Get row of a matrix as a vector *)
Section mrow.

  Variable T : Type.

  Definition mrow {r c} def ir (m : @mat T r c) : vec c :=
    vnth (vrepeat c def) ir m.

  Lemma mrow_0 {r c} def (m : @mat T (S r) c) : mrow def 0 m = mhdr m.
  Proof. destruct m. compute. auto. Qed.

  Lemma mrow_S {r c} def i (m : @mat T (S r) c) :
    mrow def (S i) m = mrow def i (mtlr m).
  Proof. destruct m. simpl. unfold mrow. auto. Qed.

End mrow.

Arguments mrow {T r c}.
Arguments mrow_0 {T r c}.
Arguments mrow_S {T r c}.

(** ** Get column of a matrix as a vector *)
Section mcol.

  Variable T : Type.

  Fixpoint mcol {r c} def (ic : nat) : @mat T r c -> vec r :=
    match r with
    | O => fun (m : mat 0 _) => tt
    | S r' => fun (m : mat (S r') c) =>
      (vnth def ic (fst m), mcol def ic (snd m))
    end.

  Lemma mcol_0 {r c} def (m : @mat T r (S c)) : mcol def 0 m = mhdc m.
  Proof.
    induction r; destruct m; simpl; auto. f_equal; auto.
  Qed.

  Lemma mcol_S {r c} def i (m : @mat T r (S c)) :
    mcol def (S i) m = mcol def i (mtlc m).
  Proof.
    induction r; destruct m; simpl; auto. f_equal; auto.
  Qed.

End mcol.

Arguments mcol {T r c}.
Arguments mcol_0 {T r c}.
Arguments mcol_S {T r c}.

(** Convert from a vector to a row matrix or column matrix, and convert the
 matrix back to a vector *)
Section v2m_m2v.

  Variable T : Type.
  Variable T0 : T.

  (** Type Conversion *)
  Definition vv2m {r c} (vv : @vec (@vec T c) r) : @mat T r c := vv.
  Definition m2vv {r c} (m : @mat T r c) : @vec (@vec T c) r := m.

  Lemma vv2m_eq : forall {r c} (vv : @vec (@vec T c) r), vv = vv2m vv.
  Proof. intros. auto. Qed.
  Lemma m2vv_eq : forall {r c} (m : @mat T r c), m = m2vv m.
  Proof. intros. auto. Qed.
  Lemma m2vv_vv2m_id : forall {r c} (vv : @vec (@vec T c) r),
    vv = m2vv (vv2m vv).
  Proof. intros. auto. Qed.
  Lemma vv2m_m2vv_id : forall {r c} (m : @mat T r c), m = vv2m (m2vv m).
  Proof. intros. auto. Qed.

  (** Convert a vector to a row matrix *)
  Definition v2rm {n} (v : @vec T n) : @mat T 1 n := [v].

  (** Convert a row matrix to a vector *)
  Definition rm2v {n} (m : @mat T 1 n) : @vec T n := fst m.

  (** Convert a vector to a column matrix *)
  Fixpoint v2cm {n} : @vec T n -> @mat T n 1 := match n with
  | O => fun (v : @vec T 0) => tt
  | S r' => fun (v : @vec T (S r')) => ([fst v], v2cm (snd v))
  end.

  (** Convert a column matrix to a vector *)
  Fixpoint cm2v {n} : @mat T n 1 -> @vec T n := match n with
  | O => fun (m : @mat T 0 1) => let v : @vec T 0 := tt in v
  | S r' => fun (m : @mat T (S r') 1) =>
    let v : @vec T (S r') :=
    (fst (fst m), cm2v (snd m)) in v
  end.

  Lemma v2rm_rm2v_id : forall {n} (m : @mat T 1 n), v2rm (rm2v m) = m.
  Proof. intros. induction n; destruct m; destruct v,m; simpl; auto. Qed.

  Lemma rm2v_v2rm_id : forall {n} (v : @vec T n), rm2v (v2rm v) = v.
  Proof. intros. induction n; destruct v; simpl; auto. Qed.

  Lemma v2cm_cm2v_id : forall {n} (m : @mat T n 1), v2cm (cm2v m) = m.
  Proof.
    intros. induction n; destruct m; simpl; auto. destruct v. destruct v.
    simpl. f_equal. auto.
  Qed.

  Lemma cm2v_v2cm_id : forall {n} (v : @vec T n), cm2v (v2cm v) = v.
  Proof. intros. induction n; destruct v; simpl; auto. f_equal. auto. Qed.

  Lemma rm2v_eq_mhdr : forall {n} (m : @mat T 1 n), rm2v m = mhdr m.
  Proof. intros. auto. Qed.

  Lemma cm2v_eq_mhdc : forall {n} (m : @mat T n 1), cm2v m = mhdc m.
  Proof. intros. induction n; destruct m; simpl; auto. f_equal. auto. Qed.

  Lemma mat_r1_ex_v2rm : forall {n} (m : @mat T 1 n), {v | m = v2rm v}.
  Proof.
    induction n; intros; destruct m; destruct v,m.
    - exists tt. auto.
    - exists (t,v). auto.
  Qed.

  Lemma mat_c1_ex_v2cm : forall {n} (m : @mat T n 1), {v | m = v2cm v}.
  Proof.
    induction n; intros; destruct m.
    - exists tt. auto.
    - exists (cm2v ((v,m) : mat (S n) 1)). simpl. f_equal.
      + destruct v. simpl. destruct v. auto.
      + rewrite v2cm_cm2v_id. auto.
  Qed.

  (** Construct a matrix by columns with the matrix which row column is 0 *)
  Lemma mconsc_mc0 : forall {n} (v : @vec T n) (m : @mat T n 0),
    mconsc v m = v2cm v.
  Proof.
    induction n; intros; destruct v,m; simpl; auto.
    destruct v0. f_equal. auto.
  Qed.

  (** v2cm (vec0) = mat0 *)
  Lemma v2cm_vec0_eq_mat0 : forall {n}, v2cm (@vec0 T T0 n) = @mat0 T T0 n 1.
  Proof.
    induction n; simpl; auto.
    unfold mat0. unfold mmake. rewrite vmake_zero_eq_vec0. simpl.
    rewrite vmake_S. f_equal.
    rewrite IHn. rewrite mat0_eq_vec0_vec0. f_equal.
  Qed.

  (** v2rm (vec0) = mat0 *)
  Lemma v2rm_vec0_eq_mat0 : forall {n}, v2rm (@vec0 T T0 n) = @mat0 T T0 1 n.
  Proof.
    intros. unfold v2rm. unfold mat0,mmake. rewrite vmake_zero_eq_vec0.
    rewrite vmake_zero_eq_vec0. simpl. auto.
  Qed.

End v2m_m2v.

Arguments v2rm {T n}.
Arguments rm2v {T n}.
Arguments v2cm {T n}.
Arguments cm2v {T n}.
Arguments v2rm_rm2v_id {T n}.
Arguments rm2v_v2rm_id {T n}.
Arguments v2cm_cm2v_id {T n}.
Arguments cm2v_v2cm_id {T n}.
Arguments rm2v_eq_mhdr {T n}.
Arguments cm2v_eq_mhdc {T n}.
Arguments mat_r1_ex_v2rm {T n}.
Arguments mat_c1_ex_v2cm {T n}.
Arguments mconsc_mc0 {T n}.

(** ** Append two matrix with same column number or row number *)
Section mapp.

  Variable T : Type.

  (** Append two matrix with same column number by row *)
  Definition mappr {r1 r2 c} (m1 : @mat T r1 c) (m2 : @mat T r2 c)
    : @mat T (r1 + r2) c := vapp m1 m2.

  (** Append two matrix with same row number by column *)
  Fixpoint mappc {r c1 c2} : @mat T r c1 -> @mat T r c2 -> @mat T r (c1 + c2)
    := match r with
    | O => fun _ _ => tt
    | S r' => fun (m1 : mat (S r') c1) (m2 : mat (S r') c2) =>
      (vapp (fst m1) (fst m2), mappc (snd m1) (snd m2))
    end.

End mapp.

Arguments mappr {T r1 r2 c}.
Arguments mappc {T r c1 c2}.

(** ** Split a matrix to two parts by row or column *)
Section msplit.

  Variable T : Type.

  (** Split a matrix to two parts by row *)
  Definition msplitr r1 r2 {c} def (m: @mat T (r1+r2) c)
    : (@mat T r1 c) * (@mat T (r1+r2-r1) c) :=
    (vfirstn (vrepeat c def) r1 m, vskipn r1 m).

  (** I can't write this lemma *)
(*   Lemma mappr_msplitr r1 r2 {c} def (m : @mat T (r1+r2) c) :
       mappr (msplitr r1 r2 def m) = m.
 *)
  (** Convert Type as well, but too complicated!! *)
  Definition cvtMatShape r1 r2 {c} (m1 : @mat T (r1 + r2 - r1) c)
    : @mat T r2 c.
  Proof.
    (* rewrite minus_plus in m1. *)
    rewrite Nat.add_comm in m1.
    rewrite Nat.add_sub in m1.
    exact m1.
  Defined.

  Definition msplitr' r1 r2 {c} def (m: @mat T (r1+r2) c)
    : (@mat T r1 c) * (@mat T r2 c) :=
      (vfirstn (vrepeat c def) r1 m, cvtMatShape r1 r2 (vskipn r1 m)).

  Lemma mappr_msplitr' r1 r2 {c} def (m : @mat T (r1+r2) c) :
    let '(m1,m2) := msplitr' r1 r2 def m in
    let m' : @mat T (r1+r2) c := mappr m1 m2 in
      m' = m.
  Proof.
    simpl. induction r1.
    - induction r2; destruct m; simpl.
      + unfold cvtMatShape. simpl (0+0-0). unfold eq_rect. Abort.

  (** Split a matrix to two parts by column *)
  Fixpoint msplitc {r} c1 c2 def :
    (@mat T r (c1+c2)) -> (@mat T r c1) * (@mat T r (c1+c2-c1)) :=
    match r with
    | O => fun (_ : mat 0 (c1+c2)) => (tt, tt)
    | S r' => fun (m : mat (S r') (c1+c2)) =>
      let defV : vec (c1+c2) := vrepeat (c1+c2) def in
      let (m1, m2) := msplitc c1 c2 def (vtl m) in
        ((vfirstn def c1 (vhd defV m), m1), (vskipn c1 (vhd defV m), m2))
    end.

End msplit.

Arguments msplitr {T} r1 r2 {c}.
Arguments msplitr' {T} r1 r2 {c}.
Arguments msplitc {T} {r} c1 c2.

(** matrix addition. m1(r,c) + m2(r,c) = m(r,c) *)
Section madd.
  Variable T : Type.
  Variable T0 : T.
  Variable fadd fmul : T -> T -> T.
  Variable fadd_comm : forall a b, fadd a b = fadd b a.
  Variable fmul_comm : forall a b, fmul a b = fmul b a.
  Variable fadd_assoc : forall a b c, fadd (fadd a b) c = fadd a (fadd b c).
  Variable fmul_assoc : forall a b c, fmul (fmul a b) c = fmul a (fmul b c).
  Variable fmul_fadd_dist_l : forall a b c,
    fmul a (fadd b c) = fadd (fmul a b) (fmul a c).
  Variable fmul_0_l : forall a, fmul T0 a = T0.
  Variable fadd_0_l : forall a, fadd T0 a = a.
  Variable fadd_0_r : forall a, fadd a T0 = a.

  Definition madd {r c} (m1 m2 : @mat T r c) : @mat T r c :=
    vmap2 (vadd fadd) m1 m2.

  Lemma madd_mconsc : forall {r c} (v1 v2 : @vec T r)
    (m1 m2 : @vec (@vec T c) r),
    madd (mconsc v1 m1) (mconsc v2 m2) = mconsc (vadd fadd v1 v2) (madd m1 m2).
  Proof. induction r; intros; simpl; auto. f_equal. auto. Qed.

  Lemma madd_comm : forall {r c} (m1 m2 : @mat T r c),
     madd m1 m2 = madd m2 m1.
  Proof. intros. apply vmap2_comm. apply vadd_comm; auto. Qed.

  Lemma madd_assoc : forall {r c} (m1 m2 m3 : @mat T r c),
     madd (madd m1 m2) m3 = madd m1 (madd m2 m3).
  Proof. intros. apply vmap2_assoc. apply vadd_assoc; auto. Qed.

  Lemma madd_0_l : forall {r c} (m : @mat T r c),
    madd (mat0 T0) m = m.
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal; auto.
    - rewrite vmake_zero_eq_vec0. apply vadd_0_l. auto.
    - rewrite vmake_zero_eq_vec0. rewrite vmake_aux_S.
      rewrite vmake_aux_zero_eq_vec0. rewrite <- mat0_eq_vec0_vec0. auto.
  Qed.

  Lemma madd_0_r : forall {r c} (m : @mat T r c),
    madd m (mat0 T0) = m.
  Proof.
    intros. rewrite madd_comm. apply madd_0_l.
  Qed.

End madd.

Arguments madd {T} _ {r c}.

(** matrix substraction. m1(r,c) - m2(r,c) = m(r,c) *)
Section msub.

  Variable T : Type.
  Variable T0 : T.
  Variable fopp : T -> T.
  Variable fadd fmul : T -> T -> T.
  Definition fsub a b := fadd a (fopp b).
  Infix "+" := fadd.
  Infix "-" := fsub.
  Notation "- a" := (fopp a).

  Variable fopp_opp : forall a, - (- a) = a.
  Variable fadd_comm : forall a b, a + b = b + a.
  Variable fadd_assoc : forall a b c, (a + b) + c = a + (b + c).
  Variable fadd_0_l : forall t, T0 + t = t.
  Variable fadd_0_r : forall t, t + T0 = t.
  Variable fadd_opp : forall a, a + (-a) = T0.
  Variable fopp_add_dist : forall a b, -(a+b) = -a + -b.
  Variable fopp_0 : - T0 = T0.

  (* 矩阵减法 *)
  Definition mopp {r c} (m : mat r c) : mat r c :=
    vmap (vopp fopp) m.

  Definition msub {r c} (m1 m2 : @mat T r c) : @mat T r c :=
    madd fadd m1 (mopp m2).
(*     vmap2 (vsub fsub) m1 m2. *)

  Lemma mopp_mopp : forall {r c} (m : mat r c), mopp (mopp m) = m.
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal; auto.
    apply vopp_vopp. auto.
  Qed.

  Lemma msub_comm : forall {r c} (m1 m2 : @mat T r c),
     msub m1 m2 = mopp (msub m2 m1).
  Proof.
    unfold msub.
    induction r; intros; simpl; auto.
    destruct m1,m2; simpl. f_equal; auto.
    apply vsub_comm; auto.
  Qed.

  Lemma msub_assoc : forall {r c} (m1 m2 m3 : @mat T r c),
     msub (msub m1 m2) m3 = msub m1 (madd fadd m2 m3).
  Proof.
    unfold msub.
    induction r; intros; simpl; auto.
    destruct m1,m2,m3; simpl. f_equal; auto.
    apply vsub_assoc; auto.
  Qed.

  Lemma msub_0_l : forall {r c} (m : mat r c), msub (mat0 T0) m = mopp m.
  Proof.
    unfold msub.
    induction r; intros; destruct m; simpl; auto. f_equal.
    - rewrite vmake_zero_eq_vec0. apply vsub_v0_l. auto.
    - rewrite vmake_zero_eq_vec0. rewrite vmake_aux_S.
      rewrite vmake_aux_zero_eq_vec0. rewrite <- mat0_eq_vec0_vec0. auto.
  Qed.

  Lemma msub_0_r : forall {r c} (m : mat r c), msub m (mat0 T0) = m.
  Proof.
    intros. rewrite msub_comm. rewrite msub_0_l. apply mopp_mopp.
  Qed.

  Lemma msub_self : forall {r c} (m : mat r c), msub m m = (mat0 T0).
  Proof.
    unfold msub.
    induction r; intros; destruct m; simpl; auto.
    rewrite mat0_S. f_equal; auto. apply vsub_self. auto.
  Qed.

End msub.

Arguments mopp {T} _ {r c}.
Arguments msub {T} _ _ {r c}.
Arguments msub_0_r {T}.

(* constant multiplied to a matrix *)
Section mcmul_mmulc.

  Variable T : Type.
  Variable T0 T1 : T.
  Variable fadd : T -> T -> T.
  Variable fmul : T -> T -> T.
  Variable fmul_comm : forall a b, fmul a b = fmul b a.
  Variable fmul_assoc : forall a b c, fmul (fmul a b) c = fmul a (fmul b c).

  Variable fmul_add_distr_l : forall a b1 b2,
    fmul a (fadd b1 b2) = fadd (fmul a b1) (fmul a b2).
  Variable fmul_add_distr_r : forall a1 a2 b,
    fmul (fadd a1 a2) b = fadd (fmul a1 b) (fmul a2 b).
  Variable fmul_1_l : forall a, fmul T1 a = a.
  Variable fmul_0_l : forall a, fmul T0 a = T0.

  Definition mcmul {r c : nat} a m : mat r c := mmap (fun x => fmul a x) m.
  Definition mmulc {r c : nat} m a : mat r c := mmap (fun x => fmul x a) m.

  Lemma mmulc_eq_mcmul : forall {r c} (a : T) (m : mat r c),
    mmulc m a = mcmul a m.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vmap_eq. auto.
  Qed.

  Lemma mcmul_assoc1 : forall {r c} (a b : T) (m : mat r c),
    mcmul a (mcmul b m) = mcmul (fmul a b) m.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vmap_assoc1. auto.
  Qed.

  Lemma mcmul_assoc2 : forall {r c} (a b : T) (m : mat r c),
    mcmul a (mcmul b m) = mcmul b (mcmul a m).
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vmap_assoc2. auto. intros. auto.
  Qed.

  Lemma mcmul_distr_l : forall {r c} (a : T) (m1 m2 : mat r c),
    mcmul a (madd fadd m1 m2) = madd fadd (mcmul a m1) (mcmul a m2).
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vmap_vadd_distr_l. auto.
  Qed.

  Lemma mcmul_distr_r : forall {r c} (a b : T) (m : mat r c),
    mcmul (fadd a b) m = madd fadd (mcmul a m) (mcmul b m).
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vmap_vadd_distr_r. auto.
  Qed.

  Lemma mcmul_1_l : forall {r c} (m : mat r c),
    mcmul T1 m = m.
  Proof.
    induction r; intros; simpl; auto. destruct m; auto. destruct m. simpl.
    f_equal; auto. apply vcmul_1_l. auto.
  Qed.

  Lemma mcmul_0_l : forall {r c} (m : mat r c),
    mcmul T0 m = mat0 T0.
  Proof.
    induction r; intros; simpl; auto. destruct m; auto. simpl.
    rewrite IHr. unfold mat0.
    rewrite mmake_row_S. f_equal.
    rewrite vmake_zero_eq_vec0. clear m.
    induction c; auto. simpl. f_equal; auto.
  Qed.

End mcmul_mmulc.

Arguments mcmul {T} fmul {r c}.
Arguments mmulc {T} fmul {r c}.

(* Transpose a matrix *)
Section mtrans.

  Variable T : Type.
  Variable T0 T1 : T.
  Variable fadd : T -> T -> T.

  Fixpoint mtrans {r c} : @mat T r c -> mat c r :=
    match c with
    | O => fun (m : @mat T r 0) => tt
    | S c' => fun (m : @mat T r (S c')) => (mhdc m, mtrans (mtlc m))
    end.

  (** Head row of a transposed matrix equal to Head column *)
  Lemma mhdr_mtrans_eq_mhdc {r c} (m : @mat T r (S c)) :
    mhdr (mtrans m) = mhdc m.
  Proof. unfold mhdr. induction r; simpl; auto. Qed.

  (** Tail rows of a transposed matrix equal to transposed tail columns *)
  Lemma mtlr_mtrans_eq_mtrans_mtlc {r c} (m : @mat T r (S c)) :
    mtlr (mtrans m) = mtrans (mtlc m).
  Proof. unfold mtlr. induction r; destruct m; simpl; auto. Qed.

  (** Head column of a transposed matrix equal to Head row *)
  Lemma mhdc_mtrans_eq_mhdr {r c} (m : @mat T (S r) c) :
    mhdc (mtrans m) = mhdr m.
  Proof.
    unfold mhdr. destruct m. simpl. induction c; destruct v; simpl; auto.
    f_equal. rewrite IHc. auto.
  Qed.

  (** Tail columns of a transposed matrix equal to transposed tail rows *)
  Lemma mtlc_mtrans_eq_mtrans_mtlr {r c} (m : @mat T (S r) c) :
    mtlc (mtrans m) = mtrans (mtlr m).
  Proof.
    unfold mtlr. induction c; destruct m; simpl; auto.
    f_equal. rewrite IHc. simpl. auto.
  Qed.

  (** Transpose twice return back *)
  Lemma mtrans_trans {r c} (m : @mat T r c) : mtrans (mtrans m) = m.
  Proof.
    generalize dependent c.
    induction r; intros; destruct m; auto. simpl.
    rewrite mhdc_mtrans_eq_mhdr. rewrite mtlc_mtrans_eq_mtrans_mtlr.
    rewrite IHr. simpl. auto.
  Qed.

  (** Transpose a matrix composed by head column and tail columns, equal to
    seperately transpose two part them append by row *)
  Lemma mtrans_hdc_tlc : forall {r c} (m : @mat T r (S c)),
    mtrans (mconsc (mhdc m) (mtlc m)) =
    (mhdr (mtrans m), mtlr (mtrans m)).
  Proof.
    intros. destruct r; destruct m; simpl; auto. repeat f_equal;
    rewrite mhdc_mtlc; auto.
  Qed.

  (** Transpose a matrix composed by head row and tail rows, equal to
    seperately transpose two part them append by column *)
  Lemma mtrans_hdr_tlr : forall {r c} (m : @mat T (S r) c),
    mtrans ((mhdr m, mtlr m) : @mat T (S r) c) =
    mconsc (mhdc (mtrans m)) (mtlc (mtrans m)).
  Proof.
    intros. rewrite <- (mtrans_trans m). rewrite <- mtrans_hdc_tlc.
    repeat rewrite mtrans_trans. auto.
  Qed.

  (** Transpose a zero rows matrix *)
  Lemma mtrans_r0 {n} (m : @mat T 0 n) : mtrans m = vec0 tt n.
  Proof. induction n; simpl; auto; f_equal; auto. Qed.

  (** Transpose a zero columns matrix *)
  Lemma mtrans_c0 {n} (m : @mat T n 0) : mtrans m = (tt : @mat T 0 n).
  Proof. induction n; simpl; auto. Qed.

  (** Transpose a one row matrix *)
  Lemma mtrans_r1 : forall {n} (m : @mat T 1 n), mtrans m = v2cm (rm2v m).
  Proof.
    induction n; intros; destruct m; simpl; auto. f_equal.
    destruct v; destruct m. simpl. rewrite IHn. f_equal.
  Qed.

  (** Transpose a one column matrix *)
  Lemma mtrans_c1 : forall {n} (m : @mat T n 1), mtrans m = v2rm (cm2v m).
  Proof.
    destruct n; intros; destruct m; simpl; auto.
    destruct v; destruct v. simpl. unfold v2rm. f_equal. f_equal.
    rewrite cm2v_eq_mhdc. auto.
  Qed.

  (** Transpose a one column matrix created by a vector *)
  Lemma mtrans_v2cm : forall {n} (v : @vec T n), mtrans (v2cm v) = v2rm v.
  Proof.
    destruct n; intros; destruct v; simpl; auto. unfold v2rm. f_equal.
    f_equal. rewrite <- cm2v_eq_mhdc. rewrite cm2v_v2cm_id. auto.
  Qed.

  (** Transpose a one row matrix created by a vector *)
  Lemma mtrans_v2rm : forall {n} (v : @vec T n), mtrans (v2rm v) = v2cm v.
  Proof.
    destruct n; intros; destruct v; simpl; auto. f_equal.
    rewrite mtrans_r1. simpl. auto.
  Qed.

  (** Transpose a matrix which splited by row *)
  Lemma mtrans_split_r : forall {r c} (v : @vec T c) (m : @vec (@vec T c) r),
    mtrans ((v, m) : mat (S r) c) = mconsc v (mtrans m).
  Proof.
    induction c; intros; destruct v; simpl; auto. f_equal. rewrite IHc. auto.
  Qed.

  (** Transpose a matrix which splited by column *)
  Lemma mtrans_split_c : forall {r c} (v : @vec T r) (m : @vec (@vec T c) r),
    mtrans (mconsc v m) = (v, mtrans m).
  Proof.
    destruct r; intros; destruct m,v; simpl; auto.
    rewrite mhdc_mconsc. f_equal. f_equal. f_equal. apply mtlc_mconsc.
  Qed.

  (** (m1 + m2)^T = m1^T + m2^T *)
  Lemma mtrans_madd {r c} (m1 m2 : @mat T r c)
    : mtrans (madd fadd m1 m2) = madd fadd (mtrans m1) (mtrans m2).
  Proof.
    induction r.
    - destruct m1,m2. simpl. rewrite mtrans_r0.
      induction c; simpl; f_equal; auto.
    - destruct m1 as [v1 m1], m2 as [v2 m2]. simpl.
      rewrite mtrans_split_r.
      unfold mat in *. repeat rewrite mtrans_split_r.
      rewrite madd_mconsc. f_equal. auto.
  Qed.

  (** mat0^T = mat0 *)
  Lemma mtrans_mat0 : forall {r c}, mtrans (@mat0 T T0 r c) = @mat0 T T0 c r.
  Proof.
    intros r c; generalize dependent r.
    induction c; intros; simpl.
    - rewrite mat_r0. auto.
    - replace (@mat0 T T0 (S c) r) with (vec0 T0 r, @mat0 T T0 c r).
      + f_equal; auto.
        * rewrite mhdc_mat0. auto.
        * rewrite mtlc_mat0. auto.
      + rewrite mhdr_mtlr. f_equal.
        rewrite mhdr_mat0; auto. rewrite mtlr_mat0; auto.
  Qed.

  (** mat1^T = mat1 *)
  Lemma mtrans_mat1 : forall {n}, mtrans (mat1 T0 T1 n) = mat1 T0 T1 n.
  Proof.
    induction n; simpl; auto.
    rewrite mhdc_mconsc. rewrite mtlc_mconsc.
    rewrite mconsr_eq. f_equal.
(*     Fail rewrite <- mtrans_split_c. *)
(*     Fail rewrite mtrans_split_r. *)
    rewrite <- mtrans_trans. rewrite mtrans_split_c. f_equal. f_equal. auto.
  Qed.

End mtrans.

Arguments mtrans {T r c}.
Arguments mhdr_mtrans_eq_mhdc {T r c}.
Arguments mtlr_mtrans_eq_mtrans_mtlc {T r c}.
Arguments mhdc_mtrans_eq_mhdr {T r c}.
Arguments mtlc_mtrans_eq_mtrans_mtlr {T r c}.
Arguments mtrans_trans {T r c}.
Arguments mtrans_hdc_tlc {T r c}.
Arguments mtrans_hdr_tlr {T r c}.
Arguments mtrans_r0 {T n}.
Arguments mtrans_c0 {T n}.
Arguments mtrans_r1 {T n}.
Arguments mtrans_c1 {T n}.
Arguments mtrans_v2cm {T n}.
Arguments mtrans_v2rm {T n}.
Arguments mtrans_split_r {T r c}.
Arguments mtrans_split_c {T r c}.
Arguments mtrans_madd {T} _ {r c}.

(** Inner product a vector and a matrix. v(c) *' m(r,c) = v(r) *)
Section vdotm.
  Variable T : Type.
  Variable T0 T1 : T.
  Variable fadd fmul : T -> T -> T.
  Variable fadd_comm : forall a b, fadd a b = fadd b a.
  Variable fadd_assoc : forall a b c, fadd (fadd a b) c = fadd a (fadd b c).
  Variable fadd_0_l : forall a, fadd T0 a = a.
  Variable fadd_0_r : forall a, fadd a T0 = a.
  Variable fmul_comm : forall a b, fmul a b = fmul b a.
  Variable fmul_assoc : forall a b c, fmul (fmul a b) c = fmul a (fmul b c).
  Variable fmul_0_l : forall a, fmul T0 a = T0.
  Variable fmul_0_r : forall a, fmul a T0 = T0.
  Variable fmul_1_r : forall a, fmul a T1 = a.
  Variable fmul_fadd_dist_l : forall a b c,
    fmul a (fadd b c) = fadd (fmul a b) (fmul a c).
  Variable fmul_fadd_dist_r : forall a b c,
    fmul (fadd a b) c = fadd (fmul a c) (fmul b c).

  Notation vdot := (vdot T0 fadd fmul).
  Notation vadd := (vadd fadd).
  Notation vcmul := (vcmul fmul).

  Fixpoint vdotm {r c} (v : @vec T c) : @mat T r c -> @vec T r :=
    match r with
    | O => fun (m : mat 0 _) => tt
    | S r' => fun (m : mat (S r') c) =>
      (vdot v (fst m), vdotm v (snd m))
    end.

  Lemma vdotm_c0 : forall {n} (v : vec 0) (m : mat n 0),
    vdotm v m = (vec0 T0 n).
  Proof.
    induction n; intros; destruct v; simpl; auto. f_equal.
    destruct m. simpl. auto.
  Qed.

  Lemma vdotm_r0 : forall {n} (v : vec n) (m : mat 0 n), vdotm v m = tt.
  Proof. induction n; intros; destruct v,m; simpl; auto. Qed.

  Lemma vdotm_v0 : forall {r c} (m : mat r c), vdotm (vec0 T0 c) m = vec0 T0 r.
  Proof.
    induction r; intros; destruct m; simpl; auto. rewrite IHr. f_equal.
    rewrite vdot_0_l; auto.
  Qed.

  Lemma vdotm_split : forall {r c} (v : vec c) (m : mat (S r) c),
    vdotm v m = (vdot v (mhdr m), vdotm v (mtlr m)).
  Proof. induction r; intros; simpl. f_equal. f_equal. Qed.

  Lemma vdotm_cons : forall {r c} a (v : vec c) (m : mat r (S c)),
    @vdotm r (S c) (a, v) m =
    vadd (vcmul a (mhdc m)) (vdotm v (mtlc m)).
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal. rewrite IHr.
    f_equal.
  Qed.

  Lemma vdotm_vcmul : forall {r c} a (v : vec c) (m : mat r c),
    vdotm (vcmul a v) m = vcmul a (vdotm v m).
  Proof.
    induction r; intros; destruct m; simpl; auto.
    unfold vcmul. f_equal.
    - rewrite <- vdot_vcmul_l; auto.
    - unfold vcmul in IHr. rewrite <- IHr. auto.
  Qed.

  Lemma vdotm_vadd : forall {r c} (v1 v2 : vec c) (m : mat r c),
    vdotm (vadd v1 v2) m = vadd (vdotm v1 m) (vdotm v2 m).
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal; auto.
    rewrite vdot_vadd_r; auto.
  Qed.

  Lemma vdotm_madd_distr_l : forall {r c} (v : vec r) (m1 m2 : mat c r),
    vdotm v (madd fadd m1 m2) = vadd (vdotm v m1) (vdotm v m2).
  Proof.
    intros r c. generalize dependent r.
    induction c; intros; destruct m1,m2; simpl; auto. f_equal; auto.
    apply vdot_vadd_l; auto.
  Qed.

  Lemma vdotm_madd_distr_r : forall {r c} (v1 v2 : vec r) (m : mat c r),
    vdotm (vadd v1 v2) m = vadd (vdotm v1 m) (vdotm v2 m).
  Proof.
    intros r c. generalize dependent r.
    induction c; intros; destruct m; simpl; auto. f_equal; auto.
    apply vdot_vadd_r; auto.
  Qed.

  (** 0 . m = 0 *)
  Lemma vdotm_0_l : forall {r c} (m : @mat T r c),
    vdotm (vec0 T0 c) m = vec0 T0 r.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    apply vdot_0_l; auto.
  Qed.

  (** v . 0 = 0 *)
  Lemma vdotm_0_r : forall {r c} (v : vec c),
    vdotm v (mat0 T0) = vec0 T0 r.
  Proof.
    induction r; intros; simpl; auto. f_equal; auto.
    - rewrite vmake_zero_eq_vec0. apply vdot_0_r; auto.
    - rewrite vmake_zero_eq_vec0. rewrite vmake_aux_S.
      rewrite vmake_aux_zero_eq_vec0.
      rewrite <- mat0_eq_vec0_vec0. apply IHr.
  Qed.

  (** v . 1 = v *)
  Lemma vdotm_1_r : forall {n} (v : vec n),
    vdotm v (mat1 T0 T1 n) = v.
  Proof.
    induction n; intros; destruct v; simpl; auto. f_equal; auto.
    - rewrite vdot_S. rewrite vdot_0_r; auto.
      rewrite fmul_1_r. auto.
    - rewrite vdotm_cons. rewrite mtlc_mconsc. rewrite mhdc_mconsc.
      rewrite IHn. rewrite <- vec0_eq_vrepeat0.
      rewrite vcmul_0_r; auto. rewrite vadd_0_l; auto.
  Qed.

End vdotm.

Arguments vdotm {T} T0 fadd fmul {r c}.
Arguments vdotm_c0 {T} T0 fadd fmul {n}.
Arguments vdotm_r0 {T} T0 fadd fmul {n}.
Arguments vdotm_0_l {T} T0 fadd fmul fadd_0_r fmul_0_l {r c}.
Arguments vdotm_0_r {T} T0 fadd fmul fadd_0_r fmul_comm fmul_0_l {r c}.
Arguments vdotm_split {T} T0 fadd fmul {r c}.
Arguments vdotm_cons {T} T0 fadd fmul {r c}.
Arguments vdotm_vcmul {T} T0 fadd fmul fmul_comm fmul_assoc fmul_0_l
  fmul_fadd_dist_l {r c}.
Arguments vdotm_vadd {T} T0 fadd fmul fadd_comm fadd_assoc
  fadd_0_r fmul_comm fmul_fadd_dist_l {r c}.

(** Inner product two matrix. m(r1,c) *' (m(r2,c) = m(r1,r2) *)
Section mdot.
  Variable T : Type.
  Variable T0 T1 : T.
  Variable fadd fmul : T -> T -> T.
  Variable fadd_comm : forall a b, fadd a b = fadd b a.
  Variable fmul_comm : forall a b, fmul a b = fmul b a.
  Variable fadd_assoc : forall a b c, fadd (fadd a b) c = fadd a (fadd b c).
  Variable fmul_assoc : forall a b c, fmul (fmul a b) c = fmul a (fmul b c).
  Variable fmul_fadd_dist_l : forall a b c,
    fmul a (fadd b c) = fadd (fmul a b) (fmul a c).
  Variable fmul_0_l : forall a, fmul T0 a = T0.
  Variable fadd_0_l : forall a, fadd T0 a = a.
  Variable fadd_0_r : forall a, fadd a T0 = a.

  Notation vdotm := (vdotm T0 fadd fmul).
  Notation vdot := (vdot T0 fadd fmul).
  Notation vadd := (vadd fadd).
  Notation vcmul := (vcmul fmul).

  Fixpoint mdot {r c t} : (@mat T r c) -> (@mat T t c) -> (@mat T r t) :=
    match r with
    | O => fun (m1 : mat 0 _) m2 => tt
    | S r' => fun (m1 : mat (S r') _) m2 =>
      (vdotm (fst m1) m2, mdot (snd m1) m2)
    end.

  Lemma vdotm_comm_mdot : forall {r c} (v : vec c) (m : @mat T r c),
    vdotm v m = cm2v (mdot m (v2rm v)).
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal; auto.
    apply vdot_comm; auto.
  Qed.

  Lemma mhdc_mdot_eq_vdotm {r c t} (v : vec c) (m1 : mat r c) (m2 : mat t c)
    : mhdc (@mdot t c (S r) m2 (v, m1)) = vdotm v m2.
  Proof.
    induction t; destruct m2; simpl; auto. f_equal; auto.
    apply vdot_comm. auto.
  Qed.

  (* mtlc (mdot m1 m2) = mdot m1 (mtlr m2). *)
  Lemma mtlc_mdot : forall {r c t} (m1 : mat r c) (m2 : mat (S t) c),
    mtlc (mdot m1 m2) = mdot m1 (mtlr m2).
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal. apply IHr.
  Qed.

  Lemma mdot_split_l {r c t} (v : vec c) (m1 : mat r c) (m2 : mat t c) :
    @mdot (S r) c t (v, m1) m2 =
    mconsr (vdotm v m2) (mdot m1 m2).
  Proof. induction r; destruct m1; simpl; auto. Qed.

  Lemma mdot_split_r {r c t} (v : vec c) (m1 : mat r c) (m2 : mat t c) :
    @mdot r c (S t) m1 (v, m2) =
    mconsc (cm2v (mdot m1 (v2rm v))) (mdot m1 m2).
  Proof. induction r; destruct m1; simpl; auto. f_equal. auto. Qed.

  Lemma mdot_comm : forall {r c t} (m1 : @mat T r c) (m2 : @mat T t c),
    mdot m1 m2 = mtrans (mdot m2 m1).
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal.
    - rewrite mhdc_mdot_eq_vdotm. auto.
    - rewrite IHr. f_equal. rewrite mtlc_mdot. f_equal.
  Qed.

  Lemma mdot_tt : forall {r c} (m1 : mat r 0) (m2 : mat c 0),
    mdot m1 m2 = vrepeat r (vec0 T0 c).
  Proof.
    induction r; intros; destruct m1; simpl; auto. rewrite IHr; f_equal.
    destruct v. rewrite vdotm_c0. auto.
  Qed.

  (** Head row for a mdot of (v,M1) and M2, equal to v dot M2 *)
  Lemma mhdr_mdot : forall {r c t} (v : vec c) (m1 : mat r c) (m2 : mat t c),
    mhdr (mdot ((v, m1) : mat (S r) c) m2) = vdotm v m2.
  Proof.
    induction r; intros; destruct m1; simpl; auto.
  Qed.

  (** Head column for a mdot of M1 and (v,M2), equal to v dot M1 *)
  Lemma mhdc_mdot : forall {r c t} (m1 : mat r c) (v : vec c) (m2 : mat t c),
    mhdc (mdot m1 ((v, m2) : mat (S t) c)) = vdotm v m1.
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal; auto.
    apply vdot_comm; auto.
  Qed.

  Lemma vdotm_assoc : forall {r c t} (v : vec r) (m2 : mat c r) (m3 : mat t c),
    vdotm (vdotm v m2) m3 = vdotm v (mdot m3 (mtrans m2)).
  Proof.
    induction r; intros; destruct v; simpl.
    - repeat rewrite vdotm_v0; auto.
    - rewrite vdotm_cons. rewrite vdotm_vadd; auto.
      rewrite vdotm_cons. f_equal.
      + rewrite vdotm_vcmul; auto. f_equal. rewrite mhdc_mdot. auto.
      + rewrite mtlc_mdot. simpl. auto.
  Qed.

  Lemma mdot_assoc :  forall {r c t s} (m1 : @mat T r c) (m2 : @mat T t c)
    (m3 : @mat T s t), mdot (mdot m1 m2) m3 = mdot m1 (mdot m3 (mtrans m2)).
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal; auto.
    apply vdotm_assoc.
  Qed.

  Lemma mdot_madd_distr_l : forall {r c t} (m1 : @mat T r c)
    (m2 m3 : @mat T t c),
    mdot m1 (madd fadd m2 m3) = madd fadd (mdot m1 m2) (mdot m1 m3).
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal; auto.
    apply vdotm_madd_distr_l; auto.
  Qed.

  Lemma mdot_madd_distr_r : forall {r c t} (m1 m2 : @mat T r c)
    (m3 : @mat T t c),
    mdot (madd fadd m1 m2) m3 = madd fadd (mdot m1 m3) (mdot m2 m3).
  Proof.
    induction r; intros; destruct m1; simpl; auto. f_equal; auto.
    apply vdotm_madd_distr_r; auto.
  Qed.

  Lemma mdot_0_r : forall {r c t} (m : @mat T r c),
    mdot m (@mat0 T T0 t c) = mat0 T0.
  Proof.
    induction r; intros; destruct m; simpl.
    - rewrite mat_r0; auto.
    - replace (@mat0 T T0 (S r) t) with (vec0 T0 t, @mat0 T T0 r t).
      + f_equal; auto. apply vdotm_0_r; auto.
      + rewrite mat0_S. auto.
  Qed.

  Lemma mdot_0_l : forall {r c t} (m : @mat T t c),
    mdot (@mat0 T T0 r c) m = mat0 T0.
  Proof.
    intros. rewrite mdot_comm. rewrite mdot_0_r.
    rewrite mtrans_mat0. auto.
  Qed.
  (*
  Lemma mdot_1_l : forall {r c} (m : @mat T r c),
    mdot (mat1 T0 T1 c) m = m.
  Proof.
    induction r; intros; destruct m; simpl.
    - rewrite mat_r0; auto.
    - replace (@mat0 T T0 (S r) t) with (vec0 T0 t, @mat0 T T0 r t).
      + f_equal; auto. apply vdotm_0_r; auto.
      + rewrite mat0_S. auto.
  Qed.

  Lemma mdot_0_l : forall {r c t} (m : @mat T t c),
    mdot (@mat0 T T0 r c) m = mat0 T0.
  Proof.
    intros. rewrite mdot_comm. rewrite mdot_0_r.
    rewrite mtrans_mat0. auto.
  Qed.

  mdot T0 fadd fmul m (mat1 T0 T1 c) = m *)

End mdot.

Arguments mdot {T} T0 fadd fmul {r c t}.
Arguments vdotm_comm_mdot {T} T0 fadd fmul fmul_comm {r c}.
Arguments mhdc_mdot_eq_vdotm {T} T0 fadd fmul fmul_comm {r c t}.
Arguments mtlc_mdot {T} T0 fadd fmul {r c t}.
Arguments mdot_split_l {T} T0 fadd fmul {r c t}.
Arguments mdot_split_r {T} T0 fadd fmul {r c t}.
Arguments mdot_comm {T} T0 fadd fmul fmul_comm {r c t}.
Arguments mdot_tt {T} T0 fadd fmul {r c}.
Arguments mhdr_mdot {T} T0 fadd fmul {r c}.
Arguments mhdc_mdot {T} T0 fadd fmul fmul_comm {r c t}.
Arguments vdotm_assoc {T} T0 fadd fmul fadd_comm fmul_comm
  fadd_assoc fmul_assoc fmul_fadd_dist_l fmul_0_l fadd_0_r {r c t}.
Arguments mdot_assoc {T} T0 fadd fmul fadd_comm fmul_comm
  fadd_assoc fmul_assoc fmul_fadd_dist_l fmul_0_l fadd_0_r {r c t}.

(** matrix multiplication. m1(r,c) * m2(c,t) = m(r,t) *)
Section mmul.

  Variable T : Type.
  Variable T0 T1 : T.
  Variable fadd fmul : T -> T -> T.
  Variable fadd_comm : forall a b, fadd a b = fadd b a.
  Variable fadd_assoc : forall a b c, fadd (fadd a b) c = fadd a (fadd b c).
  Variable fadd_0_l : forall a, fadd T0 a = a.
  Variable fadd_0_r : forall a, fadd a T0 = a.
  Variable fmul_comm : forall a b, fmul a b = fmul b a.
  Variable fmul_assoc : forall a b c, fmul (fmul a b) c = fmul a (fmul b c).
  Variable fmul_fadd_dist_l : forall a b c,
    fmul a (fadd b c) = fadd (fmul a b) (fmul a c).
  Variable fmul_0_l : forall a, fmul T0 a = T0.
  Variable fmul_0_r : forall a, fmul a T0 = T0.
  Variable fmul_1_l : forall a, fmul T1 a = a.
  Variable fmul_1_r : forall a, fmul a T1 = a.

  Definition mmul {r c s} (m1 : @mat T r c) (m2 : @mat T c s) : @mat T r s :=
    mdot T0 fadd fmul m1 (mtrans m2).

  Lemma mmul_trans {r c s} (m1 : @mat T r c) (m2 : @mat T c s)
    : mtrans (mmul m1 m2) = mmul (mtrans m2) (mtrans m1).
  Proof.
    unfold mmul. rewrite <- mdot_comm;auto. rewrite mtrans_trans; auto.
  Qed.

  Lemma mmul_assoc {r c s t} (m1 : @mat T r c) (m2 : @mat T c s)
    (m3 : @mat T s t) : mmul (mmul m1 m2) m3 = mmul m1 (mmul m2 m3).
  Proof.
    unfold mmul. rewrite <- mdot_comm; auto.
    rewrite mdot_assoc; auto. f_equal. f_equal. rewrite mtrans_trans. auto.
  Qed.

  Lemma mmul_madd_distr_l : forall {r c s} (m1 : mat r c) (m2 m3 : mat c s),
    mmul m1 (madd fadd m2 m3) = madd fadd (mmul m1 m2) (mmul m1 m3).
  Proof.
    intros. unfold mmul. rewrite mtrans_madd.
    rewrite mdot_madd_distr_l; auto.
  Qed.

  Lemma mmul_madd_distr_r : forall {r c s} (m1 m2 : mat r c) (m3 : mat c s),
    mmul (madd fadd m1 m2) m3 = madd fadd (mmul m1 m3) (mmul m2 m3).
  Proof.
    intros. unfold mmul.
    rewrite mdot_madd_distr_r; auto.
  Qed.

  Lemma mmul_consr_l : forall {r c s} (v1 : vec c) (m1 : mat r c)
    (m2 : mat c s),
    mmul ((v1, m1) : mat (S r) c) m2 =
    (vdotm T0 fadd fmul v1 (mtrans m2), mmul m1 m2).
  Proof.
    intros. unfold mmul. rewrite mdot_split_l. rewrite mconsr_eq. auto.
  Qed.

  (* a difficult lemma *)
  (** (v1 | m1) x (v2 / m2) = [v1^T]x[v2] + m1 x m2 *)
  Lemma mmul_consc_consr : forall {r c s} (v1 : vec r) (m1 : mat r c)
    (v2 : vec s) (m2 : mat c s),
    mmul (mconsc v1 m1) (mconsr v2 m2) =
    madd fadd (mmul (v2cm v1) (v2rm v2)) (mmul m1 m2).
  Proof.
    unfold mmul.
    induction r.
    - intros; simpl; auto.
    - induction c.
      + intros; simpl. destruct v1,m1,m2. destruct v0. simpl.
        rewrite vdotm_0_l; auto. rewrite vadd_0_r; auto. f_equal.
        rewrite IHr. auto.
      + intros; simpl. destruct v1,m1,m2. destruct v0. f_equal; simpl.
        * rewrite vdotm_cons. rewrite vdotm_cons.
          repeat rewrite mhdc_mtrans_eq_mhdr.
          unfold v2rm. simpl.
          rewrite mtlc_mtrans_eq_mtrans_mtlr. simpl.
          rewrite vdotm_0_l; auto.
          rewrite vadd_0_r; auto.
          rewrite (@vdotm_cons T T0 fadd fmul s (S c) t (t0,v0)).
          rewrite mhdc_mtrans_eq_mhdr. simpl. f_equal.
          rewrite mtlc_mtrans_eq_mtrans_mtlr.
          rewrite mtlr_mconsr.
          rewrite vdotm_cons.
          rewrite mhdc_mtrans_eq_mhdr, mtlc_mtrans_eq_mtrans_mtlr. simpl.
          auto.
        * auto.
  Qed.

  Lemma mmul_0_l : forall {r c t} (m : mat c t),
    mmul (@mat0 T T0 r c) m = mat0 T0.
  Proof.
    intros. unfold mmul. rewrite mdot_0_l; auto.
  Qed.

  Lemma mmul_0_r : forall {r c t} (m : mat r c),
    mmul m (@mat0 T T0 c t) = mat0 T0.
  Proof.
    intros. unfold mmul. rewrite mtrans_mat0. rewrite mdot_0_r; auto.
  Qed.

  Lemma mmul_1_r : forall {r c} (m : mat r c), mmul m (mat1 T0 T1 c) = m.
  Proof.
    induction r; intros; destruct m; simpl; auto.
    rewrite mmul_consr_l. f_equal; auto.
    rewrite mtrans_mat1. rewrite vdotm_1_r; auto.
  Qed.

  Lemma mmul_1_l : forall {r c} (m : mat r c), mmul (mat1 T0 T1 r) m = m.
  Proof.
    induction r; intros; destruct m; simpl; auto.
    rewrite mconsr_eq. rewrite mmul_consr_l. f_equal; auto.
    - rewrite vdotm_cons. rewrite <- vec0_eq_vrepeat0.
      rewrite vdotm_0_l; auto.
      rewrite vadd_0_r; auto.
      rewrite vcmul_1_l; auto.
      rewrite mhdc_mtrans_eq_mhdr. auto.
    - rewrite <- mconsr_eq. rewrite mmul_consc_consr.
      replace (mmul (v2cm (vrepeat r T0)) (v2rm v)) with (@mat0 T T0 r c).
      + rewrite IHr. rewrite madd_0_l; auto.
      + rewrite <- vec0_eq_vrepeat0.
        rewrite v2cm_vec0_eq_mat0. rewrite mmul_0_l. auto.
  Qed.

End mmul.

Arguments mmul {T} T0 fadd fmul {r c s}.
Arguments mmul_trans {T} T0 fadd fmul fmul_comm {r c s}.
Arguments mmul_assoc {T} T0 fadd fmul fadd_comm fadd_assoc
  fadd_0_r fmul_comm fmul_assoc fmul_fadd_dist_l fmul_0_l {r c s}.

(** ** Row-vector multiply a matrix, or matrix multiply column-vector.
  1. v(r) converted to mv(1,r)
  2. v(r) * m(r,c) = mv(1,r) * m(r,c) = m'(1,c) *)
Section vmulm_mmulv.

  Variable T : Type.
  Variable T0 : T.
  Variable fadd fmul : T -> T -> T.

  Definition vmulm {r c} (v : @vec T r) (m : @mat T r c) : (@mat T 1 c) :=
    mmul T0 fadd fmul (v2rm v) m.

  Definition mmulv {r c} (m : @mat T r c) (v : @vec T c) : @mat T r 1:=
    mmul T0 fadd fmul m (v2cm v).

End vmulm_mmulv.

Arguments vmulm {T} T0 fadd fmul {r c}.
Arguments mmulv {T} T0 fadd fmul {r c}.

(** Matrix to list list *)
Section m2l.

  Variable A : Type.
  Variable A0 : A.

  Fixpoint m2l {r c} : (@mat A r c) -> list (list A) :=
    match r with
    | O => fun (m : @vec (@vec A c) 0) => nil
    | S r' => fun (m : @vec (@vec A c) (S r')) =>
      cons (v2l (fst m)) (m2l (snd m))
    end.

  Fixpoint l2m (dl : list (list A)) (r c : nat) {struct r} : @mat A r c :=
    match r as r0 return (@vec (@vec A c) r0) with
    | 0 => tt
    | S n' => (l2v A0 (hd nil dl) c, l2m (tl dl) n' c)
    end.

  Lemma m2l_l2m_id : forall {r c} (dl : list (list A)) (H1 : length dl = r)
    (H2 : width dl c), m2l (l2m dl r c) = dl.
  Proof.
    unfold m2l,l2m. induction r; intros; simpl.
    - apply length_zero_iff_nil in H1; auto.
    - rewrite IHr; auto.
      + rewrite v2l_l2v_id; auto.
        * destruct dl; simpl in *; auto. lia.
        * destruct dl; simpl in *; auto. lia. destruct H2; auto.
      + destruct dl; simpl in *; auto. lia.
      + destruct dl; simpl in *; auto. destruct H2; auto.
  Qed.

  Lemma l2m_m2l_id : forall {r c} (m : mat r c), l2m (m2l m) r c = m.
  Proof.
    induction r; intros; destruct m; simpl; auto. f_equal; auto.
    apply l2v_v2l_id.
  Qed.

End m2l.

Arguments m2l {A r c}.
Arguments l2m {A} A0 dl r c.

author: zhengpushi

repo: coq-matrix

save_path: github-repos/coq/zhengpushi-coq-matrix


text:
(* This file is an automatic translation, the licence of the source can be found here: *)
(* https://github.com/herd/herdtools7/blob/master/LICENSE.txt *)
(* Translation of model Model pretty print *)
From Coq Require Import Relations Ensembles String.
From RelationAlgebra Require Import lattice prop monoid rel kat.
From Catincoq.lib Require Import Cat proprel.
Section Model.
Variable c : candidate.
Definition events := events c.
Definition R := R c.
Definition W := W c.
Definition IW := IW c.
Definition FW := FW c.
Definition B := B c.
Definition RMW := RMW c.
Definition F := F c.
Definition rf := rf c.
Definition po := po c.
Definition int := int c.
Definition ext := ext c.
Definition loc := loc c.
Definition addr := addr c.
Definition data := data c.
Definition ctrl := ctrl c.
Definition amo := amo c.
Definition rmw := rmw c.
Definition unknown_set := unknown_set c.
Definition unknown_relation := unknown_relation c.
Definition M := R ⊔ W.
Definition emptyset : set events := empty.
Definition classes_loc : set events -> Ensemble (Ensemble events) := partition loc.
Definition X := unknown_set "X".
Definition tag2events := unknown_relation "tag2events".
Definition emptyset_0 : set events := domain 0.
Definition partition := classes_loc.
Definition tag2instrs := tag2events.
Definition po_loc := po ⊓ loc.
Definition rfe := rf ⊓ ext.
Definition rfi := rf ⊓ int.
Definition co0 := loc ⊓ ([IW] ⋅ top ⋅ [(W ⊓ !IW)] ⊔ [(W ⊓ !FW)] ⋅ top ⋅ [FW]).
Definition toid (s : set events) : relation events := [s].
Definition fencerel (B : set events) := (po ⊓ [top] ⋅ top ⋅ [B]) ⋅ po.
Definition ctrlcfence (CFENCE : set events) := (ctrl ⊓ [top] ⋅ top ⋅ [CFENCE]) ⋅ po.
Definition imply (A : relation events) (B : relation events) := !A ⊔ B.
Definition nodetour (R1 : relation events) (R2 : relation events) (R3 : relation events) := R1 ⊓ !(R2 ⋅ R3).
Definition singlestep (R : relation events) := nodetour R R R.
(* Definition of map already included in the prelude *)
Definition LKW := (*failed: try LKW with emptyset_0*) emptyset_0.
Definition A := ((*successful: try X with emptyset_0*) X) ⊔ ((*failed: try A with emptyset_0*) emptyset_0).
Definition P := M ⊓ !A.
Definition WW r := r ⊓ [W] ⋅ top ⋅ [W].
Definition WR r := r ⊓ [W] ⋅ top ⋅ [R].
Definition RW r := r ⊓ [R] ⋅ top ⋅ [W].
Definition RR r := r ⊓ [R] ⋅ top ⋅ [R].
Definition RM r := r ⊓ [R] ⋅ top ⋅ [M].
Definition MR r := r ⊓ [M] ⋅ top ⋅ [R].
Definition WM r := r ⊓ [W] ⋅ top ⋅ [M].
Definition MW r := r ⊓ [M] ⋅ top ⋅ [W].
Definition MM r := r ⊓ [M] ⋅ top ⋅ [M].
Definition AA r := r ⊓ [A] ⋅ top ⋅ [A].
Definition AP r := r ⊓ [A] ⋅ top ⋅ [P].
Definition PA r := r ⊓ [P] ⋅ top ⋅ [A].
Definition PP r := r ⊓ [P] ⋅ top ⋅ [P].
Definition AM r := r ⊓ [A] ⋅ top ⋅ [M].
Definition MA r := r ⊓ [M] ⋅ top ⋅ [A].
Definition noid r : relation events := r ⊓ !id.
Definition atom := [A].
Definition obsco := WW po_loc ⊔ (rf ⋅ RW po_loc ⊔ (noid (WR po_loc ⋅ rf°) ⊔ noid (rf ⋅ (RR po_loc ⋅ rf°)))).
Definition cobase := obsco ⊔ co0.
Definition uniproc := acyclic cobase.
Definition co := cobase^+.
Definition fr := noid (rf° ⋅ co).
Definition coi := co ⊓ int.
Definition fri := fr ⊓ int.
Definition coe := co ⊓ !coi.
Definition fre := fr ⊓ !fri.
Definition dd := addr ⊔ data.
Definition rdw := po_loc ⊓ fre ⋅ rfe.
Definition detour := po_loc ⊓ coe ⋅ rfe.
Definition addrpo := addr ⋅ po.
Definition dmb_st : relation events := (*failed: try fencerel DMB.ST with 0*) 0.
Definition dsb_st : relation events := (*failed: try fencerel DSB.ST with 0*) 0.
Definition dmb : relation events := (*failed: try fencerel DMB with 0*) 0.
Definition dsb : relation events := (*failed: try fencerel DSB with 0*) 0.
Definition isb : relation events := (*failed: try fencerel ISB with 0*) 0.
Definition ctrlisb : relation events := (*failed: try ctrlcfence ISB with 0*) 0.
Definition sync : relation events := (*failed: try fencerel SYNC with 0*) 0.
Definition lwsync : relation events := (*failed: try fencerel LWSYNC with 0*) 0.
Definition eieio : relation events := (*failed: try fencerel EIEIO with 0*) 0.
Definition isync : relation events := (*failed: try fencerel ISYNC with 0*) 0.
Definition ctrlisync : relation events := (*failed: try ctrlcfence ISYNC with 0*) 0.
Definition ci0 := ctrlisync ⊔ (ctrlisb ⊔ detour).
Definition ii0 := dd ⊔ (rfi ⊔ rdw).
Definition cc0 := dd ⊔ (po_loc ⊔ (ctrl ⊔ addrpo)).
Definition ic0 : relation events := 0.
Inductive ci : relation _ := ci_c : incl (ci0 ⊔ (ci ⋅ ii ⊔ cc ⋅ ci)) ci
     with ii : relation _ := ii_c : incl (ii0 ⊔ (ci ⊔ (ic ⋅ ci ⊔ ii ⋅ ii))) ii
     with cc : relation _ := cc_c : incl (cc0 ⊔ (ci ⊔ (ci ⋅ ic ⊔ cc ⋅ cc))) cc
     with ic : relation _ := ic_c : incl (ic0 ⊔ (ii ⊔ (cc ⊔ (ic ⋅ cc ⊔ ii ⋅ ic)))) ic.
Section scheme.
Variables ci' ii' cc' ic' : relation events.
Variable Hci' : incl (ci0 ⊔ (ci' ⋅ ii' ⊔ cc' ⋅ ci')) ci'.
Variable Hii' : incl (ii0 ⊔ (ci' ⊔ (ic' ⋅ ci' ⊔ ii' ⋅ ii'))) ii'.
Variable Hcc' : incl (cc0 ⊔ (ci' ⊔ (ci' ⋅ ic' ⊔ cc' ⋅ cc'))) cc'.
Variable Hic' : incl (ic0 ⊔ (ii' ⊔ (cc' ⊔ (ic' ⋅ cc' ⊔ ii' ⋅ ic')))) ic'.

  Fixpoint ci_ind' x y (r : ci x y) : ci' x y
      with ii_ind' x y (r : ii x y) : ii' x y
      with cc_ind' x y (r : cc x y) : cc' x y
      with ic_ind' x y (r : ic x y) : ic' x y.
  Proof.
    destruct r as [x y r]; apply Hci'.
    destruct r as [r | r]; [ left | right ].
     exact r.
     destruct r as [r | r]; [ left | right ].
      destruct r as [x_y r1 r2]; exists x_y.
       apply ci_ind'; exact r1.
       apply ii_ind'; exact r2.
      destruct r as [x_y r1 r2]; exists x_y.
       apply cc_ind'; exact r1.
       apply ci_ind'; exact r2.
    destruct r as [x y r]; apply Hii'.
    destruct r as [r | r]; [ left | right ].
     exact r.
     destruct r as [r | r]; [ left | right ].
      apply ci_ind'; exact r.
      destruct r as [r | r]; [ left | right ].
       destruct r as [x_y r1 r2]; exists x_y.
        apply ic_ind'; exact r1.
        apply ci_ind'; exact r2.
       destruct r as [x_y r1 r2]; exists x_y.
        apply ii_ind'; exact r1.
        apply ii_ind'; exact r2.
    destruct r as [x y r]; apply Hcc'.
    destruct r as [r | r]; [ left | right ].
     exact r.
     destruct r as [r | r]; [ left | right ].
      apply ci_ind'; exact r.
      destruct r as [r | r]; [ left | right ].
       destruct r as [x_y r1 r2]; exists x_y.
        apply ci_ind'; exact r1.
        apply ic_ind'; exact r2.
       destruct r as [x_y r1 r2]; exists x_y.
        apply cc_ind'; exact r1.
        apply cc_ind'; exact r2.
    destruct r as [x y r]; apply Hic'.
    destruct r as [r | r]; [ left | right ].
     exact r.
     destruct r as [r | r]; [ left | right ].
      apply ii_ind'; exact r.
      destruct r as [r | r]; [ left | right ].
       apply cc_ind'; exact r.
       destruct r as [r | r]; [ left | right ].
        destruct r as [x_y r1 r2]; exists x_y.
         apply ic_ind'; exact r1.
         apply cc_ind'; exact r2.
        destruct r as [x_y r1 r2]; exists x_y.
         apply ii_ind'; exact r1.
         apply ic_ind'; exact r2.
  Qed.
End scheme.
Definition ppo := let ppoR := ii ⊓ [R] ⋅ top ⋅ [R] in let ppoW := ic ⊓ [R] ⋅ top ⋅ [W] in ppoR ⊔ ppoW.
Definition lwsync_0 := RM lwsync ⊔ WW lwsync.
Definition eieio_0 := WW eieio.
Definition dmb_st_0 := WW dmb_st.
Definition dsb_st_0 := WW dsb_st.
Definition strong := sync ⊔ (dmb ⊔ (dsb ⊔ (dmb_st_0 ⊔ dsb_st_0))).
Definition light := lwsync_0 ⊔ eieio_0.
Definition fence := strong ⊔ light.
Definition hb := ppo ⊔ (fence ⊔ rfe).
Definition thinair := acyclic hb.
Definition hbstar := hb^*.
Definition propbase := (fence ⊔ rfe ⋅ fence) ⋅ hbstar.
Definition chapo := rfe ⊔ (fre ⊔ (coe ⊔ (fre ⋅ rfe ⊔ coe ⋅ rfe))).
Definition prop := propbase ⊓ [W] ⋅ top ⋅ [W] ⊔ (chapo ⊔ 1) ⋅ (propbase^* ⋅ (strong ⋅ hbstar)).
Definition propagation := acyclic (co ⊔ prop).
Definition observation := irreflexive (fre ⋅ (prop ⋅ hbstar)).
Definition xx := po ⊓ [X] ⋅ top ⋅ [X].
Definition scXX := acyclic (co ⊔ xx).
Definition witness_conditions := True.
Definition model_conditions := uniproc /\ (thinair /\ (propagation /\ (observation /\ scXX))).
End Model.

Hint Unfold events R W IW FW B RMW F rf po int ext loc addr data ctrl amo rmw unknown_set unknown_relation M emptyset classes_loc X tag2events emptyset_0 partition tag2instrs po_loc rfe rfi co0 toid fencerel ctrlcfence imply nodetour singlestep LKW A P WW WR RW RR RM MR WM MW MM AA AP PA PP AM MA noid atom obsco cobase uniproc co fr coi fri coe fre dd rdw detour addrpo dmb_st dsb_st dmb dsb isb ctrlisb sync lwsync eieio isync ctrlisync ci0 ii0 cc0 ic0 ppo lwsync_0 eieio_0 dmb_st_0 dsb_st_0 strong light fence hb thinair hbstar propbase chapo prop propagation observation xx scXX witness_conditions model_conditions : cat.

Definition valid (c : candidate) := model_conditions c.

(* End of translation of model Model pretty print *)

author: jmadiot

repo: cats

save_path: github-repos/coq/jmadiot-cats