FinMatrix.CoqExt.Basic


Basic libraries


Require Export Coq.Setoids.Setoid. Require Export Coq.Classes.Morphisms. Require Export Coq.Classes.SetoidTactics. Require Export Coq.Relations.Relations. Require Export Coq.Bool.Sumbool. Require Export Coq.Bool.Bool. Require Export ExtrOcamlBasic ExtrOcamlNatInt MyExtrOCamlR.
Require Export LogicExt BoolExt StrExt.
Require Export List.

Reserved Notations




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 "s*" (at level 40, left associativity). Reserved Infix "*s" (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".

Eliminate Warning.



Customized tactics


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

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

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

inversion and subst
Ltac inv H := inversion H; clear H; subst.

first step of the proof of Proper
Ltac simp_proper :=
  unfold Proper; unfold respectful.

destruct by sumbool comparison procedure. Note that we should register the reflect reflection to "bdestruct" database first.


#[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]].

simplify the logic expressions
Ltac logic :=
  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 |- False] => destruct H
     end;
     try congruence).

Solve simple logic about "bool"
Ltac autoBool :=
  repeat
    let H := fresh "H" in
    match goal with
    
    | |- ?b = false <-> ?b <> true => split
    
    | |- ?b = false <-> ?b <> true => split
    
    | H: ?b = false |- ?b <> true => rewrite H
    
    | H: ?b <> true |- ?b = false => apply not_true_is_false
    
    | H: ?a && ?b = true |- _ => apply andb_prop in H
    end;
    logic.

Repeat executing an unary function

execute an unary function multiply times with the initial value. Similiar to fold. nexec a0 f n := f (f ... (f x) ...)
Fixpoint nexec {A:Type} (a0:A) (f:A->A) (n:nat) : A :=
  match n with
  | O => a0
  | S n' => nexec (f a0) f n'
  end.


nexec rewriting
Lemma nexec_rw : forall (A:Type) (a:A) (f:A->A) (n:nat),
  nexec (f a) f n = f (nexec a f n).
Proof.
  intros. revert a. induction n; intros; simpl; auto.
Qed.

Linear property of nexec
Lemma nexec_linear : forall (A:Type) (a:A) (f:A->A) (g:A->A) (n:nat)
  (H: forall x:A, f (g x) = g (f x)),
  nexec (g a) f n = g (nexec a f n).
Proof.
  intros. revert a. induction n; intros; simpl; auto. rewrite H,IHn. auto.
Qed.

map f (seq 0 (S n)) = map f (seq 0 n) + f n So, a0 + f 0 + f 1 + ... + f n = (a0 + f 0 + ... + f (n-1)) + f n
Lemma fold_map_seq : forall (A:Type) (f:nat->A) (g:A->A->A) (a0:A) (n:nat),
  fold_left g (map f (seq 0 (S n))) a0 = g (fold_left g (map f (seq 0 n)) a0) (f n).
Proof.
  intros.
  rewrite seq_S.   rewrite map_app.   rewrite fold_left_app.   simpl. auto.
Qed.

Extension for option type

Convert option type to base type
Definition option_get {tA} (o : option tA) (def : tA) : tA :=
  match o with
  | Some a => a
  | _ => def
  end.

Extension for sig type


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

{a | P a} = {b | P b} <-> a = b
Lemma sig_eq_iff : forall {tA} {P : tA -> 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.

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

{a.val | P (a.val)} = a
Lemma val_sig_eq : forall {tA} {P : tA -> 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.

Usually used scopes

Scope for element type of matrix/vector/list
Declare Scope A_scope.
Delimit Scope A_scope with A.
Open Scope A.

Scope for vector type
Declare Scope vec_scope.
Delimit Scope vec_scope with V.
Open Scope vec_scope.

Scope for matrix type
Declare Scope mat_scope.
Delimit Scope mat_scope with M.
Open Scope mat_scope.