Library Algebra.Monoid.ConcatnF

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for the concatenation of a family of families.

Description

Let G : AbelianMonoid. Let N : 'nat^n. Let A : i, 'G^(n i). Let i : 'I_n, j : 'I_(N i) and k : 'I_(sum N).

Used logic axioms

  • classic, the weak form of excluded middle.

Usage

This module may be used through the import of Algebra.Monoid.Monoid, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import stdlib.
From Coq Require Import List.

From Requisite Require Import ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid_sum.

Local Open Scope Monoid_scope.

Section ConcatnF_Def.

Context {G : Type}.

Lemma list_concat_length :
   (A : list (list G)),
    length (List.concat A) = sum (fun ilength (of_listF A i)).
Proof.
intros A; induction A.
simpl; now rewrite sum_nil.
rewrite sum_ind_l.
rewrite length_app.
unfold plus; simpl; f_equal.
rewrite IHA.
apply sum_ext; intros i.
unfold liftF_S.
rewrite -(of_listF_correct a); now simpl.
Qed.

Lemma list_concat_ind_r :
   A (l : list G), List.concat (A ++ (l :: nil)) = List.concat A ++ l.
Proof. intros; rewrite concat_app concat_cons concat_nil app_nil_r; easy. Qed.

Lemma list_concat_nth :
   x (A : list (list G)) i j k,
    (i = sum (fun zlength (of_listF (firstn j A) z)) + k)%coq_nat
    (j < length A)%coq_nat (k < length (nth j A nil))%coq_nat
    nth i (List.concat A) x = (nth k (nth j A nil) x).
Proof.
intros x A; induction A.
intros i j k H1 H2 H3.
contradict H2; simpl; auto with zarith.
intros i j k H1 H2 H3.
case_eq j.
intros Hj; simpl.
assert (Y: i = k).
rewrite H1 Hj; simpl.
rewrite sum_nil; auto.
rewrite app_nth1.
f_equal; easy.
rewrite Y; rewrite Hj in H3; simpl in H3; easy.
intros jj Hjj; simpl.
assert (Y: (i = length a + sum
  (fun z : 'I_(length (firstn jj A))
   length (of_listF (firstn jj A) z)) + k)%coq_nat).
rewrite H1; f_equal.
rewrite Hjj.
simpl (firstn jj.+1 (a :: A)).
simpl (length (a :: firstn jj A)).
rewrite sum_ind_l; unfold liftF_S; simpl.
unfold plus; simpl.
rewrite -plusE; f_equal.
apply sum_ext; intros z.
now rewrite of_listF_correct.

assert (length a i)%coq_nat.
rewrite Y; auto with zarith arith.
rewrite app_nth2; try easy.
apply IHA.
apply (proj1 (Nat.add_cancel_r _ _ (length a))).
apply trans_eq with i; auto with zarith arith.
rewrite Nat.add_comm.
rewrite Y; auto with zarith arith.
simpl in H2; auto with zarith.
rewrite Hjj in H3; simpl in H3; auto with zarith.
Qed.

Definition concatnF_aux {n} {b : 'nat^n} (g : i, 'G^(b i)) : list G :=
  List.concat (to_listF (fun ito_listF (g i))).

Lemma concatnF_aux_length :
   {n} {b : 'nat^n} (g : i, 'G^(b i)),
    length (concatnF_aux g) = sum b.
Proof.
intros n b g; unfold concatnF_aux.
rewrite list_concat_length; simpl.
rewrite of_to_listF'.
rewrite -(sum_castF (to_listF_length _)).
apply sum_ext; intros i.
unfold castF; simpl.
rewrite to_listF_length.
rewrite eq_sym_involutive; simpl.
rewrite cast_ordKV; easy.
Qed.

Definition concatnF {n} {b : 'nat^n} (g : i, 'G^(b i)) : 'G^(sum b) :=
  castF (concatnF_aux_length g) (of_listF (concatnF_aux g)).

End ConcatnF_Def.

Section ConcatnF_Facts.

Context {G : Type}.

Lemma fun_ext2_dep :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) n1 n2 m1 m2,
    nat_of_ord n1 = nat_of_ord n2
    nat_of_ord m1 = nat_of_ord m2
    g n1 m1 = g n2 m2.
Proof.
intros n b g n1 n2 m1 m2 H1 H2.
assert (T: n1 = n2).
apply ord_inj; easy.
subst.
f_equal; apply ord_inj; easy.
Qed.

Lemma concatnF_ind_l :
   {n} {b : 'nat^n.+1} (g : i, 'G^(b i)),
    concatnF g
      = castF (eq_sym (sum_ind_l b))
              (concatF (g ord0) (concatnF (fun i ⇒ (g (lift_S i) )))).
Proof.
intros n b g.
apply to_listF_inj; try apply 0.
rewrite <- to_listF_castF.
rewrite to_listF_concatF.
unfold concatnF.
rewrite <- 2!to_listF_castF.
rewrite 2!to_of_listF.
unfold concatnF_aux.
simpl; f_equal.
now rewrite castF_id.
rewrite castF_id; easy.
Qed.

Lemma concatnF_ind_r :
   {n} {b : 'nat^n.+1} (g : i, 'G^(b i)),
    concatnF g
      = castF (eq_sym (sum_ind_r b))
              (concatF (concatnF (fun ig (widen_S i))) (g ord_max)).
Proof.
intros n b g.
apply to_listF_inj; try apply 0.
rewrite <- to_listF_castF.
rewrite to_listF_concatF.
unfold concatnF.
rewrite <- 2!to_listF_castF.
rewrite 2!to_of_listF.
unfold concatnF_aux; f_equal.
rewrite -list_concat_ind_r; f_equal.
replace (fun i : 'I_n.+1to_listF (g i)) with
  (castF (Nat.add_1_r n)
  (concatF ((fun i : 'I_nto_listF (g (widen_S i))))
           (fun ito_listF (g ord_max)))).
rewrite -to_listF_castF; try apply 0.
rewrite to_listF_concatF; easy.
apply extF; intros i; unfold castF.
case (ord_eq_dec i ord_max); intros Hi.
rewrite Hi; rewrite concatF_correct_r; try easy.
simpl; auto with arith.
rewrite concatF_correct_l; try easy.
simpl; assert (i < n.+1)%coq_nat.
apply /ltP; easy.
assert (nat_of_ord i n)%coq_nat; auto with zarith.
intros V; apply Hi; apply ord_inj; simpl; auto.
intros K.
replace (widen_S (concat_l_ord K)) with i; try easy.
apply ord_inj; simpl; easy.
Qed.

Lemma concatnF_one :
   {b : 'nat^1} (g : i, 'G^(b i)),
    inhabited G concatnF g = castF (eq_sym (sum_1 b)) (g ord0).
Proof.
intros b g [x0]; apply extF; intros i.
unfold concatnF, castF.
rewrite -(of_listF_correct x0); simpl.
unfold concatnF_aux; simpl.
rewrite castF_id app_nil_r.
replace (nat_of_ord i) with (nat_of_ord (cast_ord (sum_1 b) i)) by easy.
rewrite -to_listF_correct.
f_equal; apply ord_inj; easy.
Qed.

Lemma concatnF_two :
   {b : 'nat^2} (g : i, 'G^(b i)),
    inhabited G
    concatnF g = castF (eq_sym (sum_2 b)) (concatF (g ord0) (g ord_max)).
Proof.
intros b g [x0]; apply extF; intros i.
unfold concatnF, castF.
rewrite -(of_listF_correct x0); simpl.
unfold concatnF_aux; simpl.
rewrite 2!castF_id app_nil_r; unfold liftF_S.
rewrite -to_listF_concatF.
rewrite (to_listF_correct x0 (concatF (g ord0) (g ord_max))).
f_equal; try easy.
replace (lift_S ord0) with (ord_max:'I_2); try easy.
apply ord_inj; simpl; easy.
Qed.

Definition concatn_ord_val {n} (b : 'nat^n) (i : 'I_n) (j : 'I_(b i)) :=
  (sum_part b (widen_S i) + j)%coq_nat.

Lemma concatn_ord_val_eq :
   {n} (b : 'nat^n) (i : 'I_n) (j : 'I_(b i)),
    concatn_ord_val b i j =
      (sum (of_listF (firstn i (to_listF b))) + j)%coq_nat.
Proof.
intros n b i j.
rewrite to_listF_firstn.
rewrite of_to_listF'.
rewrite sum_castF; easy.
Qed.

Lemma concatn_ord_proof :
   {n} (b : 'nat^n) (i : 'I_n) (j : 'I_(b i)),
    concatn_ord_val b i j < sum b.
Proof.
intros n b i j.
apply /ltP.
induction n.
destruct i; easy.
unfold concatn_ord_val.
case (Nat.eq_dec (nat_of_ord i) 0); intros Hi.
assert (Hi2 : i = ord0).
apply ord_inj; easy.
subst; simpl.
rewrite sum_part_nil; try easy.
apply Nat.lt_le_trans with (b ord0).
rewrite Nat.add_0_l.
apply /ltP; easy.
apply sum_ub_nat.
rewrite sum_part_ind_l_alt.
intros T; apply Hi; now rewrite T.
intros Hi2.
rewrite -Nat.add_assoc.
rewrite sum_ind_l.
apply Nat.add_lt_mono_l.
assert (V: b i = b (lift_S (lower_S Hi2))).
rewrite lift_lower_S; easy.
apply Nat.le_lt_trans with
  (2:= IHn (liftF_S b) (lower_S Hi2) (cast_ord V j)).
apply Nat.eq_le_incl; easy.
Qed.

Definition concatn_ord
    {n} (b : 'nat^n) (i : 'I_n) (j : 'I_(b i)) : 'I_(sum b) :=
  Ordinal (concatn_ord_proof b i j).

Lemma concatn_ord_lt_aux :
   {n} (b : 'nat^n) (i1 i2 : 'I_n) (j1 : 'I_(b i1)) (j2 : 'I_(b i2)),
    (i1 < i2)%coq_nat
    (concatn_ord b i1 j1 < concatn_ord b i2 j2)%coq_nat.
Proof.
intros n b i1 i2 j1 j2 H; simpl.
unfold concatn_ord_val.
apply Nat.lt_le_trans with (sum_part b (lift_S i1)).
rewrite sum_part_ind_r.
apply Nat.add_lt_mono_l.
apply /ltP; easy.
rewrite -(Nat.add_0_r (sum_part b (lift_S i1))).
apply Nat.add_le_mono.
2: auto with arith.
assert (V: i1.+1 i2).
apply /ltP; easy.
apply sum_le_nat_gen with V.
intros j; apply Nat.eq_le_incl.
unfold firstF, castF_nip, castF; simpl.
f_equal; apply ord_inj; now simpl.
Qed.

Lemma concatn_ord_lt :
   {n} (b : 'nat^n) (i1 i2 : 'I_n) (j1 : 'I_(b i1)) (j2 : 'I_(b i2)),
    ((i1 < i2)%coq_nat ( i1 = i2 (j1 < j2)%coq_nat))
     (concatn_ord b i1 j1 < concatn_ord b i2 j2)%coq_nat.
Proof.
intros n b i1 i2 j1 j2; split.
intros H; case H; intros H'.
now apply concatn_ord_lt_aux.
destruct H' as (H1,H2); subst.
simpl; unfold concatn_ord_val.
apply Nat.add_lt_mono_l; easy.
intros H.
case (Nat.le_gt_cases i1 i2); intros H1.
case (proj1 (Nat.lt_eq_cases i1 i2) H1); intros H2.
now left.
right; split.
apply ord_inj; easy.
apply ord_inj in H2.
generalize H; simpl ; unfold concatn_ord_val; simpl; subst.
apply Nat.add_lt_mono_l.
contradict H.
apply Nat.le_ngt.
apply Nat.lt_le_incl.
now apply concatn_ord_lt_aux.
Qed.

Lemma concatn_ord_correct :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) (i : 'I_n) (j : 'I_(b i)),
    concatnF g (concatn_ord b i j) = g i j.
Proof.
case (classic (( (elt:G), True))); intros HP.
destruct HP as (elt,_).
intros n b g i j; unfold concatnF.
unfold castF; simpl.
unfold concatnF_aux.
rewrite -(of_listF_correct elt); simpl.
rewritelist_concat_nth with (j:=i) (k:=j).
rewrite -to_listF_correct.
rewrite (to_listF_correct elt (g i)); easy.
unfold concatn_ord_val; f_equal.
assert (L1: (length (firstn i
       (to_listF (fun i0 : 'I_nto_listF (g i0)))) = i)).
apply firstn_length_le.
rewrite to_listF_length.
assert (i < n)%coq_nat; auto with zarith.
apply /ltP; easy.
rewrite -(sum_castF L1).
apply sum_ext.
intros z.
unfold castF; simpl.
unfold firstF, castF_nip, castF; simpl.
rewrite -(of_listF_correct nil); simpl.
rewrite to_listF_firstn.
unfold firstF; simpl.
unfold castF_nip, castF; simpl.
rewrite -to_listF_correct.
rewrite to_listF_length; easy.
rewrite to_listF_length.
now apply /ltP.
rewrite -to_listF_correct.
rewrite to_listF_length.
now apply /ltP.
intros [| n] b g i j; [now destruct i |].
case_eq (b i).
intros H1; exfalso; rewrite H1 in j; destruct j; easy.
intros l Hl; exfalso; rewrite Hl in j; apply HP.
(g i (cast_ord (eq_sym Hl) ord0)); easy.
Qed.

Lemma concatn_ord_correct' :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) k (i : 'I_n) (j : 'I_(b i)),
    nat_of_ord k = concatn_ord b i j concatnF g k = g i j.
Proof.
intros n b g k i j H.
apply ord_inj in H.
rewrite H; apply concatn_ord_correct.
Qed.

Definition succF {n} (b : 'nat^n) := mapF S b.

Lemma succF_correct : {n} (b : 'nat^n) i, succF b i = (b i).+1.
Proof. easy. Qed.

Lemma sum_is_S :
   {n} (b : 'nat^n.+1), sum (succF b) = ((sum (succF b)).-1).+1.
Proof.
intros n b.
assert (H: (0 < sum (succF b))%coq_nat).
apply Nat.lt_le_trans with ((b ord0).+1); auto with arith.
apply (sum_ub_nat (succF b) ord0).
generalize H; case (sum (succF b)); auto with arith.
Qed.

Lemma splitn_ord_aux0 :
   {n} {b : 'nat^n.+1} i,
    (sum_part (liftF_S b) (widen_S i) =
      sum_part b (widen_S (lift_S i)) - b ord0)%coq_nat.
Proof.
intros n b i.
rewrite sum_part_ind_l_alt.
apply lift_S_not_first.
intros K.
rewrite lower_lift_S.
unfold plus; simpl; rewrite Nat.add_comm.
rewrite PeanoNat.Nat.add_sub; easy.
Qed.

Lemma splitn_ord_aux1 :
   {n} {b : 'nat^n.+1} k,
    (b ord0 k)%coq_nat (k < sum b)%coq_nat
    (k - b ord0 < sum (liftF_S b))%coq_nat.
Proof.
intros n b k H1 H2.
apply Nat.add_lt_mono_l with (p:= b ord0).
replace ((b ord0 + (k - b ord0)))%coq_nat with k; auto with zarith arith.
replace (b ord0 + sum (liftF_S b))%coq_nat with (sum b); try easy.
rewrite sum_ind_l; easy.
Qed.

Lemma splitn_ord_aux2 :
   {n} {b : 'nat^n} (k : 'I_(sum b)),
    {i : 'I_n |
      (sum_part b (widen_S i) k)%coq_nat
      (k < sum_part b (lift_S i))%coq_nat}.
Proof.
induction n; intros b.
rewrite sum_nil; intros [k Hk]; easy.
intros k.
case (le_lt_dec (b ord0) k); intros Hk.
assert (Hkk : (k - b ord0)%coq_nat < sum (liftF_S b)).
apply /ltP.
apply splitn_ord_aux1; try easy.
now apply /ltP.
destruct (IHn (liftF_S b) (Ordinal Hkk)) as (i, (Hi1,Hi2)); simpl in Hi1, Hi2.
(lift_S i); split.
rewrite splitn_ord_aux0 in Hi1.
apply nat_sub_le_mono_r with (b ord0); try auto with arith.
unfold firstF, castF_nip, castF.
replace ord0 with (cast_ord (eq_sym (ord_split (widen_S (lift_S i))))
         (first_ord (n.+1 - widen_S (lift_S i)) ord0)).
apply: sum_ub_nat.
apply ord_inj; now simpl.
apply nat_sub_lt_mono_r with (b ord0); try auto with arith.
unfold firstF, castF_nip, castF.
replace ord0 with (cast_ord (eq_sym (ord_split (lift_S (lift_S i))))
         (first_ord (n.+1 - lift_S (lift_S i)) ord0)).
apply: sum_ub_nat.
apply ord_inj; now simpl.
apply Nat.lt_le_trans with (1:=Hi2).
rewrite 2!sum_part_ind_r.
rewrite splitn_ord_aux0.
unfold liftF_S; simpl.
rewrite PeanoNat.Nat.add_sub_swap.
apply Nat.eq_le_incl; easy.
unfold firstF, castF_nip, castF.
replace ord0 with (cast_ord (eq_sym (ord_split (widen_S (lift_S i))))
         (first_ord (n.+1 - widen_S (lift_S i)) ord0)).
apply: sum_ub_nat.
apply ord_inj; now simpl.
ord0.
rewrite sum_part_ind_r.
rewrite sum_part_nil; try easy.
split; auto with arith zarith.
Qed.

Lemma splitn_ord_aux3 :
   {n} {b : 'nat^n} (k : 'I_(sum (succF b))) (i j: 'I_n),
    (sum_part (succF b) (widen_S i) k)%coq_nat
      (k < sum_part (succF b) (lift_S i))%coq_nat
    (sum_part (succF b) (widen_S j) k)%coq_nat
      (k < sum_part (succF b) (lift_S j))%coq_nat
    (i < j)%coq_nat False.
Proof.
intros n b k i j (Hi1,Hi2) (Hj1,Hj2) H1.
assert (k < k)%coq_nat; auto with arith zarith.
apply Nat.lt_le_trans with (1:=Hi2).
apply Nat.le_trans with (2:=Hj1).
apply sum_part_nat_monot.
simpl; auto with arith.
Qed.

Lemma splitn_ord1_inj :
   {n} {b : 'nat^n} (k : 'I_(sum (succF b))) (i j: 'I_n),
    (sum_part (succF b) (widen_S i) k)%coq_nat
      (k < sum_part (succF b) (lift_S i))%coq_nat
    (sum_part (succF b) (widen_S j) k)%coq_nat
      (k < sum_part (succF b) (lift_S j))%coq_nat
    i = j.
Proof.
intros n b k i j Hi Hj.
case (Nat.le_gt_cases i j); intros H1.
case (proj1 (Nat.lt_eq_cases i j) H1); intros H2.
exfalso; apply (splitn_ord_aux3 k i j); easy.
apply ord_inj; easy.
exfalso; apply (splitn_ord_aux3 k j i); easy.
Qed.

Definition splitn_ord1 {n} {b : 'nat^n} (k : 'I_(sum b)) : 'I_n :=
  proj1_sig (splitn_ord_aux2 k).

Lemma splitn_ord1_correct :
   {n} {b : 'nat^n} (k : 'I_(sum b)),
    (sum_part b (widen_S (splitn_ord1 k)) k)%coq_nat
    (k < sum_part b (lift_S (splitn_ord1 k)))%coq_nat.
Proof.
intros n b k; unfold splitn_ord1.
destruct (splitn_ord_aux2 k); easy.
Qed.

Lemma splitn_ord2_proof :
   {n} {b : 'nat^n} (k : 'I_(sum b)),
    (k - sum_part b (widen_S (splitn_ord1 k)))%coq_nat < b (splitn_ord1 k).
Proof.
intros n b k.
destruct (splitn_ord1_correct k) as (Hi1,Hi2).
apply /ltP.
apply Nat.add_lt_mono_l with (p:=sum_part b (widen_S (splitn_ord1 k))).
apply Nat.le_lt_trans with k; auto with zarith arith.
apply Nat.lt_le_trans with (1:=Hi2).
rewrite sum_part_ind_r; easy.
Qed.

Definition splitn_ord2
    {n} {b : 'nat^n} (k : 'I_(sum b)) : 'I_(b (splitn_ord1 k)) :=
  Ordinal (splitn_ord2_proof k).

Lemma splitn_ord2_val :
   {n} {b : 'nat^n} (k : 'I_(sum b)),
    nat_of_ord (splitn_ord2 k) =
      (k - sum_part b (widen_S (splitn_ord1 k)))%coq_nat.
Proof.
intros; easy.
Qed.

Lemma splitn_ord :
   {n} {b : 'nat^n} k, k = concatn_ord b (splitn_ord1 k) (splitn_ord2 k).
Proof.
intros n b k; apply ord_inj; simpl.
destruct (splitn_ord1_correct k) as (Hi1,Hi2).
unfold concatn_ord_val; simpl; auto with zarith arith.
Qed.

Lemma concatnF_splitn_ord :
   {n : nat} {b : 'nat^n} (g : i : 'I_n, 'G^(b i)) k,
    concatnF g k = g (splitn_ord1 k) (splitn_ord2 k).
Proof.
intros n b g k.
rewrite {1}(splitn_ord k).
now rewrite concatn_ord_correct.
Qed.

Lemma concatn_splitn1_ord :
   {n} {b : 'nat^n} i j, i = splitn_ord1 (concatn_ord (succF b) i j).
Proof.
intros n b i j.
apply splitn_ord1_inj
   with (concatn_ord (succF b) i j).
2: split; apply splitn_ord1_correct.
unfold concatn_ord, concatn_ord_val; simpl.
split; auto with arith zarith.
rewrite sum_part_ind_r.
apply Nat.add_lt_mono_l.
unfold succF; apply /ltP; easy.
Qed.

Lemma concatn_splitn2_ord :
   {n} {b : 'nat^n} i j,
    nat_of_ord j = splitn_ord2 (concatn_ord (succF b) i j).
Proof.
intros n b i j.
rewrite splitn_ord2_val.
rewrite -concatn_splitn1_ord.
unfold concatn_ord, concatn_ord_val; simpl; auto with zarith.
Qed.

Lemma concatnF_invalF :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) i,
    invalF (g i) (concatnF g).
Proof.
intros n b g i j.
(concatn_ord b i j).
apply eq_sym, concatn_ord_correct.
Qed.

Lemma concatnF_inclF_equiv :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) (PG : G Prop),
    inclF (concatnF g) PG i, inclF (g i) PG.
Proof.
intros n b g PG; split; intros H.
intros i j.
rewrite <- concatn_ord_correct.
apply H.
intros i.
rewrite (splitn_ord i).
rewrite concatn_ord_correct.
apply H.
Qed.

Lemma concatnF_P :
   {n} {b : 'nat^n} (g : i, 'G^(b i)) (P : G Prop),
    ( i j, P (g i j)) k, P (concatnF g k).
Proof.
intros n b g P H k.
rewrite (splitn_ord k).
rewrite concatn_ord_correct; easy.
Qed.

Lemma splitn_ord1_0 :
   {n} {b : 'nat^n.+1} (k : 'I_(sum (succF b))),
    nat_of_ord k = 0 splitn_ord1 k = ord0.
Proof.
intros n b k Hk.
apply splitn_ord1_inj with k.
apply splitn_ord1_correct.
split.
rewrite sum_part_nil; try easy.
rewrite Hk; auto with arith.
rewrite Hk.
rewrite sum_part_ind_r sum_part_nil; try easy.
unfold plus, succF; simpl; rewrite mapF_correct; auto with arith.
Qed.

Lemma splitn_ord2_0 :
   {n} (b : 'nat^n.+1) (k : 'I_(sum (succF b))),
    nat_of_ord k = 0 splitn_ord2 k = ord0.
Proof.
intros n b k Hk.
apply ord_inj; rewrite splitn_ord2_val.
rewrite splitn_ord1_0; try easy.
rewrite sum_part_nil; auto with arith.
rewrite Hk; auto with arith.
Qed.

Lemma splitn_ord1_max :
   {n} (b : 'nat^n.+1) (k : 'I_(sum (succF b))),
    nat_of_ord k = (sum (succF b)).-1 splitn_ord1 k = ord_max.
Proof.
intros n b k Hk.
apply splitn_ord1_inj with k.
apply splitn_ord1_correct.
split.
apply Nat.le_trans with
  (((sum_part (succF b) (widen_S ord_max)
         + (b ord_max).+1))%coq_nat.-1)%coq_nat.
rewrite Nat.add_succ_r; auto with arith zarith.
apply Nat.le_trans with
 ((sum_part (succF b) (lift_S ord_max)).-1).
rewrite sum_part_ind_r; auto with arith.
rewrite Hk; apply Nat.pred_le_mono.
rewrite <- sum_part_ord_max.
apply Nat.eq_le_incl.
f_equal; apply ord_inj; simpl.
rewrite bump_r; auto with arith.
rewrite Hk -sum_part_ord_max.
apply Nat.lt_le_trans with
 (sum_part (succF b) ord_max).
assert (V: (0 < sum_part (succF b) ord_max)%coq_nat).
rewrite sum_part_ord_max.
apply Nat.lt_le_trans with ((b ord0).+1); auto with arith.
apply (sum_ub_nat (succF b) ord0).
generalize V; case (sum_part (succF b) ord_max); auto with arith zarith.
apply Nat.eq_le_incl.
f_equal; apply ord_inj; simpl.
rewrite bump_r; auto with arith.
Qed.

Lemma splitn_ord2_max :
   {n} (b : 'nat^n.+1) (k : 'I_(sum (succF b))),
    nat_of_ord k = (sum (succF b)).-1 splitn_ord2 k = ord_max.
Proof.
intros n b k Hk.
apply ord_inj; rewrite splitn_ord2_val.
rewrite splitn_ord1_max; try easy; simpl.
apply Nat.add_sub_eq_l.
apply trans_eq with
(((sum_part (succF b) (widen_S ord_max)) + (b ord_max).+1)%coq_nat.-1)%coq_nat.
auto with zarith arith.
rewrite Hk -sum_part_ord_max; f_equal.
generalize (sum_part_ind_r (succF b) ord_max); unfold plus; simpl.
intros V; rewrite -V; f_equal.
apply ord_inj; simpl; rewrite bump_r; auto with arith.
Qed.

Lemma splitn_ord1_S :
   {n} {b : 'nat^n.+1} (i j : 'I_(sum (succF b))),
    nat_of_ord j = i.+1
    (splitn_ord1 j = splitn_ord1 i
     nat_of_ord (splitn_ord2 j) = (splitn_ord2 i).+1)
    (nat_of_ord (splitn_ord1 j) = (splitn_ord1 i).+1
     splitn_ord2 i = ord_max splitn_ord2 j = ord0).
Proof.
intros n b i j H.
generalize (splitn_ord1_correct i); intros (K1,K2).
generalize (splitn_ord1_correct j); intros (K3,K4).
case (proj1 (Nat.lt_eq_cases i.+1
        (sum_part (succF b) (lift_S (splitn_ord1 i)))));
   auto with arith; intros H1.
left.
assert (splitn_ord1 j = splitn_ord1 i).
apply splitn_ord1_inj with j; split; try easy.
rewrite H; auto with arith.
rewrite H; auto with arith.
split; try easy.
rewrite 2!splitn_ord2_val H0 H.
auto with zarith arith.
right.
assert (nat_of_ord (splitn_ord1 j) = (splitn_ord1 i).+1)%coq_nat.
assert (H2 : (splitn_ord1 i).+1 < n.+1).
apply /ltP.
assert (H3: (splitn_ord1 i < n.+1)%coq_nat).
apply /ltP; easy.
case (proj1 (Nat.lt_eq_cases (splitn_ord1 i) n)); try auto with arith.
intros H4.
absurd (j < (sum (succF b)))%coq_nat.
2: apply /ltP; easy.
apply Nat.nlt_ge, Nat.eq_le_incl.
rewrite H H1.
rewrite -(sum_part_ord_max (succF b)); f_equal.
apply ord_inj; apply eq_trans with (n.+1); try easy.
apply eq_trans with ((splitn_ord1 i).+1); try easy.
now rewrite H4.
pose (u:= Ordinal H2).
apply trans_eq with (nat_of_ord u); try easy.
f_equal; apply splitn_ord1_inj with j; try easy; split.
rewrite H H1; apply Nat.eq_le_incl; f_equal.
apply ord_inj; easy.
rewrite H H1.
rewrite (sum_part_ind_r _ u).
unfold succF at 4; rewrite mapF_correct.
replace (lift_S (splitn_ord1 i)) with (widen_S u).
unfold plus; simpl; auto with zarith arith.
apply ord_inj; easy.
split; try easy; split.
apply ord_inj; rewrite splitn_ord2_val.
apply Nat.add_sub_eq_l; apply eq_add_S.
rewrite H1 sum_part_ind_r -Nat.add_succ_r; easy.
apply ord_inj; rewrite splitn_ord2_val.
rewrite H H1.
replace (widen_S (splitn_ord1 j))
   with (lift_S (splitn_ord1 i)); try auto with arith.
apply ord_inj; easy.
Qed.

Lemma concatnF_order :
   (Q : G G Prop)
      {n} (b : 'nat^n.+1) (g : i, 'I_(b i).+1 G),
    ( c d e, Q c d Q d e Q c e)
    ( i, sortedF Q (g i))
    ( (i : 'I_n.+1) (H : i ord_max ),
      Q (g i ord_max) (g (lift_S (narrow_S H)) ord0))
    sortedF Q (concatnF g).
Proof.
intros Q n b g Htrans H1 H2.
apply (sortedF_castF_equiv (sum_is_S b)), sortedF_equiv; [easy |].
intros i Hi; unfold castF.
pose (i' := cast_ord (eq_sym (sum_is_S b)) i).
pose (j' := cast_ord (eq_sym (sum_is_S b)) (Ordinal Hi)).
assert (Q (concatnF g i') (concatnF g j')); try easy.
destruct (splitn_ord1_S i' j') as [[K1 K2] | [K1 [K2 K3]]]; [easy |..].
rewrite (splitn_ord i') (splitn_ord j') !concatn_ord_correct.
assert (HQ : i1 i2 (j1 : 'I_(b i1).+1) (j2 : 'I_(b i2).+1),
    i1 = i2 (j1 < j2)%coq_nat Q (g i1 j1) (g i2 j2))
    by now intros; subst; apply H1.
apply HQ; [easy | rewrite K2; apply nat_ltS].
assert (K4 : splitn_ord1 i' ord_max)
    by now intros H; absurd (splitn_ord1 j' < n.+1)%coq_nat;
      [apply Nat.nlt_ge; rewrite K1 H | apply /ltP].
rewrite (splitn_ord i') (splitn_ord j') !concatn_ord_correct K2 K3.
replace (splitn_ord1 j') with (lift_S (narrow_S K4));
    [apply H2 | apply ord_inj; easy].
Qed.

End ConcatnF_Facts.

Section ConcatnF_Monoid_Facts.

Context {G : AbelianMonoid}.

Lemma concatnF_nil :
   {b : 'nat^0} (g : i, 'G^(b i)), concatnF g = 0.
Proof.
intros; apply extF; intros i.
exfalso; rewrite sum_nil in i; destruct i; easy.
Qed.

Lemma sum_assoc :
   {n} {b : 'nat^n} (g : i, 'G^(b i)),
    sum (concatnF g) = sum (fun isum (g i)).
Proof.
intros n; induction n; intros b g.
rewrite concatnF_nil !sum_nil; easy.
rewrite concatnF_ind_l sum_castF sum_concatF sum_ind_l IHn; easy.
Qed.

End ConcatnF_Monoid_Facts.