Library FEM.multi_index
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.
This file is about the definitions of C and A.
CSdk d k is the vector of all vectors of size (d+1) and of sum k.
Adk d k is the vector of all vectors of size d and of sum <= k.
This file contains their definitions (with the correct size) and properties.
In particular, we order the vectiors so that they respect a specific order MOn
defined below (akin to grevlex order).
[RR9557v1]
François Clément and Vincent Martin,
Finite element method. Detailed proofs to be formalized in Coq,
RR-9557, first version, Inria Paris, 2024,
https://inria.hal.science/hal-04713897v1.
Description
Bibliography
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Algebra Require Import Algebra_wDep.
Section About_is_order.
Context {G : AbelianMonoid}.
Variable order : G → G → Prop.
Definition order_irrefl := ∀ x, ¬ order x x.
Definition order_trans := ∀ x y z, order x y → order y z → order x z.
Definition order_asym := ∀ x y, order x y → order y x → False.
Definition order_monomial := ∀ x y z,
order x y → order (plus x z) (plus y z).
Definition order_total := ∀ x y, order x y ∨ x = y ∨ order y x.
Lemma order_irrefl_asym :
order_trans → order_irrefl → order_asym.
Proof.
intros H1 H2 x y H3 H4.
apply (H2 x).
apply (H1 x y x); easy.
Qed.
Lemma asym_irrefl : order_trans → order_asym → order_irrefl.
Proof. intros H1 H2 x H3; apply (H2 x x); easy. Qed.
Lemma irrefl_asym_equiv : order_trans → order_irrefl ↔ order_asym.
Proof.
intro; split; [apply order_irrefl_asym | apply asym_irrefl]; easy.
Qed.
This order is strict, monomial, irreflexive, transitive and total
Be aware that this is a strong requirement; this applies
to (nat,lt) and many groups but not to (R^*, mul) or
( 0,1,..,n, + with saturation at n) for instance
Lemma is_smitt_irrefl :
is_smitt_order → order_irrefl.
Proof.
intros H; apply H.
Qed.
Lemma is_smitt_trans :
is_smitt_order → order_trans.
Proof.
intros H; apply H.
Qed.
Lemma is_smitt_monomial :
is_smitt_order → order_monomial.
Proof.
intros H; apply H.
Qed.
Lemma is_smitt_total :
is_smitt_order → order_total.
Proof.
intros H; apply H.
Qed.
Lemma is_smitt_asym :
is_smitt_order → order_asym.
Proof.
intros H; apply order_irrefl_asym; apply H.
Qed.
Lemma is_smitt_monomial_inv_r : is_smitt_order → ∀ x y z,
order (plus x z) (plus y z) → order x y.
Proof.
intros H x y z H1.
case (is_smitt_total H x y); intros V; try easy.
case V; intros W.
rewrite W in H1; exfalso; apply (is_smitt_irrefl H _ H1).
exfalso; apply (is_smitt_asym H (x+z)%M (y+z)%M); try easy.
apply (is_smitt_monomial H); easy.
Qed.
Lemma is_smitt_monomial_inv_l : is_smitt_order → ∀ x y z,
order (plus z x) (plus z y) → order x y.
Proof.
intros H x y z H1.
apply is_smitt_monomial_inv_r with z; try easy.
rewrite 2!(plus_comm _ z); easy.
Qed.
Lemma is_smitt_total_alt : is_smitt_order →
∀ (x y : G), ¬ order x y → ¬ order y x → x = y.
Proof.
intros H x y H1 H2.
case (is_smitt_total H x y); intros H4; try easy; case H4; easy.
Qed.
equivalent to Nat.add_cancel_l for nat ; requires G to have such an order
Lemma is_smitt_plus_cancel_r : is_smitt_order →
∀ (x y z: G), plus x z = plus y z → x = y.
Proof.
intros H x y z H1.
apply is_smitt_total_alt; try easy; intros T;
apply (is_smitt_irrefl H (x+z)%M).
rewrite {2}H1.
apply is_smitt_monomial; easy.
rewrite {1}H1.
apply is_smitt_monomial; easy.
Qed.
Lemma is_smitt_plus_cancel_l : is_smitt_order →
∀ (x y z: G), plus z x = plus z y → x = y.
Proof.
intros H x y z H1.
apply is_smitt_plus_cancel_r with z; try easy.
rewrite plus_comm H1 plus_comm; easy.
Qed.
End About_is_order.
Section is_order_props.
Lemma is_smitt_lt : is_smitt_order lt.
Proof.
split; try split; try split.
intros x; auto with arith.
intros x y z; auto with zarith.
intros x y z; unfold plus; simpl; auto with zarith.
intros x y; apply Nat.lt_total.
Qed.
Definition order_sym {T : Type} (order: T → T → Prop) := fun x y ⇒ order y x.
Lemma order_sym_sym : ∀ {T : Type} (order: T → T → Prop),
order_sym (order_sym order) = order.
Proof.
intros T order.
apply fun_ext; intros x; apply fun_ext; intros y; easy.
Qed.
Lemma is_smitt_sym : ∀ {G : AbelianMonoid} (Glt Ggt: G → G → Prop),
(∀ x y, Ggt x y = Glt y x) →
is_smitt_order Glt → is_smitt_order Ggt.
Proof.
intros G Glt Ggt H (Y1,(Y2,(Y3,Y4))); split; try split; try split.
intros x; rewrite H; apply Y1.
intros x y z; repeat rewrite H; intros H1 H2; apply (Y2 z y x); easy.
intros x y z; rewrite 2!H; apply Y3.
intros x y; case (Y4 x y); repeat rewrite H; intros H1;[right; now right|idtac].
case H1; intros H2; [right; now left|now left].
Qed.
End is_order_props.
Section Mon_def1.
∀ (x y z: G), plus x z = plus y z → x = y.
Proof.
intros H x y z H1.
apply is_smitt_total_alt; try easy; intros T;
apply (is_smitt_irrefl H (x+z)%M).
rewrite {2}H1.
apply is_smitt_monomial; easy.
rewrite {1}H1.
apply is_smitt_monomial; easy.
Qed.
Lemma is_smitt_plus_cancel_l : is_smitt_order →
∀ (x y z: G), plus z x = plus z y → x = y.
Proof.
intros H x y z H1.
apply is_smitt_plus_cancel_r with z; try easy.
rewrite plus_comm H1 plus_comm; easy.
Qed.
End About_is_order.
Section is_order_props.
Lemma is_smitt_lt : is_smitt_order lt.
Proof.
split; try split; try split.
intros x; auto with arith.
intros x y z; auto with zarith.
intros x y z; unfold plus; simpl; auto with zarith.
intros x y; apply Nat.lt_total.
Qed.
Definition order_sym {T : Type} (order: T → T → Prop) := fun x y ⇒ order y x.
Lemma order_sym_sym : ∀ {T : Type} (order: T → T → Prop),
order_sym (order_sym order) = order.
Proof.
intros T order.
apply fun_ext; intros x; apply fun_ext; intros y; easy.
Qed.
Lemma is_smitt_sym : ∀ {G : AbelianMonoid} (Glt Ggt: G → G → Prop),
(∀ x y, Ggt x y = Glt y x) →
is_smitt_order Glt → is_smitt_order Ggt.
Proof.
intros G Glt Ggt H (Y1,(Y2,(Y3,Y4))); split; try split; try split.
intros x; rewrite H; apply Y1.
intros x y z; repeat rewrite H; intros H1 H2; apply (Y2 z y x); easy.
intros x y z; rewrite 2!H; apply Y3.
intros x y; case (Y4 x y); repeat rewrite H; intros H1;[right; now right|idtac].
case H1; intros H2; [right; now left|now left].
Qed.
End is_order_props.
Section Mon_def1.
a first bunch of monomial strict orders
Context {G: AbelianMonoid}.
Variable order:G → G → Prop.
Fixpoint lex_alt {n} (x y:'G^n) : Prop :=
match n as p return (n = p → _) with
| 0 ⇒ fun H ⇒ reflexive order
| S m ⇒ fun H ⇒ (order (castF H x ord0) (castF H y ord0)) ∨
((castF H x) ord0 = (castF H y) ord0 ∧ lex_alt (skipF (castF H x) ord0) (skipF (castF H y) ord0))
end erefl.
Lemma truc : ∀ {n} (g:G), order_irrefl order
→ order_irrefl (@lex_alt n).
Proof.
induction n.
simpl.
intros g H1 x H2.
specialize (H2 g).
now apply (H1 g).
intros g H1 x Hx.
case Hx; repeat rewrite castF_refl.
apply H1.
intros (_,H2); generalize H2.
apply IHn; easy.
Qed.
Lemma truc2 : ∀ {n}, reflexive order
→ reflexive (@lex_alt n).
Proof.
induction n.
simpl; intros H1 x; easy.
intros H1 x.
right; repeat rewrite castF_refl.
split; try easy.
apply IHn; easy.
Qed.
Fixpoint lex {n} (x y:'G^n) : Prop :=
match n as p return (n = p → _) with
| 0 ⇒ fun H ⇒ False
| S m ⇒ fun H ⇒ (order (castF H x ord0) (castF H y ord0)) ∨
((castF H x) ord0 = (castF H y) ord0 ∧ lex (skipF (castF H x) ord0) (skipF (castF H y) ord0))
end erefl.
Fixpoint colex {n} (x y:'G^n) : Prop :=
match n as p return (n = p → _) with
| 0 ⇒ fun H ⇒ False
| S m ⇒ fun H ⇒ (order (castF H x ord_max) (castF H y ord_max)) ∨
((castF H x) ord_max = (castF H y) ord_max ∧ colex (skipF (castF H x) ord_max) (skipF (castF H y) ord_max))
end erefl.
Lemma lex_nil : ∀ (x y :'G^0), ¬ lex x y.
Proof.
intros x y; easy.
Qed.
Lemma lex_S : ∀ {n} (x y :'G^n.+1),
lex x y = (order (x ord0) (y ord0) ∨
(x ord0 = y ord0 ∧ lex (skipF x ord0) (skipF y ord0))).
Proof.
intros n x y; simpl; repeat rewrite castF_refl; easy.
Qed.
Lemma colex_nil : ∀ (x y :'G^0), ¬ colex x y.
Proof.
intros x y; easy.
Qed.
Lemma colex_S : ∀ {n} (x y :'G^n.+1),
colex x y = (order (x ord_max) (y ord_max) ∨
(x ord_max = y ord_max ∧ colex (skipF x ord_max) (skipF y ord_max))).
Proof.
intros n x y; simpl; repeat rewrite castF_refl; easy.
Qed.
Definition symlex {n} : ('G^n → 'G^n → Prop) := order_sym (@lex n).
Definition revlex {n} : ('G^n → 'G^n → Prop) := order_sym (@colex n).
Definition graded {n} (ordern:'G^n → 'G^n → Prop) (x y:'G^n) : Prop :=
(order (sum x) (sum y)) ∨ (sum x = sum y ∧ ordern x y).
Definition grlex {n} := graded (@lex n).
Definition grcolex {n} := graded (@colex n).
Definition grevlex {n} := graded (@revlex n).
Definition grsymlex {n} := graded (@symlex n).
Lemma sum_order_graded : ∀ {n} ordern (x y:'G^n),
order (sum x) (sum y) → graded ordern x y.
Proof.
intros ordern x y H; now left.
Qed.
Lemma graded_idem : ∀ {n:nat} (ordern:'G^n → 'G^n → Prop),
graded ordern = graded (graded ordern).
Proof.
intros n ordern.
apply fun_ext; intros x; apply fun_ext; intros y; apply prop_ext; split.
intros H; destruct H; try now left.
right; split; try easy.
right; easy.
intros H; destruct H; [now left| easy].
Qed.
Lemma is_smitt_lex : ∀ {n},
is_smitt_order order → is_smitt_order (@lex n).
Proof.
intros n H; repeat split; induction n; try easy.
intros x; rewrite lex_S; intros T; case T; try apply H.
intros (_,H1); generalize H1; apply IHn.
intros x y z; rewrite 3!lex_S; intros V1 V2; case V1; case V2.
intros H1 H2; left; apply (is_smitt_trans _ H _ (y ord0)); easy.
intros (H1,H2); rewrite H1; intros H3; now left.
intros H1 (H2,H3); rewrite -H2 in H1; now left.
intros (H1,H2) (H3,H4); right; split; [now rewrite -H1|idtac].
apply IHn with (skipF y ord0); easy.
intros x y z; rewrite 2!lex_S; intros H1; case H1.
intros H2; left; apply is_smitt_monomial; easy.
intros (H2,H3); right; split.
unfold plus; simpl; unfold fct_plus; simpl; now rewrite H2.
apply IHn; easy.
intros x y; rewrite (hat0F_unit x y); right; left; easy.
intros x y; rewrite 2!lex_S.
case (is_smitt_total _ H (x ord0) (y ord0)); intros H1.
left; left; easy.
case H1; clear H1; intros H1.
case (IHn (skipF x ord0) (skipF y ord0)); intros H2.
left; right; easy.
case H2; clear H2; intros H2.
right; left.
apply (eqxF_reg _ ord0); try easy.
apply eqxF_equiv; easy.
right; right; right; now split.
right; right; now left.
Qed.
Lemma is_smitt_colex : ∀ {n},
is_smitt_order order → is_smitt_order (@colex n).
Proof.
intros n H; repeat split; induction n; try easy.
intros x; rewrite colex_S; intros T; case T; try apply H.
intros (_,H1); generalize H1; apply IHn.
intros x y z; rewrite 3!colex_S; intros V1 V2; case V1; case V2.
intros H1 H2; left; apply (is_smitt_trans _ H _ (y ord_max)); easy.
intros (H1,H2); rewrite H1; intros H3; now left.
intros H1 (H2,H3); rewrite -H2 in H1; now left.
intros (H1,H2) (H3,H4); right; split; [now rewrite -H1|idtac].
apply IHn with (skipF y ord_max); easy.
intros x y z; rewrite 2!colex_S; intros H1; case H1.
intros H2; left; apply is_smitt_monomial; easy.
intros (H2,H3); right; split.
unfold plus; simpl; unfold fct_plus; simpl; now rewrite H2.
apply IHn; easy.
intros x y; rewrite (hat0F_unit x y); right; left; easy.
intros x y; rewrite 2!colex_S.
case (is_smitt_total _ H (x ord_max) (y ord_max)); intros H1.
left; left; easy.
case H1; clear H1; intros H1.
case (IHn (skipF x ord_max) (skipF y ord_max)); intros H2.
left; right; easy.
case H2; clear H2; intros H2.
right; left.
apply (eqxF_reg _ ord_max); try easy.
apply eqxF_equiv; easy.
right; right; right; now split.
right; right; now left.
Qed.
Lemma is_smitt_symlex : ∀ {n},
is_smitt_order order → is_smitt_order (@symlex n).
Proof.
intros n H; apply is_smitt_sym with (@lex n); try easy.
apply is_smitt_lex; easy.
Qed.
Lemma is_smitt_revlex : ∀ {n},
is_smitt_order order → is_smitt_order (@revlex n).
Proof.
intros n H; apply is_smitt_sym with (@colex n); try easy.
apply is_smitt_colex; easy.
Qed.
Lemma is_smitt_graded : ∀ {n} (ordern: 'G^n → 'G^n → Prop),
is_smitt_order order → is_smitt_order ordern
→ is_smitt_order (graded ordern).
Proof.
intros n ordern (Y1,(Y2,(Y3,Y4))) (Z1,(Z2,(Z3,Z4))); unfold graded; repeat split.
intros x T; case T.
apply Y1.
intros (_,H); generalize H; apply Z1.
intros x y z H1 H2.
case H1; [intros U1|intros (U1,U2)].
case H2; [intros U3|intros (U3,U4)].
left; apply (Y2 _ (sum y)); easy.
left; rewrite -U3; easy.
case H2; [intros U3|intros (U3,U4)].
left; rewrite U1; easy.
right; split.
rewrite U1; easy.
apply (Z2 _ y); easy.
intros x y z; intros H1.
case H1; [intros U1|intros (U1,U2)].
left; rewrite 2!sum_plus.
apply Y3; easy.
right; split.
rewrite 2!sum_plus; rewrite U1; easy.
apply Z3; easy.
intros x y.
case (Y4 (sum x) (sum y)); intros U1.
left; now left.
case U1; clear U1; intros U1.
case (Z4 x y); intros U2.
left; right; now split.
case U2; clear U2; intros U2.
right; now left.
right; right; right; now split.
right; right; now left.
Qed.
Lemma is_smitt_grsymlex : ∀ {n},
is_smitt_order order → is_smitt_order (@grsymlex n).
Proof.
intros n H.
apply is_smitt_graded; try easy.
apply is_smitt_symlex; easy.
Qed.
Lemma is_smitt_grlex : ∀ {n},
is_smitt_order order → is_smitt_order (@grlex n).
Proof.
intros n H.
apply is_smitt_graded; try easy.
apply is_smitt_lex; easy.
Qed.
Lemma is_smitt_grcolex : ∀ {n},
is_smitt_order order → is_smitt_order (@grcolex n).
Proof.
intros n H.
apply is_smitt_graded; try easy.
apply is_smitt_colex; easy.
Qed.
Lemma is_smitt_grevlex : ∀ {n},
is_smitt_order order → is_smitt_order (@grevlex n).
Proof.
intros n H.
apply is_smitt_graded; try easy.
apply is_smitt_revlex; easy.
Qed.
End Mon_def1.
Section Mon_prop1.
Context {G: AbelianMonoid}.
Variable order: G → G → Prop.
Hypothesis Ho : is_smitt_order order.
Lemma graded_nil : ∀ (ordern:'G^0 → 'G^0 → Prop) (x y :'G^0),
is_smitt_order ordern → ¬ graded order ordern x y.
Proof.
intros ordern x y H0.
rewrite (hat0F_unit x y).
apply is_smitt_graded; easy.
Qed.
Lemma grevlex_S : ∀ {n} (x y :'G^n.+1),
grevlex order x y ↔ (order (sum x) (sum y) ∨
(sum x = sum y ∧ grevlex order (skipF x ord_max) (skipF y ord_max))).
Proof.
intros n x y; split; intros H1.
case H1;[intros H2|intros (H2,H3)].
now left.
right; split; try easy.
case H3; repeat rewrite castF_refl;[intros H4|intros (H4,H5)].
left.
apply (is_smitt_monomial_inv_l _ Ho _ _ (y ord_max)).
rewrite -(sum_skipF y ord_max) -H2.
rewrite (sum_skipF _ ord_max).
apply is_smitt_monomial; easy.
right; split; try easy.
apply (is_smitt_plus_cancel_l _ Ho) with (x ord_max).
rewrite -(sum_skipF x ord_max) H2 -H4.
rewrite (sum_skipF _ ord_max); easy.
case H1;[intros H2|intros (H2,H3)].
now left.
right; split; try easy.
case H3; repeat rewrite castF_refl;[intros H4|intros (H4,H5)].
left; rewrite 2!castF_refl.
apply (is_smitt_monomial_inv_r _ Ho _ _ (sum (skipF y ord_max))).
rewrite -(sum_skipF y ord_max) -H2.
rewrite (sum_skipF _ ord_max).
rewrite 2!(plus_comm (x ord_max)).
apply is_smitt_monomial; easy.
right; split; repeat rewrite castF_refl; try easy.
apply (is_smitt_plus_cancel_r _ Ho _ _ (sum (skipF x ord_max))).
rewrite -(sum_skipF x ord_max) H2 H4.
rewrite (sum_skipF _ ord_max); easy.
Qed.
Lemma grsymlex_S : ∀ {n} (x y :'G^n.+1),
grsymlex order x y ↔ (order (sum x) (sum y) ∨
(sum x = sum y ∧ grsymlex order (skipF x ord0) (skipF y ord0))).
Proof.
intros n x y; split; intros H1.
case H1;[intros H2|intros (H2,H3)].
now left.
right; split; try easy.
case H3; repeat rewrite castF_refl;[intros H4|intros (H4,H5)].
left.
apply (is_smitt_monomial_inv_l _ Ho _ _ (y ord0)).
rewrite -(sum_skipF y ord0) -H2.
rewrite (sum_skipF _ ord0).
apply is_smitt_monomial; easy.
right; split; try easy.
apply (is_smitt_plus_cancel_l _ Ho) with (x ord0).
rewrite -(sum_skipF x ord0) H2 -H4.
rewrite (sum_skipF _ ord0); easy.
case H1;[intros H2|intros (H2,H3)].
now left.
right; split; try easy.
case H3; repeat rewrite castF_refl;[intros H4|intros (H4,H5)].
left; rewrite 2!castF_refl.
apply (is_smitt_monomial_inv_r _ Ho _ _ (sum (skipF y ord0))).
rewrite -(sum_skipF y ord0) -H2.
rewrite (sum_skipF _ ord0).
rewrite 2!(plus_comm (x ord0)).
apply is_smitt_monomial; easy.
right; split; repeat rewrite castF_refl; try easy.
apply (is_smitt_plus_cancel_r _ Ho _ _ (sum (skipF x ord0))).
rewrite -(sum_skipF x ord0) H2 H4.
rewrite (sum_skipF _ ord0); easy.
Qed.
Lemma graded_lt_nonneg : ∀ {n} (ordern:'nat^n → 'nat^n → Prop) (x:'nat^n),
x = zero ∨ graded lt ordern zero x.
Proof.
intros n ordern x.
case (Nat.eq_0_gt_0_cases (sum x)); intros H0.
left; clear ordern; induction n.
apply extF; intros (i,Hi); easy.
rewrite sum_ind_l in H0.
destruct (nat_plus_def _ _ H0) as (H1,H2).
specialize (IHn _ H2).
apply extF.
apply PAF_ind_l; try easy.
intros j; generalize (fun_ext_rev IHn j).
unfold liftF_S; easy.
right; apply sum_order_graded.
rewrite sum_zero; easy.
Qed.
End Mon_prop1.
Section Mon_sym.
Context {G: AbelianMonoid}.
Lemma lex_sym : ∀ (order:G → G → Prop) {n},
@lex _ (order_sym order) n = symlex order.
Proof.
intros order n; induction n; try easy.
apply fun_ext; intros x; apply fun_ext; intros y; apply prop_ext.
split; intros H; destruct H as [H|H]; try (left;easy); right; split; try easy.
rewrite -IHn; easy.
rewrite IHn; easy.
Qed.
Lemma colex_sym : ∀ (order:G → G → Prop) {n:nat},
@colex _ (order_sym order) n = revlex order.
Proof.
intros order n; induction n; try easy.
apply fun_ext; intros x; apply fun_ext; intros y; apply prop_ext.
split; intros H; destruct H as [H|H]; try (left;easy); right; split; try easy.
rewrite -IHn; easy.
rewrite IHn; easy.
Qed.
Lemma symlex_sym : ∀ (order:G → G → Prop) {n:nat},
@symlex _ (order_sym order) n = lex order.
Proof.
intros order n.
rewrite -{2}(order_sym_sym order).
now rewrite lex_sym.
Qed.
Lemma revlex_sym : ∀ (order:G → G → Prop) {n:nat},
@revlex _ (order_sym order) n = colex order.
Proof.
intros order n.
rewrite -{2}(order_sym_sym order).
now rewrite colex_sym.
Qed.
Lemma graded_sym : ∀ (order:G → G → Prop) {n:nat} (ordern:'G^n → 'G^n → Prop),
graded (order_sym order) (order_sym ordern) = order_sym (graded order ordern).
Proof.
intros order n ordern.
apply fun_ext; intros x; apply fun_ext; intros y.
unfold graded, order_sym; apply prop_ext; split; intros H.
case H; [intros H1; now left|intros (H1,H2); right; now split].
case H; [intros H1; now left|intros (H1,H2); right; now split].
Qed.
End Mon_sym.
Section lexico_MO.
Definition grsymlex_lt {n} := @grsymlex _ lt n.
Lemma grsymlex_lt_nil : ∀ (x y : 'nat^0),
¬ grsymlex_lt x y.
Proof.
intros x y; apply graded_nil; try apply is_smitt_symlex; apply is_smitt_lt.
Qed.
Lemma grsymlex_lt_S : ∀ {n : nat} (x y : 'nat^n.+1),
grsymlex_lt x y ↔
(sum x < sum y)%coq_nat ∨
sum x = sum y ∧ grsymlex_lt (skipF x ord0) (skipF y ord0).
Proof.
intros n x y.
apply grsymlex_S, is_smitt_lt.
Qed.
Lemma is_smitt_grsymlex_lt : ∀ {n}, is_smitt_order (@grsymlex_lt n).
Proof.
intros n; apply is_smitt_graded.
apply is_smitt_lt.
apply is_smitt_symlex, is_smitt_lt.
Qed.
Lemma grsymlex_lt_trans : ∀ {n} (x y z:'nat^n),
grsymlex_lt x y → grsymlex_lt y z → grsymlex_lt x z.
Proof.
intros n; apply is_smitt_grsymlex_lt.
Qed.
Lemma grsymlex_lt_irrefl : ∀ {n} (x:'nat^n), ¬ grsymlex_lt x x.
Proof.
intros n; apply is_smitt_grsymlex_lt.
Qed.
Lemma grsymlex_lt_total_strict : ∀ {n} (x y:'nat^n),
x ≠ y → grsymlex_lt x y ∨ grsymlex_lt y x.
Proof.
intros n x y H.
case (is_smitt_total _ is_smitt_grsymlex_lt x y) as [H1|H1];
[now left| destruct H1; try easy; now right].
Qed.
Fixpoint grsymlex_alt {n} (x y : 'nat^n) : Prop :=
match n as p return (n = p → _) with
| 0 ⇒ fun H ⇒ False
| S m ⇒ fun (H:n=m.+1) ⇒ (sum x < sum y)%coq_nat ∨
(sum x = sum y ∧ grsymlex_alt (skipF (castF H x) ord0) (skipF (castF H y) ord0))
end erefl.
Lemma grsymlex_alt_correct : ∀ {n}, @grsymlex_alt n = grsymlex_lt.
Proof.
induction n.
apply fun_ext; intros x; apply fun_ext; intros y; apply prop_ext; simpl.
split; try easy.
apply grsymlex_lt_nil.
apply fun_ext; intros x; apply fun_ext; intros y.
apply prop_ext; simpl; apply iff_sym.
apply iff_trans with (1:=grsymlex_lt_S x y).
repeat rewrite castF_refl; rewrite IHn; easy.
Qed.
Lemma grsymlex_lt_correct1 : ∀ x y : 'nat^1, grsymlex_lt x y = (x ord0 < y ord0)%coq_nat.
Proof.
intros x y; unfold grsymlex_lt, grsymlex, graded.
rewrite 2!sum_1; simpl; rewrite castF_id; apply prop_ext.
split; intros H; try now left.
case H; try easy.
intros (H1,H2); case H2; try easy; intros H3; auto with zarith.
Qed.
Lemma grsymlex_lt_itemF_monotS : ∀ n (i j:'I_n), (nat_of_ord j = i.+1)%coq_nat →
grsymlex_lt (itemF n 1 i) (itemF n 1 j).
Proof.
intros [| n]; [intros [i Hi]; easy |].
induction n.
intros i j H; contradict H.
rewrite 2!I_1_is_unit; easy.
intros i j H; rewrite grsymlex_lt_S.
right; split.
rewrite 2!sum_itemF; easy.
case (ord_eq_dec i ord0); intros Hi.
rewrite Hi; rewrite skipF_itemF_diag.
left.
rewrite sum_zero.
rewrite skipF_itemF_0.
apply ord_neq; rewrite H; easy.
intros Hj; rewrite sum_itemF.
now auto with arith.
rewrite skipF_itemF_0.
rewrite skipF_itemF_0.
apply ord_neq; rewrite H; easy.
intros Hj; apply IHn.
rewrite 2!lower_S_correct H.
assert (nat_of_ord i ≠ 0); auto with zarith.
contradict Hi; apply ord_inj; easy.
Qed.
Lemma grsymlex_lt_itemF_monot : ∀ n (i j:'I_n), (i < j)%coq_nat →
grsymlex_lt (itemF n 1 i) (itemF n 1 j).
Proof.
intros n i j H.
pose (t:= (j-i)%coq_nat).
assert (Ht: (nat_of_ord j = i + t)%coq_nat) by auto with zarith.
generalize t i j Ht H; clear i j t Ht H.
induction t.
intros i j H1 H2; contradict H2; auto with zarith.
intros i j Ht H.
case_eq t.
intros Ht0.
apply grsymlex_lt_itemF_monotS.
rewrite Ht Ht0; auto with zarith.
intros tt Htt.
assert (Hk: ((i + t)%coq_nat < n)).
apply ltn_trans with j.
apply /ltP; rewrite Ht; auto with zarith.
destruct j; easy.
apply is_smitt_trans with (itemF n 1 (Ordinal Hk)).
apply is_smitt_grsymlex_lt.
apply IHt; try easy.
simpl; auto with zarith.
apply grsymlex_lt_itemF_monotS.
simpl; rewrite Ht; auto with zarith.
Qed.
Goal let x := (itemF 3 1 ord1) in
let y := (itemF 3 1 ord_max) in
grsymlex_lt x y ∧ ¬ grevlex lt x y.
Proof.
intros x y; split.
apply grsymlex_lt_itemF_monot.
simpl; rewrite bump_r; auto with arith.
intros T; case T.
unfold x, y; rewrite 2!sum_itemF; auto with zarith.
intros (_,T1); generalize T1; clear T T1.
unfold revlex, order_sym; rewrite colex_S.
unfold x, y; rewrite itemF_diag itemF_correct_r.
2: apply ord_neq; simpl; rewrite bump_r; auto with arith.
intros T; case T; [intros H|intros (H,_)];
contradict H; auto with zarith arith.
Qed.
End lexico_MO.
Section Weighted_orders.
Context {K:Ring}.
Variable (R: K → K → Prop).
Fixpoint weight_order {n m : nat} (weight : 'I_m → 'K^n) (x y :'K^n) :=
match m as p return (m = p → _) with
| 0 ⇒ fun H ⇒ False
| S mm ⇒ fun H ⇒
R (dot_product x (castF H weight ord0)) (dot_product y (castF H weight ord0))
∨
((dot_product x (castF H weight ord0) = dot_product y (castF H weight ord0)) ∧
weight_order (liftF_S (castF H weight)) x y)
end erefl.
Lemma weight_order_S : ∀ {n m} (weight:'I_m.+1 → 'K^n) (x y:'K^n),
weight_order weight x y =
(R (dot_product x (weight ord0)) (dot_product y (weight ord0))
∨
((dot_product x (weight ord0) = dot_product y (weight ord0)) ∧
weight_order (liftF_S weight) x y)).
Proof.
intros; simpl; rewrite !castF_refl; easy.
Qed.
Lemma weight_order_equiv : ∀ {m n1 n2} (w1: 'I_m → 'K^n1) (w2:'I_m → 'K^n2) x1 y1 x2 y2,
(∀ i, dot_product x1 (w1 i) = dot_product x2 (w2 i)) →
(∀ i, dot_product y1 (w1 i) = dot_product y2 (w2 i)) →
weight_order w1 x1 y1 = weight_order w2 x2 y2.
Proof.
intros m; induction m.
intros; easy.
intros n1 n2 w1 w2 x1 y1 x2 y2 H1 H2.
rewrite 2!weight_order_S.
apply prop_ext; split; apply modus_ponens_or.
rewrite H1 H2; easy.
intros (H3,H4); split.
rewrite -H1 -H2; easy.
rewrite (IHm _ _ (liftF_S w2) (liftF_S w1) x2 y2 x1 y1); try easy.
intros i; now rewrite H1.
intros i; now rewrite H2.
rewrite -H1 -H2; easy.
intros (H3,H4); split.
rewrite H1 H2; easy.
rewrite (IHm _ _ (liftF_S w1) (liftF_S w2) x1 y1 x2 y2); try easy.
intros i; now rewrite H1.
intros i; now rewrite H2.
Qed.
Lemma lex_weight_aux : ∀ {n} (x:'K^n) i,
dot_product x (itemF n 1%K i) = x i.
Proof.
intros n x i.
unfold dot_product; rewrite lc_itemF_r scal_one_r; easy.
Qed.
Lemma lex_weight_aux2 : ∀ {n} (x y:'K^n.+1),
weight_order (liftF_S (itemF n.+1 1%K)) x y =
weight_order (itemF n 1%K) (skipF x ord0) (skipF y ord0).
Proof.
intros n x y; rewrite -skipF_first.
apply weight_order_equiv; intros i.
rewrite 2!lex_weight_aux; easy.
rewrite 2!lex_weight_aux; easy.
Qed.
Lemma lex_weight : ∀ n,
weight_order (itemF n (@one K)) = lex R.
Proof.
induction n.
simpl; easy.
apply fun_ext; intros x; apply fun_ext; intros y; apply prop_ext.
rewrite weight_order_S.
repeat rewrite lex_weight_aux.
rewrite lex_S.
split; apply modus_ponens_or; try easy; intros (H1,H2); split; try easy.
rewrite -IHn.
rewrite -lex_weight_aux2; easy.
rewrite lex_weight_aux2 IHn; easy.
Qed.
End Weighted_orders.
Section MI_Def.
Definition Slice_op {d:nat} (i:nat)
:= fun alpha : 'nat^d ⇒
castF (add1n d) (concatF (singleF i) alpha).
Lemma Slice_op_sum: ∀ d k i (alpha:'nat^d),
(i ≤ k)%coq_nat → (sum alpha = k-i)%coq_nat → sum (Slice_op i alpha) = k.
Proof.
intros dd k i alpha H0 H1; unfold Slice_op.
rewrite sum_castF sum_concatF.
rewrite sum_singleF H1.
auto with arith.
Qed.
Lemma Slice_op_correct : ∀ {d:nat} k (alpha: 'nat^(d.+1)),
sum alpha = k →
{ ibeta : nat × 'nat^d | let i := fst ibeta in let beta := snd ibeta in
(i ≤ k)%coq_nat ∧ (sum beta = k-i)%coq_nat ∧ Slice_op i beta = alpha }.
Proof.
intros d k alpha H.
∃ (alpha ord0, liftF_S alpha); split; try split; simpl.
apply sum_ub_alt_nat; try easy.
now apply Nat.eq_le_incl.
apply nat_add_sub_r.
rewrite <- H.
rewrite -skipF_first.
apply (sum_skipF alpha ord0).
unfold Slice_op; apply extF; intros i; unfold castF; simpl.
case (Nat.eq_0_gt_0_cases i); intros Hi.
rewrite concatF_correct_l.
simpl; rewrite Hi; auto with arith.
intros V; simpl; rewrite singleF_0; f_equal.
apply ord_inj; now simpl.
rewrite concatF_correct_r.
simpl; auto with arith.
intros V; unfold liftF_S; simpl; f_equal.
apply ord_inj; simpl; unfold bump; simpl; auto with arith.
Qed.
Definition Slice_fun {d n:nat} (u:nat) (a:'I_n → 'nat^d) : 'I_n → 'nat^(d.+1)
:= mapF (Slice_op u) a.
Lemma Slice_fun_skipF0: ∀ {d n} u (a:'I_n → 'nat^d.+1) i,
skipF (Slice_fun u a i) ord0 = a i.
Proof.
intros d n u a i.
unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
apply extF; intros j.
unfold skipF, castF, concatF.
case (lt_dec _ _).
intros V; contradict V.
simpl; unfold bump; simpl; auto with arith.
intros V; f_equal.
apply ord_inj; simpl; unfold bump; simpl; auto with arith.
Qed.
Lemma grsymlex_lt_Slice_fun_monot : ∀ {d n} u (alpha:'I_n → 'nat^d)
(i j:'I_n), (i < j)%coq_nat →
grsymlex_lt (alpha i) (alpha j) →
grsymlex_lt (Slice_fun u alpha i) (Slice_fun u alpha j).
Proof.
intros d; induction d.
intros n u alpha i j H1 H.
contradict H; apply grsymlex_lt_nil.
intros n u alpha i j H1 H'.
assert (H'2 : grsymlex_lt (alpha i) (alpha j)) by assumption.
rewrite grsymlex_lt_S in H'; case H'.
intros H2; left.
rewrite (Slice_op_sum _ (sum (alpha i)+u)%coq_nat u); auto with arith.
rewrite (Slice_op_sum _ (sum (alpha j)+u)%coq_nat u); auto with arith.
now rewrite Nat.add_sub.
now rewrite Nat.add_sub.
intros (H2,H3).
rewrite grsymlex_lt_S;right; split.
rewrite (Slice_op_sum _ (sum (alpha i)+u)%coq_nat u); auto with arith.
rewrite (Slice_op_sum _ (sum (alpha j)+u)%coq_nat u); auto with arith.
now rewrite Nat.add_sub.
now rewrite Nat.add_sub.
rewrite 2!Slice_fun_skipF0; easy.
Qed.
Lemma grsymlex_lt_Slice_fun_sortedF : ∀ {d n} u (alpha:'I_n → 'nat^d),
sortedF grsymlex_lt alpha → sortedF grsymlex_lt (Slice_fun u alpha).
Proof.
intros d n u alpha H i j H1.
apply grsymlex_lt_Slice_fun_monot; try easy.
apply H; easy.
Qed.
Lemma CSdk_aux : ∀ (d k:nat),
(sum (succF (fun i : 'I_k.+1 ⇒ pbinom d i))).-1 = pbinom d.+1 k.
Proof.
intros d k.
rewrite pbinomS_rising_sum_l; easy.
Qed.
Fixpoint CSdk (d k :nat) {struct d} : 'I_((pbinom d k).+1) → 'nat^d.+1
:= match d with
| O ⇒ fun _ _ ⇒ k
| S dd ⇒ castF (pbinomS_rising_sum_l dd k)
(concatnF (fun i:'I_k.+1 ⇒ Slice_fun (k-i)%coq_nat (CSdk dd i)))
end.
Lemma CS0k_eq : ∀ k, CSdk 0 k = fun _ _ ⇒ k.
Proof.
easy.
Qed.
Lemma CSdk_eq : ∀ d k,
CSdk d.+1 k = castF (pbinomS_rising_sum_l d k)
(concatnF (fun i:'I_k.+1 ⇒ Slice_fun (k-i)%coq_nat (CSdk d i))).
Proof.
intros d k.
apply extF; intros i; simpl; unfold castF; f_equal.
Qed.
Lemma CSdk_ext : ∀ d k1 k2 i1 i2,
k1 = k2 → nat_of_ord i1 = nat_of_ord i2 →
CSdk d k1 i1 = CSdk d k2 i2.
Proof.
intros d k1 k2 i1 i2 Hk Hi; subst.
f_equal; apply ord_inj; easy.
Qed.
Lemma CSdk_sum : ∀ d k i, sum (CSdk d k i) = k.
Proof.
intros d; induction d.
intros k i.
rewrite sum_1.
rewrite CS0k_eq; easy.
intros k i.
rewrite CSdk_eq.
unfold castF.
rewrite (splitn_ord (cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)).
rewrite concatn_ord_correct.
unfold Slice_fun; rewrite mapF_correct.
apply Slice_op_sum.
auto with arith zarith.
rewrite IHd.
assert (splitn_ord1
(cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)< k.+1)%coq_nat.
apply /ltP; easy.
apply eq_sym, Nat.add_sub_eq_l.
auto with arith zarith.
Qed.
Lemma CSd0_eq : ∀ d, CSdk d 0 = fun _ ⇒ constF d.+1 0.
Proof.
intros d; case d.
rewrite CS0k_eq; easy.
clear d; intros d.
apply extF; intros i.
apply extF; intros j.
rewrite constF_correct.
assert (V: sum (CSdk d.+1 0 i) = 0).
apply CSdk_sum; auto with arith.
case_eq (CSdk d.+1 0 i j); try easy.
intros m Hm.
absurd (1 ≤ sum (CSdk d.+1 0 i))%coq_nat.
rewrite V; auto with arith.
apply Nat.le_trans with (2:=sum_ub_nat _ j).
rewrite Hm; auto with arith.
Qed.
Lemma CSd1_eq_aux : ∀ d, d.+1 = (pbinom d 1).+1.
Proof.
intros d; now rewrite pbinom_1_r.
Qed.
Lemma CSd1_eq : ∀ d,
CSdk d 1 = castF (CSd1_eq_aux d) (itemF d.+1 1).
Proof.
intros d; induction d.
rewrite CS0k_eq.
apply extF; intros i; apply extF; intros j.
rewrite !I_1_is_unit; unfold castF.
rewrite itemF_correct_l; try easy.
apply ord_inj; easy.
rewrite CSdk_eq.
rewrite concatnF_two.
2: apply (inhabits zero).
simpl (nat_of_ord ord0); simpl (nat_of_ord ord_max).
replace (1-0)%coq_nat with 1 by auto with arith.
replace (1-1)%coq_nat with 0 by auto with arith.
rewrite CSd0_eq IHd.
rewrite (itemF_ind_l d.+1).
rewrite castF_comp.
apply: concatF_castF_eq.
apply pbinomS_0_r.
apply pbinomS_1_r.
intros K1; apply extF; intros i; unfold castF, Slice_fun; simpl.
rewrite mapF_correct; unfold Slice_op.
unfold singleF; rewrite constF_correct.
unfold itemF.
apply extF; intros j; unfold castF.
case (ord_eq_dec j ord0); intros Hj.
rewrite replaceF_correct_l; try easy.
rewrite concatF_correct_l; try easy.
rewrite Hj; simpl; auto with arith.
rewrite replaceF_correct_r; try easy.
rewrite concatF_correct_r; try easy.
simpl; assert (nat_of_ord j ≠ 0)%coq_nat; auto with arith.
intros T; apply Hj; apply ord_inj; easy.
apply Nat.le_ngt; auto with zarith.
intros K1; rewrite mapF_correct.
apply extF; intros i.
unfold castF, Slice_fun; simpl.
rewrite mapF_correct; unfold Slice_op.
apply extF; intros j; unfold castF.
f_equal.
f_equal.
apply ord_inj; easy.
apply ord_inj; easy.
Qed.
Lemma CSdk_head : ∀ d k,
CSdk d k ord0 = itemF d.+1 k ord0.
Proof.
intros d; induction d.
intros k; rewrite CS0k_eq.
apply extF; intros i.
unfold itemF, replaceF; simpl.
rewrite I_1_is_unit; case (ord_eq_dec _ _); easy.
intros k; rewrite CSdk_eq.
unfold castF; apply extF; intros i.
rewrite concatnF_splitn_ord.
unfold Slice_fun; rewrite mapF_correct; unfold Slice_op, castF.
rewrite splitn_ord2_0; try easy; auto with arith.
rewrite IHd.
rewrite splitn_ord1_0; try easy; auto with arith.
case (ord_eq_dec i ord0); intros Hi.
rewrite Hi concatF_correct_l singleF_0.
rewrite itemF_diag; simpl; auto with arith.
rewrite concatF_correct_r.
simpl; intros V; apply Hi; apply ord_inj; simpl; auto with zarith.
intros K.
rewrite itemF_zero_compat; try easy.
rewrite fct_zero_eq.
rewrite itemF_correct_r; try easy.
Qed.
Lemma CSdk_last : ∀ d k,
CSdk d k ord_max = itemF d.+1 k ord_max.
Proof.
intros d; induction d.
intros k; rewrite CS0k_eq.
apply extF; intros i.
unfold castF; simpl; rewrite 2!I_1_is_unit; simpl.
rewrite itemF_diag; try easy.
intros k; rewrite CSdk_eq.
generalize (CSdk_aux d k); intros H1.
unfold castF.
rewrite concatnF_splitn_ord.
rewrite splitn_ord2_max; try easy.
unfold Slice_fun, Slice_op; rewrite mapF_correct.
rewrite IHd.
replace ((k -
splitn_ord1
(cast_ord (eq_sym (pbinomS_rising_sum_l d k)) ord_max))) with 0 at 1.
unfold castF; apply extF; intros i.
rewrite splitn_ord1_max; simpl; try easy.
case (ord_eq_dec i ord_max); intros Hi.
rewrite Hi concatF_correct_r.
simpl; auto with zarith.
intros K; replace (concat_r_ord K) with (ord_max:'I_d.+1).
rewrite 2!itemF_diag; simpl; auto with arith.
apply ord_inj; simpl; auto with arith.
rewrite itemF_correct_r; try easy.
case (ord_eq_dec i ord0); intros Hi2.
rewrite Hi2; rewrite concatF_correct_l; try easy.
rewrite concatF_correct_r; try easy.
simpl; intros V; apply Hi2; apply ord_inj; simpl; auto with zarith.
intros K; rewrite itemF_correct_r; try easy.
apply ord_neq; simpl; rewrite -minusE; intros V; apply Hi.
apply ord_inj; simpl.
assert (nat_of_ord i ≠ 0); auto with zarith arith.
intros V'; apply Hi2; apply ord_inj; easy.
rewrite splitn_ord1_max; simpl; try easy; auto with arith.
Qed.
Lemma CSdk_grsymlex_lt_aux : ∀ {n} (A B :'nat^n.+1) i,
sum A = sum B → (B i < A i)%coq_nat →
(sum (skipF A i) < sum (skipF B i))%coq_nat.
Proof.
intros n A B i H1 H2.
apply Nat.add_lt_mono_l with (A i).
apply Nat.le_lt_trans with (sum A).
rewrite (sum_skipF A i); unfold plus; simpl; auto with arith.
rewrite H1; rewrite (sum_skipF B i).
unfold plus; simpl.
apply Nat.add_lt_mono_r; auto with arith.
Qed.
Lemma CSdk_grsymlex_lt : ∀ d k, sortedF grsymlex_lt (CSdk d k).
Proof.
intros d; induction d.
intros k; apply (sortedF_castF_rev (pbinomS_0_l _)).
intros i j H.
contradict H; rewrite 2!I_1_is_unit; auto with arith.
intros k; rewrite CSdk_eq.
apply sortedF_castF.
apply concatnF_order.
apply is_smitt_trans, is_smitt_grsymlex_lt.
intros i; apply grsymlex_lt_Slice_fun_sortedF.
apply IHd.
intros i Him.
rewrite grsymlex_lt_S; right.
assert (i < k)%coq_nat.
assert (nat_of_ord i ≠ k)%coq_nat.
intros V; apply Him.
apply ord_inj; rewrite V; simpl; auto with arith.
assert (i < k.+1)%coq_nat; try auto with zarith.
apply /ltP; easy.
split.
rewrite (Slice_op_sum _ k); try auto with arith zarith.
rewrite (Slice_op_sum _ k); try auto with arith zarith.
rewrite CSdk_head sum_itemF.
simpl; rewrite bump_r; auto with zarith.
rewrite CSdk_last sum_itemF; simpl; auto with arith zarith.
left.
apply CSdk_grsymlex_lt_aux.
rewrite (Slice_op_sum _ k); try auto with zarith.
rewrite (Slice_op_sum _ k); try auto with zarith.
rewrite CSdk_head sum_itemF.
simpl; rewrite bump_r; auto with zarith arith.
rewrite CSdk_last sum_itemF; simpl; auto with arith zarith.
unfold Slice_fun, Slice_op; rewrite 2!mapF_correct; simpl.
unfold castF; rewrite 2!concatF_correct_l; simpl.
rewrite 2!singleF_0.
rewrite bump_r; auto with zarith arith.
Qed.
Lemma CSdk_surj : ∀ d k, ∀ b : 'nat^d.+1,
sum b = k → { i | b = CSdk d k i }.
Proof.
intros d; induction d.
intros k b.
rewrite sum_1; intros H.
∃ ord0.
rewrite CS0k_eq.
apply extF; intros i.
rewrite I_1_is_unit; easy.
intros k b Hb.
destruct (Slice_op_correct k b Hb) as ((u,beta),(Hu1,(Hu2,Hu3))).
destruct (IHd (k-u)%coq_nat beta Hu2) as (i1,Hi1).
rewrite CSdk_eq.
assert (Vu : (k - u < k.+1)).
apply /ltP; rewrite -minusE; auto with arith zarith.
assert (K : ((sum (succF (fun i : 'I_k.+1 ⇒ pbinom d i))) =
(pbinom (d.+2.-1) k).+1)).
rewrite -CSdk_aux.
assert (T: (0 < sum (succF (fun i : 'I_k.+1 ⇒ pbinom d i)))%coq_nat).
apply Nat.lt_le_trans with ((pbinom d 0).+1); auto with arith.
apply (sum_ub_nat (succF (fun i : 'I_k.+1 ⇒ pbinom d i)) ord0).
generalize T; case (sum (succF (fun i : 'I_k.+1 ⇒ pbinom d i))); auto with zarith arith.
∃ (cast_ord K (concatn_ord _ (Ordinal Vu) i1)).
apply extF; intros z; unfold castF.
rewrite (concatn_ord_correct' _ _ (Ordinal Vu) i1).
2: now simpl.
rewrite -Hu3 Hi1.
unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
unfold castF; f_equal; f_equal; simpl.
apply eq_sym, Nat.add_sub_eq_l; auto with arith zarith.
apply Nat.sub_add; easy.
Qed.
Lemma CSdk_inj : ∀ d k,
injective (CSdk d k).
Proof.
intros d k; apply sortedF_inj with grsymlex_lt.
apply is_smitt_irrefl, is_smitt_grsymlex_lt.
apply CSdk_grsymlex_lt.
Qed.
Lemma Adk_aux : ∀ d k,
sum (fun i : 'I_k.+1 ⇒ (pbinom d i).+1) = (pbinom d.+1 k).+1.
Proof.
intros d k; rewrite pbinomS_rising_sum_l; easy.
Qed.
[RR9557v1]
Def 1486, p. 67.
See also Lem 1496, p. 70.
See also Lem 1496, p. 70.
Definition Adk (d k :nat) : 'I_((pbinom d k).+1) → 'nat^d
:= match d with
| 0 ⇒ zero
| S dd ⇒ castF (pbinomS_rising_sum_l dd k)
(concatnF (fun i:'I_k.+1 ⇒ CSdk dd i))
end.
Lemma A0k_eq : ∀ k, Adk O k = zero.
Proof.
intros k; easy.
Qed.
Lemma AdSk_eq_aux : ∀ d k,
((pbinom d.+1 k).+1 +
(pbinom d k.+1).+1)%coq_nat =
(pbinom d.+1 k.+1).+1.
Proof.
intros d k; rewrite Nat.add_comm.
apply pbinomS_pascal.
Qed.
Lemma AdSk_eq : ∀ d k,
Adk d.+1 k.+1
= castF (AdSk_eq_aux d k) (concatF (Adk d.+1 k) (CSdk d k.+1)).
Proof.
intros d k; unfold Adk.
rewrite concatnF_ind_r.
rewrite castF_comp.
apply: concatF_castF_eq.
rewrite Adk_aux; easy.
intros K.
apply extF; intros i; unfold castF; f_equal.
apply ord_inj; easy.
now rewrite castF_id.
Qed.
Lemma Adk_ext : ∀ d k1 k2 i1 i2,
k1 = k2 → nat_of_ord i1 = nat_of_ord i2 →
Adk d k1 i1 = Adk d k2 i2.
Proof.
intros d k1 k2 i1 i2 Hk Hi; subst.
f_equal; apply ord_inj; easy.
Qed.
Lemma Ad1_eq_aux : ∀ d, (1 + d = (pbinom d 1).+1).
Proof.
intros d.
rewrite pbinomS_1_r; easy.
Qed.
:= match d with
| 0 ⇒ zero
| S dd ⇒ castF (pbinomS_rising_sum_l dd k)
(concatnF (fun i:'I_k.+1 ⇒ CSdk dd i))
end.
Lemma A0k_eq : ∀ k, Adk O k = zero.
Proof.
intros k; easy.
Qed.
Lemma AdSk_eq_aux : ∀ d k,
((pbinom d.+1 k).+1 +
(pbinom d k.+1).+1)%coq_nat =
(pbinom d.+1 k.+1).+1.
Proof.
intros d k; rewrite Nat.add_comm.
apply pbinomS_pascal.
Qed.
Lemma AdSk_eq : ∀ d k,
Adk d.+1 k.+1
= castF (AdSk_eq_aux d k) (concatF (Adk d.+1 k) (CSdk d k.+1)).
Proof.
intros d k; unfold Adk.
rewrite concatnF_ind_r.
rewrite castF_comp.
apply: concatF_castF_eq.
rewrite Adk_aux; easy.
intros K.
apply extF; intros i; unfold castF; f_equal.
apply ord_inj; easy.
now rewrite castF_id.
Qed.
Lemma Adk_ext : ∀ d k1 k2 i1 i2,
k1 = k2 → nat_of_ord i1 = nat_of_ord i2 →
Adk d k1 i1 = Adk d k2 i2.
Proof.
intros d k1 k2 i1 i2 Hk Hi; subst.
f_equal; apply ord_inj; easy.
Qed.
Lemma Ad1_eq_aux : ∀ d, (1 + d = (pbinom d 1).+1).
Proof.
intros d.
rewrite pbinomS_1_r; easy.
Qed.
[RR9557v1]
Lem 1497, Eq (9.14), p. 70.
Lemma Ad1_eq : ∀ d,
Adk d 1 = castF (Ad1_eq_aux d)
(concatF (singleF (constF d 0))
(itemF d 1)).
Proof.
intros d; case d.
rewrite A0k_eq; simpl.
apply extF; intros i; unfold castF, singleF, constF.
rewrite concatF_nil_r.
unfold castF; simpl; easy.
clear d; intros d.
unfold Adk, singleF.
rewrite concatnF_two.
2: apply (inhabits zero).
rewrite CSd0_eq.
rewrite CSd1_eq.
rewrite castF_comp.
assert (K: (pbinom d.+1.-1 0).+1 = 1) by apply pbinomS_0_r.
apply concatF_castF_eq with (H3:=K)
(H4:= eq_sym ((CSd1_eq_aux d))).
unfold constF; easy.
apply extF; intros i; unfold castF; f_equal.
apply ord_inj; easy.
Qed.
Lemma Ad1_S : ∀ d ipk (H : ipk ≠ ord0),
Adk d 1 ipk = itemF d 1 (cast_ord (pbinom_1_r d) (lower_S H)).
Proof.
intros d ipk H.
rewrite Ad1_eq; unfold castF.
rewrite concatF_correct_r.
simpl; intros K; apply H.
apply ord_inj; simpl; auto with zarith.
intros K; f_equal.
apply ord_inj; easy.
Qed.
Lemma Adk_sum : ∀ d k i,
(sum (Adk d k i) ≤ k)%coq_nat.
Proof.
intros d; case d; clear d.
intros k i; rewrite A0k_eq.
rewrite sum_zero; simpl; auto with arith.
intros d k i.
unfold Adk, castF.
rewrite (splitn_ord (cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)).
rewrite concatn_ord_correct.
rewrite CSdk_sum; auto with arith.
assert (splitn_ord1
(cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)< k.+1)%coq_nat; auto with arith.
apply /ltP; easy.
Qed.
Lemma Adk_le : ∀ d k i j,
(Adk d k i j ≤ k)%coq_nat.
Proof.
intros d k i j.
apply Nat.le_trans with (2:= Adk_sum d k i).
apply sum_ub_nat.
Qed.
Lemma Adk_surj : ∀ d k (b:'nat^d),
(sum b ≤ k)%coq_nat → { i | b = Adk d k i }.
Proof.
intros d; case d; clear d.
intros k b H.
∃ ord0.
apply extF; intros [i Hi]; easy.
intros d k b Hb.
destruct (CSdk_surj d (sum b) b) as(j,Hj); try auto with arith.
assert (V: (sum b < k.+1)).
apply /ltP; auto with arith.
∃ (cast_ord (Adk_aux d k)
(concatn_ord (fun i : 'I_k.+1 ⇒ (pbinom (d.+1.-1) i).+1)
(Ordinal V) j)).
unfold Adk, castF.
rewrite cast_ord_comp; unfold etrans; rewrite cast_ord_id.
rewrite concatn_ord_correct.
easy.
Qed.
Lemma Adk_grsymlex_lt : ∀ d k,
sortedF grsymlex_lt (Adk d k).
Proof.
intros d; case d; clear d.
intros k; apply (sortedF_castF_rev (pbinomS_0_l _)).
intros i j H.
contradict H; rewrite !I_1_is_unit; easy.
intros d k; unfold Adk.
apply sortedF_castF.
apply concatnF_order.
apply is_smitt_trans, is_smitt_grsymlex_lt.
intros i; apply CSdk_grsymlex_lt; auto with arith.
intros i Him.
apply sum_order_graded.
rewrite CSdk_sum; auto with arith.
rewrite CSdk_sum; auto with arith.
Qed.
Lemma Adk_inj : ∀ d k,
injective (Adk d k).
Proof.
intros d k; apply sortedF_inj with grsymlex_lt.
apply is_smitt_irrefl, is_smitt_grsymlex_lt.
apply Adk_grsymlex_lt.
Qed.
Definition Adk_inv (d k:nat) (b:'nat^d) : 'I_((pbinom d k).+1) :=
match (le_dec (sum b) k) with
| left H ⇒
proj1_sig (Adk_surj d k b H)
| right _ ⇒ ord0
end.
Lemma Adk_inv_correct_r : ∀ d k (b:'nat^d),
(sum b ≤ k)%coq_nat →
Adk d k (Adk_inv d k b) = b.
Proof.
intros d k b H; unfold Adk_inv.
case (le_dec (sum b) k); try easy.
intros H'.
destruct (Adk_surj _ _ _ _); easy.
Qed.
Lemma Adk_inv_correct_l : ∀ d k i,
Adk_inv d k (Adk d k i) = i.
Proof.
intros d k i; unfold Adk_inv.
case (le_dec _ k); intros H; simpl.
destruct (Adk_surj _ _ _ _).
simpl; apply Adk_inj; easy.
contradict H; apply Adk_sum.
Qed.
Lemma Adk_0 : ∀ d k,
Adk d k ord0 = zero.
Proof.
intros d k; unfold Adk; case d; try easy.
clear d; intros d; unfold castF; rewrite concatnF_splitn_ord.
rewrite splitn_ord2_0; try easy.
rewrite splitn_ord1_0; try easy.
rewrite CSd0_eq; easy.
Qed.
Adk d 1 = castF (Ad1_eq_aux d)
(concatF (singleF (constF d 0))
(itemF d 1)).
Proof.
intros d; case d.
rewrite A0k_eq; simpl.
apply extF; intros i; unfold castF, singleF, constF.
rewrite concatF_nil_r.
unfold castF; simpl; easy.
clear d; intros d.
unfold Adk, singleF.
rewrite concatnF_two.
2: apply (inhabits zero).
rewrite CSd0_eq.
rewrite CSd1_eq.
rewrite castF_comp.
assert (K: (pbinom d.+1.-1 0).+1 = 1) by apply pbinomS_0_r.
apply concatF_castF_eq with (H3:=K)
(H4:= eq_sym ((CSd1_eq_aux d))).
unfold constF; easy.
apply extF; intros i; unfold castF; f_equal.
apply ord_inj; easy.
Qed.
Lemma Ad1_S : ∀ d ipk (H : ipk ≠ ord0),
Adk d 1 ipk = itemF d 1 (cast_ord (pbinom_1_r d) (lower_S H)).
Proof.
intros d ipk H.
rewrite Ad1_eq; unfold castF.
rewrite concatF_correct_r.
simpl; intros K; apply H.
apply ord_inj; simpl; auto with zarith.
intros K; f_equal.
apply ord_inj; easy.
Qed.
Lemma Adk_sum : ∀ d k i,
(sum (Adk d k i) ≤ k)%coq_nat.
Proof.
intros d; case d; clear d.
intros k i; rewrite A0k_eq.
rewrite sum_zero; simpl; auto with arith.
intros d k i.
unfold Adk, castF.
rewrite (splitn_ord (cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)).
rewrite concatn_ord_correct.
rewrite CSdk_sum; auto with arith.
assert (splitn_ord1
(cast_ord (eq_sym (pbinomS_rising_sum_l d k)) i)< k.+1)%coq_nat; auto with arith.
apply /ltP; easy.
Qed.
Lemma Adk_le : ∀ d k i j,
(Adk d k i j ≤ k)%coq_nat.
Proof.
intros d k i j.
apply Nat.le_trans with (2:= Adk_sum d k i).
apply sum_ub_nat.
Qed.
Lemma Adk_surj : ∀ d k (b:'nat^d),
(sum b ≤ k)%coq_nat → { i | b = Adk d k i }.
Proof.
intros d; case d; clear d.
intros k b H.
∃ ord0.
apply extF; intros [i Hi]; easy.
intros d k b Hb.
destruct (CSdk_surj d (sum b) b) as(j,Hj); try auto with arith.
assert (V: (sum b < k.+1)).
apply /ltP; auto with arith.
∃ (cast_ord (Adk_aux d k)
(concatn_ord (fun i : 'I_k.+1 ⇒ (pbinom (d.+1.-1) i).+1)
(Ordinal V) j)).
unfold Adk, castF.
rewrite cast_ord_comp; unfold etrans; rewrite cast_ord_id.
rewrite concatn_ord_correct.
easy.
Qed.
Lemma Adk_grsymlex_lt : ∀ d k,
sortedF grsymlex_lt (Adk d k).
Proof.
intros d; case d; clear d.
intros k; apply (sortedF_castF_rev (pbinomS_0_l _)).
intros i j H.
contradict H; rewrite !I_1_is_unit; easy.
intros d k; unfold Adk.
apply sortedF_castF.
apply concatnF_order.
apply is_smitt_trans, is_smitt_grsymlex_lt.
intros i; apply CSdk_grsymlex_lt; auto with arith.
intros i Him.
apply sum_order_graded.
rewrite CSdk_sum; auto with arith.
rewrite CSdk_sum; auto with arith.
Qed.
Lemma Adk_inj : ∀ d k,
injective (Adk d k).
Proof.
intros d k; apply sortedF_inj with grsymlex_lt.
apply is_smitt_irrefl, is_smitt_grsymlex_lt.
apply Adk_grsymlex_lt.
Qed.
Definition Adk_inv (d k:nat) (b:'nat^d) : 'I_((pbinom d k).+1) :=
match (le_dec (sum b) k) with
| left H ⇒
proj1_sig (Adk_surj d k b H)
| right _ ⇒ ord0
end.
Lemma Adk_inv_correct_r : ∀ d k (b:'nat^d),
(sum b ≤ k)%coq_nat →
Adk d k (Adk_inv d k b) = b.
Proof.
intros d k b H; unfold Adk_inv.
case (le_dec (sum b) k); try easy.
intros H'.
destruct (Adk_surj _ _ _ _); easy.
Qed.
Lemma Adk_inv_correct_l : ∀ d k i,
Adk_inv d k (Adk d k i) = i.
Proof.
intros d k i; unfold Adk_inv.
case (le_dec _ k); intros H; simpl.
destruct (Adk_surj _ _ _ _).
simpl; apply Adk_inj; easy.
contradict H; apply Adk_sum.
Qed.
Lemma Adk_0 : ∀ d k,
Adk d k ord0 = zero.
Proof.
intros d k; unfold Adk; case d; try easy.
clear d; intros d; unfold castF; rewrite concatnF_splitn_ord.
rewrite splitn_ord2_0; try easy.
rewrite splitn_ord1_0; try easy.
rewrite CSd0_eq; easy.
Qed.
[RR9557v1]
Lem 1497, Eq (9.12), p. 70.
Lemma A1k_eq' : ∀ k,
Adk 1 k = fun i j ⇒ i.
Proof.
intros k; induction k.
apply extF; intros i; apply extF; intros j.
unfold Adk, castF; rewrite concatnF_one.
2: apply (inhabits zero).
rewrite CSd0_eq; unfold castF; simpl.
rewrite constF_correct.
rewrite I_1_is_unit; easy.
apply extF; intros i; apply extF; intros j.
rewrite AdSk_eq; unfold castF.
rewrite IHk CS0k_eq.
case (ord_eq_dec i ord_max); intros Hi.
rewrite concatF_correct_r.
rewrite Hi; simpl.
rewrite pbinom_1_l pbinomS_1_l; auto with arith.
rewrite Hi; simpl.
rewrite pbinom_1_l; easy.
rewrite concatF_correct_l; try easy.
simpl.
replace _.+1 with k.+1 by now rewrite pbinomS_1_l.
apply Nat.lt_succ_r, nat_le_S_neq.
apply Nat.lt_succ_r; apply /ltP.
rewrite -(pbinomS_1_l k.+1); easy.
contradict Hi; apply ord_inj; rewrite Hi.
rewrite pbinom_1_l; easy.
Qed.
Adk 1 k = fun i j ⇒ i.
Proof.
intros k; induction k.
apply extF; intros i; apply extF; intros j.
unfold Adk, castF; rewrite concatnF_one.
2: apply (inhabits zero).
rewrite CSd0_eq; unfold castF; simpl.
rewrite constF_correct.
rewrite I_1_is_unit; easy.
apply extF; intros i; apply extF; intros j.
rewrite AdSk_eq; unfold castF.
rewrite IHk CS0k_eq.
case (ord_eq_dec i ord_max); intros Hi.
rewrite concatF_correct_r.
rewrite Hi; simpl.
rewrite pbinom_1_l pbinomS_1_l; auto with arith.
rewrite Hi; simpl.
rewrite pbinom_1_l; easy.
rewrite concatF_correct_l; try easy.
simpl.
replace _.+1 with k.+1 by now rewrite pbinomS_1_l.
apply Nat.lt_succ_r, nat_le_S_neq.
apply Nat.lt_succ_r; apply /ltP.
rewrite -(pbinomS_1_l k.+1); easy.
contradict Hi; apply ord_inj; rewrite Hi.
rewrite pbinom_1_l; easy.
Qed.
[RR9557v1]
Lem 1497, Eq (9.12), p. 70.
Lemma A1k_eq : ∀ k,
Adk 1 k = constF 1.
Proof.
intros k; apply extF; intros i; apply extF; intros j.
rewrite constF_correct.
unfold Adk, castF.
rewrite concatnF_splitn_ord CS0k_eq.
assert (H: (pbinom 1 k).+1 = k.+1) by apply pbinomS_1_l.
apply trans_eq with (nat_of_ord (cast_ord H i)); try easy; f_equal.
assert (K: i < sum (succF (fun i:'I_k.+1 ⇒ (pbinom 1.-1 i)))).
simpl.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat Nat.mul_1_r.
rewrite -(pbinomS_1_l k); easy.
apply extF; intros z; rewrite constF_correct.
rewrite succF_correct.
apply pbinomS_0_l.
apply splitn_ord1_inj with (k:= Ordinal K).
replace (nat_of_ord (Ordinal K))
with (nat_of_ord (cast_ord (eq_sym (pbinomS_rising_sum_l 0 k)) i)); try easy.
apply splitn_ord1_correct.
simpl; split; unfold sum_part.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat.
simpl; auto with zarith.
simpl; apply extF; intros z.
rewrite constF_correct.
unfold castF_nip, firstF, castF; simpl.
rewrite succF_correct; simpl.
apply pbinomS_0_l.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat.
simpl; auto with zarith.
simpl; apply extF; intros z.
rewrite constF_correct.
unfold castF_nip, firstF, castF; simpl.
rewrite succF_correct; simpl.
apply pbinomS_0_l.
Qed.
Lemma Adk_last_layer : ∀ d k ipk,
(0 < d)%coq_nat → (0 < k)%coq_nat →
(sum (Adk d k ipk) = k)%coq_nat ↔
((pbinom d k.-1).+1 ≤ ipk)%coq_nat.
Proof.
intros d; case d; try easy; clear d.
intros d k ; case k; try easy; clear k.
intros k i _ _ ; unfold Adk; unfold castF.
pose (i':=(cast_ord (eq_sym (pbinomS_rising_sum_l d k.+1)) i)).
assert (Hi : nat_of_ord i = nat_of_ord i') by easy.
rewrite (sum_ext _ (concatnF (CSdk d) i')).
2: intros j; easy.
rewrite concatnF_splitn_ord.
rewrite CSdk_sum; auto with arith.
split; intros H.
destruct (splitn_ord1_correct i') as (Y1,_).
rewrite Hi.
apply Nat.le_trans with (2:=Y1).
apply Nat.add_le_mono_r with ((pbinom d.+1.-1 (splitn_ord1 i')).+1).
apply Nat.eq_le_incl.
generalize (sum_part_ind_r (fun i0 : 'I_k.+2 ⇒ (pbinom d.+1.-1 i0).+1)
(splitn_ord1 i')); unfold plus; simpl(AbelianMonoid.plus _ _).
intros T; rewrite -T; clear T.
replace (lift_S (splitn_ord1 i')) with (ord_max:'I_k.+3).
rewrite sum_part_ord_max.
rewrite (Adk_aux d k.+1) H.
rewrite -pbinomS_pascal Nat.add_comm pbinomS_sym; easy.
apply ord_inj.
rewrite lift_S_correct H; easy.
apply trans_eq with (nat_of_ord (ord_max:'I_k.+2)); try easy; f_equal.
apply splitn_ord1_inj with i'.
apply splitn_ord1_correct.
split.
rewrite -Hi.
apply Nat.le_trans with (2:=H).
apply Nat.add_le_mono_r with ((pbinom d.+1.-1 (ord_max:'I_k.+2)).+1).
apply Nat.eq_le_incl.
generalize (sum_part_ind_r (fun i0 : 'I_k.+2 ⇒ (pbinom d.+1.-1 i0).+1)
(ord_max)); unfold plus; simpl(AbelianMonoid.plus _ _).
intros T; rewrite -T; clear T.
replace (lift_S (ord_max)) with (ord_max:'I_k.+3).
2: apply ord_inj; easy.
rewrite sum_part_ord_max.
rewrite (Adk_aux d k.+1).
rewrite -pbinomS_pascal Nat.add_comm pbinomS_sym; easy.
replace (lift_S ord_max) with (ord_max:'I_k.+3).
2: apply ord_inj; easy.
rewrite sum_part_ord_max.
rewrite -Hi.
apply Nat.lt_le_trans with ((pbinom d.+1 k.+1).+1).
apply /ltP; easy.
apply Nat.eq_le_incl.
rewrite -(Adk_aux d k.+1).
apply sum_ext; easy.
Qed.
Lemma Adk_previous_layer : ∀ d k i1 (i2 : 'I_(pbinom d k).+1),
nat_of_ord i1 = i2 →
Adk d k.-1 i1 = Adk d k i2.
Proof.
intros d; case d; clear d.
intros k i1 i2 H.
rewrite 2!A0k_eq; easy.
intros d k; case k; clear k.
intros i1 i2 H.
apply Adk_ext; easy.
intros k i1 i2 H.
rewrite AdSk_eq; unfold castF.
rewrite concatF_correct_l.
simpl; rewrite -H.
apply /ltP; easy.
intros K; f_equal.
apply ord_inj; easy.
Qed.
Lemma Adk_kron : ∀ d k i,
mapF INR (Adk d k (Adk_inv d k (itemF d k i))) =
(fun j ⇒ (INR k × kronR i j)%K).
Proof.
intros d k i.
rewrite Adk_inv_correct_r.
rewrite -itemF_kron_eq.
apply mapF_itemF_0; easy.
rewrite sum_itemF; easy.
Qed.
End MI_Def.
Adk 1 k = constF 1.
Proof.
intros k; apply extF; intros i; apply extF; intros j.
rewrite constF_correct.
unfold Adk, castF.
rewrite concatnF_splitn_ord CS0k_eq.
assert (H: (pbinom 1 k).+1 = k.+1) by apply pbinomS_1_l.
apply trans_eq with (nat_of_ord (cast_ord H i)); try easy; f_equal.
assert (K: i < sum (succF (fun i:'I_k.+1 ⇒ (pbinom 1.-1 i)))).
simpl.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat Nat.mul_1_r.
rewrite -(pbinomS_1_l k); easy.
apply extF; intros z; rewrite constF_correct.
rewrite succF_correct.
apply pbinomS_0_l.
apply splitn_ord1_inj with (k:= Ordinal K).
replace (nat_of_ord (Ordinal K))
with (nat_of_ord (cast_ord (eq_sym (pbinomS_rising_sum_l 0 k)) i)); try easy.
apply splitn_ord1_correct.
simpl; split; unfold sum_part.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat.
simpl; auto with zarith.
simpl; apply extF; intros z.
rewrite constF_correct.
unfold castF_nip, firstF, castF; simpl.
rewrite succF_correct; simpl.
apply pbinomS_0_l.
rewrite (sum_eq _ (constF _ 1)).
rewrite sum_constF_nat.
simpl; auto with zarith.
simpl; apply extF; intros z.
rewrite constF_correct.
unfold castF_nip, firstF, castF; simpl.
rewrite succF_correct; simpl.
apply pbinomS_0_l.
Qed.
Lemma Adk_last_layer : ∀ d k ipk,
(0 < d)%coq_nat → (0 < k)%coq_nat →
(sum (Adk d k ipk) = k)%coq_nat ↔
((pbinom d k.-1).+1 ≤ ipk)%coq_nat.
Proof.
intros d; case d; try easy; clear d.
intros d k ; case k; try easy; clear k.
intros k i _ _ ; unfold Adk; unfold castF.
pose (i':=(cast_ord (eq_sym (pbinomS_rising_sum_l d k.+1)) i)).
assert (Hi : nat_of_ord i = nat_of_ord i') by easy.
rewrite (sum_ext _ (concatnF (CSdk d) i')).
2: intros j; easy.
rewrite concatnF_splitn_ord.
rewrite CSdk_sum; auto with arith.
split; intros H.
destruct (splitn_ord1_correct i') as (Y1,_).
rewrite Hi.
apply Nat.le_trans with (2:=Y1).
apply Nat.add_le_mono_r with ((pbinom d.+1.-1 (splitn_ord1 i')).+1).
apply Nat.eq_le_incl.
generalize (sum_part_ind_r (fun i0 : 'I_k.+2 ⇒ (pbinom d.+1.-1 i0).+1)
(splitn_ord1 i')); unfold plus; simpl(AbelianMonoid.plus _ _).
intros T; rewrite -T; clear T.
replace (lift_S (splitn_ord1 i')) with (ord_max:'I_k.+3).
rewrite sum_part_ord_max.
rewrite (Adk_aux d k.+1) H.
rewrite -pbinomS_pascal Nat.add_comm pbinomS_sym; easy.
apply ord_inj.
rewrite lift_S_correct H; easy.
apply trans_eq with (nat_of_ord (ord_max:'I_k.+2)); try easy; f_equal.
apply splitn_ord1_inj with i'.
apply splitn_ord1_correct.
split.
rewrite -Hi.
apply Nat.le_trans with (2:=H).
apply Nat.add_le_mono_r with ((pbinom d.+1.-1 (ord_max:'I_k.+2)).+1).
apply Nat.eq_le_incl.
generalize (sum_part_ind_r (fun i0 : 'I_k.+2 ⇒ (pbinom d.+1.-1 i0).+1)
(ord_max)); unfold plus; simpl(AbelianMonoid.plus _ _).
intros T; rewrite -T; clear T.
replace (lift_S (ord_max)) with (ord_max:'I_k.+3).
2: apply ord_inj; easy.
rewrite sum_part_ord_max.
rewrite (Adk_aux d k.+1).
rewrite -pbinomS_pascal Nat.add_comm pbinomS_sym; easy.
replace (lift_S ord_max) with (ord_max:'I_k.+3).
2: apply ord_inj; easy.
rewrite sum_part_ord_max.
rewrite -Hi.
apply Nat.lt_le_trans with ((pbinom d.+1 k.+1).+1).
apply /ltP; easy.
apply Nat.eq_le_incl.
rewrite -(Adk_aux d k.+1).
apply sum_ext; easy.
Qed.
Lemma Adk_previous_layer : ∀ d k i1 (i2 : 'I_(pbinom d k).+1),
nat_of_ord i1 = i2 →
Adk d k.-1 i1 = Adk d k i2.
Proof.
intros d; case d; clear d.
intros k i1 i2 H.
rewrite 2!A0k_eq; easy.
intros d k; case k; clear k.
intros i1 i2 H.
apply Adk_ext; easy.
intros k i1 i2 H.
rewrite AdSk_eq; unfold castF.
rewrite concatF_correct_l.
simpl; rewrite -H.
apply /ltP; easy.
intros K; f_equal.
apply ord_inj; easy.
Qed.
Lemma Adk_kron : ∀ d k i,
mapF INR (Adk d k (Adk_inv d k (itemF d k i))) =
(fun j ⇒ (INR k × kronR i j)%K).
Proof.
intros d k i.
rewrite Adk_inv_correct_r.
rewrite -itemF_kron_eq.
apply mapF_itemF_0; easy.
rewrite sum_itemF; easy.
Qed.
End MI_Def.