Require Export Coq.Classes.Morphisms. Require Export Coq.Setoids.Setoid. Require Export Coq.Classes.SetoidTactics. Require Export Coq.Relations.Relations. Require Export Coq.Bool.Sumbool. Require Export Coq.Bool.Bool. Require Export Ring. Require Export Field.
Require Export Coq.Logic.Classical.
Require Export Coq.Logic.FunctionalExtensionality.

Require Arith ZArith QArith Qcanon Reals List SetoidList.

Reserved Infix "=?" (at level 70). Reserved Infix "<?" (at level 70). Reserved Infix ">?" (at level 70). Reserved Infix "<=?" (at level 70). Reserved Infix ">=?" (at level 70).
Reserved Infix "??=" (at level 70). Reserved Infix "??<" (at level 70). Reserved Infix "??>" (at level 70). Reserved Infix "??<=" (at level 70). Reserved Infix "??>=" (at level 70).

Reserved Infix "+" (at level 50, left associativity). Reserved Infix "-" (at level 50, left associativity). Reserved Infix "*" (at level 40, left associativity). Reserved Infix "/" (at level 40, left associativity). Reserved Notation "a ²" (at level 1). Reserved Infix "c*" (at level 40, left associativity). Reserved Infix "*c" (at level 38, right associativity). Reserved Infix "*v" (at level 30, right associativity). Reserved Infix "v*" (at level 28, left associativity). Reserved Infix "⦿" (at level 40, left associativity). Reserved Infix "\o" (at level 50, no associativity).
Reserved Notation "< a , b >" (at level 60, a, b at level 55, format "< a , b >"). Reserved Notation "|| v ||" (at level 60, v at level 45, format "|| v ||"). Reserved Infix "\x" (at level 40, no associativity). Reserved Infix "∘" (at level 40, left associativity). Reserved Notation "- a" (at level 35, right associativity). Reserved Notation "/ a" (at level 35, right associativity). Reserved Notation "M \T" (at level 32, left associativity, format "M \T"). Reserved Notation "M \A" (at level 15, left associativity, format "M \A"). Reserved Notation "M \-1" (at level 20, format "M \-1"). Reserved Notation "M @ N" (at level 30, no associativity). Reserved Notation "'tr' M" (at level 33, no associativity).

Reserved Notation "'\sum' f" (at level 10). Reserved Notation "'\prod' f" (at level 10).
Reserved Infix "/_" (at level 60). Reserved Infix "/2_" (at level 60).
Reserved Infix "_|_" (at level 50). Reserved Infix "//" (at level 50). Reserved Infix "//+" (at level 50). Reserved Infix "//-" (at level 50).
Reserved Infix "+f" (at level 50, left associativity). Reserved Infix "-f" (at level 50, left associativity). Reserved Infix "*f" (at level 40, left associativity). Reserved Infix "/f" (at level 40, left associativity). Reserved Notation "-f g" (at level 35, right associativity). Reserved Notation "/f g" (at level 35, right associativity).

Reserved Notation "| r |" (at level 30, r at level 25, format "| r |").



Reserved Notation "v .[ i ]"
  (at level 2, i at next level, left associativity, format "v .[ i ]").
Reserved Notation "v .[ i <- a ]"
  (at level 2, i at next level, left associativity, format "v .[ i <- a ]").
Reserved Notation "M .[ i , j ]"
  (at level 2, i, j at next level, left associativity, format "M .[ i , j ]").
Reserved Notation "M .[ i , j <- a ]"
  (at level 2, i, j at next level, left associativity, format "M .[ i , j <- a ]").
Reserved Notation "M &[ i ]"
  (at level 2, i at next level, left associativity, format "M &[ i ]").


Reserved Notation "V .1" (at level 25, format "V .1"). Reserved Notation "V .2" (at level 25, format "V .2").
Reserved Notation "V .3" (at level 25, format "V .3").
Reserved Notation "V .4" (at level 25, format "V .4").


Reserved Notation "M .11" (at level 25, format "M .11"). Reserved Notation "M .12" (at level 25, format "M .12").
Reserved Notation "M .13" (at level 25, format "M .13").
Reserved Notation "M .14" (at level 25, format "M .14").
Reserved Notation "M .21" (at level 25, format "M .21").
Reserved Notation "M .22" (at level 25, format "M .22").
Reserved Notation "M .23" (at level 25, format "M .23").
Reserved Notation "M .24" (at level 25, format "M .24").
Reserved Notation "M .31" (at level 25, format "M .31").
Reserved Notation "M .32" (at level 25, format "M .32").
Reserved Notation "M .33" (at level 25, format "M .33").
Reserved Notation "M .34" (at level 25, format "M .34").
Reserved Notation "M .41" (at level 25, format "M .41").
Reserved Notation "M .42" (at level 25, format "M .42").
Reserved Notation "M .43" (at level 25, format "M .43").
Reserved Notation "M .44" (at level 25, format "M .44").

Reserved Notation "M &1" (at level 25, format "M &1"). Reserved Notation "M &2" (at level 25, format "M &2").
Reserved Notation "M &3" (at level 25, format "M &3").
Reserved Notation "M &4" (at level 25, format "M &4").


#[export] Set Bullet Behavior "Strict Subproofs".

Ltac copy H :=
  let HC := fresh "HC" in
  let HCeq := fresh "HCeq" in
  remember H as HC eqn: HCeq;
  clear HCeq.

#[global] Ltac list_eq :=
  repeat match goal with
    | |- cons ?h1 ?t1 = cons ?h2 ?t2 => f_equal
    | [H: cons _ _ = cons _ _ |- _] => inversion H; clear H
    end.

#[global] Ltac ssplit :=
  repeat
  match goal with
  | |- _ /\ _ => split
  end.

#[global] Ltac inv H :=
  inversion H; clear H; subst.

#[global] Ltac simp_proper :=
  unfold Proper; unfold respectful.

#[global] Ltac bdestruct X :=
  let H := fresh in
  let e := fresh "e" in
  evar (e: Prop);
  assert (H: reflect e X); subst e;
  [ try eauto with bdestruct
  | destruct H as [H|H]].

Ltac rw :=
  
  do 5
    (match goal with
     
     | [H : ?a = ?b |- ?a = ?c] => rewrite H
     
     | [H : ?a = ?b |- ?c = ?a] => rewrite H
     
     | [H : ?a = ?b |- ?c = ?b] => rewrite <- H
     
     | [H : ?a = ?b |- ?b = ?c] => rewrite <- H
     end;
     auto).

Ltac simp :=
  repeat
    (match goal with
     | [H : ?P |- ?P] => exact H
     | [|- True] => constructor
     | [H : False |- _] => destruct H
                             
     | [|- _ /\ _ ] => constructor
     | [|- _ -> _] => intro
     | [|- _ <-> _ ] => split; intros
     | [H : _ /\ _ |- _] => destruct H
     | [H : _ \/ _ |- _] => destruct H

     
                                           
     | [H : ?a = ?b |- _ ] => try progress (rewrite H)
     | [H : ?a <> ?b |- False] => destruct H
     end;
     auto).

Section example.
  Context {A : Type}.

  Goal forall a b c d e f g : A, a = b -> c = b -> d = c -> e = d -> a = e.
  Proof.
    simp. rw.
  Qed.
End example.

Definition is_true (b : bool) : Prop := b = true.
Coercion is_true : bool >-> Sortclass.


Lemma is_true_and_iff : forall b1 b2 : bool,
    is_true b1 /\ is_true b2 <-> is_true (b1 && b2).
Proof. destruct b1,b2; intros; split; intros; auto; try easy. Qed.

Lemma is_true_or_iff : forall b1 b2 : bool,
    is_true b1 \/ is_true b2 <-> is_true (b1 || b2).
Proof.
  destruct b1,b2; intros; split; intros; auto; try easy.
  simpl. unfold is_true in *. destruct H; auto.
Qed.

Example eqnP (n m : nat) : reflect (n = m) (Nat.eqb n m).
Proof.
  revert m. induction n; intros [|m]; simpl; try constructor; auto.
  destruct IHn with m; subst; constructor; auto.
Qed.

Definition option_get {A} (o : option A) (def : A) : A :=
  match o with
  | Some a => a
  | _ => def
  end.

Notation "x '.val'" := (proj1_sig x) (at level 1, format "x '.val'").
Notation "x '.prf'" := (proj2_sig x) (at level 1, format "x '.prf'").

Lemma sig_eq_iff : forall {A} {P : A -> Prop} a b (Ha : P a) (Hb : P b),
    (exist _ a Ha = exist _ b Hb) <-> a = b.
Proof.
  intros. split; intros.
  - inversion H. auto.
  - subst. f_equal. apply proof_irrelevance.
Qed.

Lemma sig_val : forall {A} {P : A -> Prop} a (Ha : P a), (exist _ a Ha).val = a.
Proof. intros. simpl. auto. Qed.

Lemma val_sig_eq : forall {A} {P : A -> Prop} (a : {x | P x}) (H : P (a.val)),
    exist _ (a.val) H = a.
Proof. intros. destruct a. simpl. apply sig_eq_iff; auto. Qed.

Declare Scope A_scope.
Delimit Scope A_scope with A.
Open Scope A.

Declare Scope vec_scope.
Delimit Scope vec_scope with V.
Open Scope vec_scope.

Declare Scope mat_scope.
Delimit Scope mat_scope with M.
Open Scope mat_scope.