Library Interval.Missing.MathComp

From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq bigop.
Require Export MathComp1or2.

Set Implicit Arguments.

Section NatCompl.

Lemma leq_subnK: ∀ m n : nat, n ≤ (n - m) + m.

Lemma leq_addLR m n p : n ≤ p → (m + n ≤ p) = (m ≤ p - n).

Lemma leq_addLRI m n p : (m + n ≤ p) → (m ≤ p - n).

Lemma ltn_leqN m n : m < n ≤ m = false.

Lemma max1n n : maxn 1 n = n.-1.+1.

Lemma ltn_leq_pred m n : m < n → m ≤ n.-1.

Lemma addn_pred_leqI a b k i :
  (a + b).-1 ≤ k → i ≤ k → a ≤ i ∨ b ≤ k - i.

End NatCompl.

Section bigops.
Lemma big_nat_leq_idx :
  ∀ (R : Type) (idx : R) (op : Monoid.law idx) (m n : nat) (F : nat → R),
  n ≤ m → (∀ i : nat, n ≤ i < m → F i = idx) →
  \big[op/idx]_(0 ≤ i < n) F i = \big[op/idx]_(0 ≤ i < m) F i.
End bigops.

Section Head_Last.
Variables (T : Type) (d : T).

Definition hb s := head d (behead s).

Lemma nth_behead s n : nth d (behead s) n = nth d s n.+1.

Lemma last_rev : ∀ s, last d (rev s) = head d s.
End Head_Last.

Lemma nth_map_dflt (C : Type) (x0 : C) (f : C → C) (n : nat) (s : seq C) :
  nth x0 (map f s) n = if size s ≤ n then x0 else f (nth x0 s n).

Section Map2.
Variable C : Type.
Variable x0 : C.
Variable op : C → C → C.
Variable op' : C → C. Fixpoint map2 (s1 : seq C) (s2 : seq C) : seq C :=
  match s1, s2 with
    | _, [::] ⇒ s1
    | [::], b :: s4 ⇒ op' b :: map2 [::] s4
    | a :: s3, b :: s4 ⇒ op a b :: map2 s3 s4
  end.

Lemma size_map2 s1 s2 : size (map2 s1 s2) = maxn (size s1) (size s2).

Lemma nth_map2_dflt (n : nat) (s1 s2 : seq C) :
  nth x0 (map2 s1 s2) n =
    match size s1 ≤ n, size s2 ≤ n with
    | true, true ⇒ x0
    | true, false ⇒ op' (nth x0 s2 n)
    | false, true ⇒ nth x0 s1 n
    | false, false ⇒ op (nth x0 s1 n) (nth x0 s2 n)
    end.

End Map2.

Lemma nth_mkseq_dflt (C : Type) (x0 : C) (f : nat → C) (n i : nat) :
  nth x0 (mkseq f n) i = if n ≤ i then x0 else f i.

Lemma nth_take_dflt (n0 : nat) (T : Type) (x0 : T) (i : nat) (s : seq T) :
  nth x0 (take n0 s) i = if n0 ≤ i then x0 else nth x0 s i.

Section map_proof.
Variables (V T : Type) (Rel : V → T → Prop).
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Variables (vop : V → V) (top : T → T).
Hypothesis H0 : Rel dv dt.
Hypothesis H0t : ∀ v : V, Rel v dt → Rel (vop v) dt.
Hypothesis H0v : ∀ t : T, Rel dv t → Rel dv (top t).
Hypothesis Hop : ∀ v t, Rel v t → Rel (vop v) (top t).
Lemma map_correct :
  ∀ sv st, RelP sv st → RelP (map vop sv) (map top st).
End map_proof.

Section map2_proof.
Variables (V T : Type) (Rel : V → T → Prop).
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Variables (vop : V → V → V) (vop' : V → V).
Variables (top : T → T → T) (top' : T → T).
Hypothesis H0 : Rel dv dt.

Hypothesis H0t : ∀ v : V, Rel v dt → Rel (vop' v) dt.
Hypothesis H0v : ∀ t : T, Rel dv t → Rel dv (top' t).
Hypothesis Hop' : ∀ v t, Rel v t → Rel (vop' v) (top' t).

Hypothesis H0eq : ∀ v, Rel v dt → v = dv.

Hypothesis H0t1 : ∀ (v1 v2 : V) (t1 : T), Rel v1 t1 →
                                               Rel v2 dt →
                                               Rel (vop v1 v2) t1.
Hypothesis H0t2 : ∀ (v1 v2 : V) (t2 : T), Rel v1 dt →
                                               Rel v2 t2 →
                                               Rel (vop v1 v2) (top' t2).
Hypothesis H0v1 : ∀ (v1 : V) (t1 t2 : T), Rel v1 t1 →
                                               Rel dv t2 →
                                               Rel v1 (top t1 t2).
Hypothesis H0v2 : ∀ (v2 : V) (t1 t2 : T), Rel dv t1 →
                                               Rel v2 t2 →
                                               Rel (vop' v2) (top t1 t2).
Hypothesis Hop : ∀ v1 v2 t1 t2, Rel v1 t1 → Rel v2 t2 → Rel (vop v1 v2) (top t1 t2).

Lemma map2_correct :
  ∀ sv1 sv2 st1 st2,
    RelP sv1 st1 →
    RelP sv2 st2 →
    RelP (map2 vop vop' sv1 sv2) (map2 top top' st1 st2).
End map2_proof.

Section fold_proof.
Variables (V T : Type).
Variable Rel : V → T → Prop.
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Hypothesis H0 : Rel dv dt.
Lemma foldr_correct fv ft sv st :
  RelP sv st →
  (∀ xv yv, Rel xv dt → Rel yv dt → Rel (fv xv yv) dt) →
  (∀ xt yt, Rel dv xt → Rel dv yt → Rel dv (ft xt yt)) →
  (∀ xv xt yv yt, Rel xv xt → Rel yv yt → Rel (fv xv yv) (ft xt yt)) →
  Rel (foldr fv dv sv) (foldr ft dt st).

Lemma seq_foldr_correct fv ft sv st (zv := [::]) (zt := [::]) :
  RelP sv st →
  (∀ xv yv, Rel xv dt → RelP yv zt → RelP (fv xv yv) zt) →
  (∀ xt yt, Rel dv xt → RelP zv yt → RelP zv (ft xt yt)) →
  (∀ xv xt yv yt, Rel xv xt → RelP yv yt → RelP (fv xv yv) (ft xt yt)) →
  RelP (foldr fv zv sv) (foldr ft zt st).

End fold_proof.

Section Foldri.
Variables (T R : Type) (f : T → nat → R → R) (z0 : R).

Fixpoint foldri (s : seq T) (i : nat) : R :=
  match s with
  | [::] ⇒ z0
  | x :: s' ⇒ f x i (foldri s' i.+1)
  end.
End Foldri.

Section foldri_proof.
Variables (V T : Type).
Variable Rel : V → T → Prop.
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Hypothesis H0 : Rel dv dt.
Lemma seq_foldri_correct fv ft sv st (zv := [::]) (zt := [::]) i :
  RelP sv st →
  
  (∀ xv yv i, Rel xv dt → RelP yv zt → RelP (fv xv i yv) zt) →
  (∀ xt yt i, Rel dv xt → RelP zv yt → RelP zv (ft xt i yt)) →
  (∀ xv xt yv yt i, Rel xv xt → RelP yv yt → RelP (fv xv i yv) (ft xt i yt)) →
  RelP (foldri fv zv sv i) (foldri ft zt st i).
End foldri_proof.

Section mkseq_proof.
Variables (V T : Type).
Variable Rel : V → T → Prop.
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Hypothesis H0 : Rel dv dt.
Lemma mkseq_correct fv ft (mv mt : nat) :
  (∀ k : nat, Rel (fv k) (ft k)) →
  
  (∀ k : nat, mv ≤ k < mt → fv k = dv) →
  (∀ k : nat, mt ≤ k < mv → fv k = dv) →
  RelP (mkseq fv mv) (mkseq ft mt).
End mkseq_proof.

Section misc_proofs.
Variables (V T : Type).
Variable Rel : V → T → Prop.
Variables (dv : V) (dt : T).
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).
Lemma set_nth_correct sv st bv bt n :
  RelP sv st →
  Rel bv bt →
  RelP (set_nth dv sv n bv) (set_nth dt st n bt).

Lemma drop_correct sv st n :
  RelP sv st →
  RelP (drop n sv) (drop n st).

Hypothesis H0 : Rel dv dt.
Lemma ncons_correct sv st n :
  RelP sv st →
  RelP (ncons n dv sv) (ncons n dt st).

End misc_proofs.