HyPre.util.VectorNat

From Coq Require Vector.
From Coq Require Import Orders.
Require Export VectorExtra.
Require Import VectorList.
Import VectorListNotations.

From Coq Require Import Lia.
From Coq Require Import Program.Equality.

Definition vn_zero k := Vector.const 0 k.

Definition vn_le {k : nat} (x y : Vector.t nat k)
  := Vector.Forall2 (fun x0 y0 => x0 <= y0) x y.

Definition vn_lt {k : nat} (x y : Vector.t nat k)
  := vn_le x y /\ x <> y.

Definition vn_add {k : nat} : Vector.t nat k -> Vector.t nat k -> Vector.t nat k
  := Vector.map2 Nat.add.

Definition vn_sub {k : nat} (v1 v2 : Vector.t nat k)
  := Vector.map2 Nat.sub v1 v2.

Definition vecnat_indexCons {k : nat} (xt : Vector.t nat k) (i : Fin.t k) (x : nat)
  : Vector.t nat k
  := Vector.replace xt i (x + Vector.nth xt i).

Module VecNatNotations.

  Infix "⪯" := vn_le (at level 71).
  Infix "≺" := vn_lt (at level 71).

  Infix "+vn+" := (Vector.map2 Nat.add) (at level 69).
  Infix "-vn-" := (Vector.map2 Nat.sub) (at level 69).
  Notation "x ':ivn:' xt 'at' i" := (vecnat_indexCons xt i x) (at level 69).
  Notation vecnat := (Vector.t nat).

End VecNatNotations.

Import VecNatNotations.

  (* TODO Prove vecnat lemmas *)
  Lemma vn_dec {k} (x y : Vector.t nat k)
    : {x = y} + {x <> y}.
  Proof.
    dependent induction x; dependent destruction y.
    - left. reflexivity.
    - destruct (NPeano.Nat.eq_dec h h0).
      + subst h0.
        specialize (IHx y).
        destruct IHx.
        * left.
          subst x. reflexivity.
        * right.
          contradict n0.
          dependent destruction n0.
          reflexivity.
      + right.
        contradict n0.
        dependent destruction n0.
        reflexivity.
  Qed.

  Global Instance vn_le_refl {k}
    : Reflexive (@vn_le k). (*x ⪯ x.*)
  Proof.
    unfold Reflexive.
    intros.
    eapply Vec_Forall2_forall2.
    intros.
    reflexivity.
  Qed.

  Global Instance vn_le_trans {k}
    : Transitive (@vn_le k).
  Proof.
    unfold Transitive.
    intros.
    eapply Vec_Forall2_forall2.
    intros.
    eapply Vec_Forall2_forall2 in H.
    eapply Vec_Forall2_forall2 in H0. Unshelve. 2,3:exact i.
    transitivity (y [[i]]);eauto.
  Qed.

  Lemma vn_lt_impl_vn_le {k} (x y : Vector.t nat k)
    : x ≺ y -> x ⪯ y.
  Proof.
    firstorder.
  Qed.

  Lemma vn_le_impl_vn_le_or_eq {k} (x y : Vector.t nat k)
    : x ⪯ y -> x ⪯ y \/ x = y.
  Proof.
    firstorder.
  Qed.

  Lemma vn_le_iff_vn_lt_or_eq {k} (x y : Vector.t nat k)
    : x ⪯ y <-> x ≺ y \/ x = y.
  Proof.
    split;intros;[destruct (vn_dec x y)|destruct H;[|subst] ];firstorder.
    reflexivity.
  Qed.

  Lemma vl_len_vl_app_vn_add {k} {X : Type} (v1 v2 : Vector.t (list X) k)
    : vl_len (v1 +vl+ v2) = vl_len v1 +vn+ vl_len v2.
  Proof.
    revert v2.
    dependent induction v1;
      intros;
      dependent destruction v2;
      cbn.
    - reflexivity.
    - f_equal.
      + rewrite app_length.
        reflexivity.
      + setoid_rewrite IHv1.
        reflexivity.
  Qed.

  Lemma vn_sub_add {k} (a b : vecnat k)
    : a ⪯ b -> (vn_sub b a) +vn+ a = b.
  Proof.
    intros.
    dependent induction b; dependent destruction a;cbn.
    - reflexivity.
    - unfold vn_le in H.
      dependent destruction H.
      replace (h0 - h + h) with h0 by lia.
      rewrite IHb;eauto.
  Qed.

  Lemma vn_zero_minimal {k} v
    : vn_zero k ⪯ v.
  Proof.
    dependent induction k;dependent destruction v;cbn.
    - unfold vn_le.
      eapply Vector.Forall2_nil.
    - eapply Vector.Forall2_cons.
      + lia.
      + setoid_rewrite IHk.
        reflexivity.
  Qed.

  Definition vn_index_plus {k} (x : vecnat k) (i : Fin.t k) (n : nat)
    := Vector.replace x i (Vector.nth x i + n).

  Lemma vn_eq_plus_minus {k} (i : Fin.t k)
    : forall a b, a ⪯ b -> b [[i]] = a [[i]] + (b [[i]] - a [[i]]).
  Proof.
    intros.
    dependent induction H.
    - lia.
    - dependent destruction i;cbn.
      + lia.
      + eapply IHForall2.
  Qed.

  Lemma forall_le_impl_vn_le {k}
    : forall a b, (forall (i : Fin.t k), a [[i]] <= b [[i]]) -> a ⪯ b.
  Proof.
    eapply Vec_Forall2_forall2.
  Qed.

  Lemma vn_le_impl_forall_le {k}
    : forall a b, a ⪯ b -> (forall (i : Fin.t k), a [[i]] <= b [[i]]).
  Proof.
    eapply Vec_Forall2_forall2.
  Qed.

  Inductive VecNatO {k} {X : Type} (fS : X -> nat -> nat) (Orcl : Vector.t nat k -> Vector.t X k)
    : Vector.t nat k -> Prop
    :=
    | VNOnil : VecNatO fS Orcl (Vector.const 0 k)
    | VNOcons : forall xt yt, VecNatO fS Orcl xt -> yt = Vector.map2 fS (Orcl xt) xt -> VecNatO fS Orcl yt.