Library Subsets.ord_compl
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.
Additional definitions and results about ordinals.
Given n : nat, let us recall that 'I_n, ie ordinal n, is the finite
type of natural numbers (strictly) smaller than n.
Its cardinal is n.
It is defined in ssreflect.fintype in the Mathematical Components library.
Naming rules:
Some conventions for the sequel:
The statements are mainly plain-Coq compatible (ie use of Prop instead of
bool).
This module may be used through the import of Subsets.Subsets,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Description
Additional notations
Changes from the Mathematical Components library
- ord1 is renamed I_1_is_unit.
- The new ord1 is the ordinal of value 1, when the bound is (strictly) larger than 1.
Support for specific ordinal transformations
- the results used to define
<transf
> are called<transf>*_proof
; - most transformations are called
<op>_ord
; - some specializations for successor are called
<op>_S
; -
<op>_ord
is used to define<op>F
in Finite_family; -
<op>_S
is used to define<op>F_S
in Finite_family.
-
n..p
means all integers fromn
top
; -
[n..
and..n]
means included the boundn
; -
(n..
and..n)
means excluded the boundn
; -
n..i^..p
means all integers fromn
top
, excepti
. - widen_S is the canonical injection from 'I_n to 'I_n.+1.
It maps [0..n) ⊂ 'I_n into [0..n) ⊂ 'I_n.+1.
- narrow_S is the canonical projection from 'I_n.+1 onto 'I_n, provided
a proof that the (implicit) argument is distinct from the largest ordinal,
of value n.
It maps [0..n) ⊂ 'I_n.+1 onto [0..n) ⊂ 'I_n.
- lift_S is the shift from 'I_n to 'I_n.+1, ie the value is incremented.
It maps [0..n) ⊂ 'I_n into [1..n.+1) ⊂ 'I_n.+1.
- lower_S is the downshift from 'I_n.+1 to 'I_n, ie the value is
decremented, provided a proof that the (implicit) argument is distinct from
the smallest ordinal, of value 0.
It maps [1..n.+1) ⊂ 'I_n.+1 into [0..n) ⊂ 'I_n.
- cast_f_ord H casts any function of type 'I_[n1] into the same function
of type 'I_[n2], provided a proof H : n1 = n2.
- first_ord n2 is the canonical injection from 'I_n1 to 'I_(n1 + n2).
It maps [0..n1) ⊂ 'I_n1 into [0..n1) ⊂ 'I_(n1 + n2).
- last_ord n1 is the n1-shift from 'I_n2 to 'I_(n1 + n2).
It maps [0..n2) ⊂ 'I_n2 into [n1..n1 + n2) ⊂ 'I_(n1 + n2).
- concat_l_ord H is the canonical projection from 'I_(n1 + n2) onto
'I_n1, provided a proof that the (implicit) argument is smaller than n1.
It maps [0..n1) ⊂ 'I_(n1 + n2) onto [0..n1) ⊂ 'I_n1.
- concat_r_ord H is the n1-downshift from 'I_(n1 + n2) to 'I_n2,
provided a proof that the (implicit) argument is not smaller than n1.
It maps [n1..n1 + n2) ⊂ 'I_(n1 + n2) into [0..n2) ⊂ 'I_n2.
- skip_ord i0 injects 'I_n to 'I_n.+1 by skipping i0.
It maps [0..n) ⊂ 'I_n into [0..i0^..n.+1) ⊂ 'I_n.+1.
- insert_ord i0 projects 'I_n.+1 onto 'I_n by skipping i0, provided
a proof that the (implicit) argument is distinct from i0.
It maps [0..i0^..n.+1) ⊂ 'I_n.+1 onto [0..n) ⊂ 'I_n.
- skip_f_ord H i0 transforms any function of type 'I_[n.+1] into a
function of type 'I_[n] by skipping the input value i0, provided a proof
H that the (implicit) function argument is injective.
- insert_f_ord p i0 transforms any function p : 'I_[n] into a function of
type 'I_[n.+1] by inserting the input value i0 associated with itself.
- extend_f_S transforms any function of type 'I_{n1,n2} into a function of
type 'I_{n1.+1,n2.+1} by mapping the (last) input ordinal, of value n1, to
the (last) output ordinal, of value n2.
- skip2_ord H injects 'I_n to 'I_n.+2 by skipping i0 and i1,
provided a proof H : i1 ≠ i0.
It maps [0..n) ⊂ 'I_n into [0..i0^..i1^..n.+2) ⊂ 'I_n.+2.
- insert2_ord H H0 H1 projecst 'I_n.+2 to 'I_n by skipping i0 and
i1, provided a proof H : i1 ≠ i0, and proofs H0 and H1 that the
(implicit) argument is distinct from i0 and i1.
It maps [0..i0^..i1^..n.+2) ⊂ 'I_n.+2 into [0..n) ⊂ 'I_n.
- move_ord i0 i1 moves i0 right after i1 (it does nothing when
i1 = i0).
It maps [0..i0..i1..n.+1) ⊂ 'I_n.+1 into
[0..i0^..i1 i0..n.+1) ⊂ 'I_n.+1.
- transp_ord i0 i1 exchanges i0 and i1 (it does nothing when i1 = i0).
It maps [0..i0..i1..n) ⊂ 'I_n into [0..i1..i0..n) ⊂ 'I_n.
- lenPF P is the cardinal of {i ∈ [0..n) | P i} for any predicate P
on 'I_n.
- filterP_ord enumerates the ordinals satisfying the (implicit) predicate
argument P : 'I_n → Prop.
It maps [0..lenPF P) ⊂ 'I_(lenPF P) into
{i ∈ [0..n) | P i} ⊂ 'I_n.
- unfilterP_ord H projects ordinals to their rank in those satisfying the (implicit) predicate argument P : 'I_n → Prop, provided a proof H : P i0 for some (implicit) witness argument i0, with default value ord0 when the predicate is not satisfied. It maps 'I_n onto 'I_(lenPF P).
About the API
Usage
From Requisite Require Import stdlib.
From Coq Require Import EqdepFacts Bool.
From Requisite Require Import ssr_wMC.
From mathcomp Require Import eqtype seq path bigop boolp.
From Numbers Require Import Numbers_wDep.
From Subsets Require Import Subset Function Function_sub.
Notation "''I_' { m , n }" := ('I_m → 'I_n)
(at level 8, m at level 2, n at level 2, format "''I_' { m , n }").
Notation "''I_' [ n ]" := ('I_{n,n})
(at level 8, n at level 2, format "''I_' [ n ]").
Notation "''I_' { m , n , p }" := ('I_m → 'I_{n,p})
(at level 8, m at level 2, n at level 2, format "''I_' { m , n , p }").
Notation iota := seq.iota (only parsing).
Section Bool_compl.
Lemma P_1 : ∀ (P : Prop) b, P → reflect P b → nat_of_bool b = 1.
Proof. intros P b HP Hb; rewrite (introT Hb); easy. Qed.
Lemma nP_0 : ∀ (P : Prop) b, ¬ P → reflect P b → nat_of_bool b = 0.
Proof. intros P b HP Hb; rewrite (introF Hb); easy. Qed.
Lemma neqP : ∀ {T : eqType} {x y : T}, x ≠ y → x != y.
Proof. intros; apply /eqP; easy. Qed.
Lemma in_asboolP :
∀ {n} {P : 'I_n → Prop} {i}, P i → i \in (fun i ⇒ asbool (P i)).
Proof. move=>> /asboolP H; easy. Qed.
End Bool_compl.
Section Seq_compl1.
Context {T : Type}.
Context {x0 x : T}.
Context {l : seq T}.
Context {i : nat}.
Lemma nth_cons_l : i = 0 → nth x0 (x :: l) i = x.
Proof. intros; subst; apply nth0. Qed.
Lemma nth_cons_r : i ≠ 0 → nth x0 (x :: l) i = nth x0 l (i - 1).
Proof.
intros Hi; rewrite (nth_ncons _ 1); case_eq (i < 1); try easy.
move⇒ /ltP Hi1; contradict Hi; apply lt_1; easy.
Qed.
Lemma nth_rcons_l : i ≠ size l → nth x0 (rcons l x) i = nth x0 l i.
Proof.
intros Hi; rewrite nth_rcons; case_eq (i < size l); intros Hi1; try easy.
case_eq (i == size l); intros Hi2; try now contradict Hi; apply /eqP.
symmetry; apply nth_default; rewrite leqNgt Hi1; easy.
Qed.
Lemma nth_rcons_r : i = size l → nth x0 (rcons l x) i = x.
Proof.
intros Hi; subst; rewrite nth_rcons; case_eq (size l < size l); intros Hl1.
exfalso; rewrite ltnn in Hl1; easy.
case_eq (size l == size l); intros Hl2; try easy.
exfalso; rewrite eq_refl in Hl2; easy.
Qed.
End Seq_compl1.
Section Seq_compl2.
Context {T : eqType}.
Context {x0 x : T}.
Context {l : seq T}.
Context {i : nat}.
Lemma nth_cons_l_rev :
x \notin l → i ≤ size l → nth x0 (x :: l) i = x → i = 0.
Proof.
intros Hx Hi H; destruct l.
apply /eqP; rewrite leqn0 // in Hi.
destruct (le_dec i 0) as [Hi0 | Hi0]; auto with arith.
apply Nat.nle_gt in Hi0; move: Hi0 ⇒ /ltP Hi0.
contradict Hx; apply /negP /negPn.
rewrite -H (nth_ncons _ 1); case_eq (i < 1); intros Hi1.
contradict Hi0; apply /negP; rewrite -ltnNge //.
clear x H; apply mem_nth; rewrite ltn_psubLR //.
Qed.
Lemma nth_cons_l_rev_uniq :
uniq (x :: l) → i ≤ size l → nth x0 (x :: l) i = x → i = 0.
Proof. move=>> /andP [Hx _]; apply nth_cons_l_rev; easy. Qed.
Lemma nth_rcons_r_rev :
x \notin l → i ≤ size l → nth x0 (rcons l x) i = x → i = size l.
Proof.
intros Hx Hi H; destruct (lastP l) as [| s y].
apply /eqP; rewrite leqn0 // in Hi.
destruct (le_dec (size (rcons s y)) i) as [Hi1 | Hi1].
apply Nat.le_antisymm; try easy; apply /leP; easy.
apply Nat.nle_gt in Hi1; move: Hi1 ⇒ /ltP Hi1.
contradict Hx; apply /negP /negPn.
rewrite -H nth_rcons; case_eq (i < size (rcons s y)); intros Hi2.
clear x H; apply mem_nth; easy.
contradict Hi1; apply /negP; apply negbT; easy.
Qed.
Lemma nth_rcons_r_rev_uniq :
uniq (rcons l x) → i ≤ size l → nth x0 (rcons l x) i = x → i = size l.
Proof.
move=>>; rewrite rcons_uniq.
move⇒ /andP [Hx _]; apply nth_rcons_r_rev; easy.
Qed.
End Seq_compl2.
Section Seq_compl3.
Context {T : eqType}.
Lemma injS_seq_equiv :
∀ {P : pred T} {sT : subType P} {f : T → sT},
injS P f ↔ ∀ s, all P s → { in s &, injective f }.
Proof.
move=>>; split.
intros H s Hs x y Hx Hy; apply H; [move: Hx | move: Hy]; apply /allP; easy.
intros H x y Hx Hy; apply (H [:: x; y]).
simpl; rewrite Hx Hy; easy.
rewrite !in_cons eq_refl; apply orTb.
rewrite !in_cons eq_refl; apply orbT.
Qed.
End Seq_compl3.
Section Ord_compl1.
Lemma I_0_is_empty : ¬ inhabited 'I_0.
Proof. intros [[n Hn]]; easy. Qed.
Definition I_1_is_unit := ord1.
Lemma I_S_is_nonempty : ∀ {n}, inhabited 'I_n.+1.
Proof. intros; apply (inhabits ord0). Qed.
Lemma fun_from_I_S_to_I_0_is_empty : ∀ n, ¬ inhabited ('I_{n.+1,0}).
Proof.
intros; apply fun_to_empty_is_empty. apply I_S_is_nonempty. apply I_0_is_empty.
Qed.
Definition fun_from_I_0 (E : Type) : 'I_0 → E := fun_from_empty I_0_is_empty.
Lemma fun_from_I_0_inj : ∀ {E : Type}, injective (fun_from_I_0 E).
Proof. intros; apply fun_from_empty_is_inj, I_0_is_empty. Qed.
Lemma fun_from_I_0_bij : bijective (fun_from_I_0 'I_0).
Proof. apply injF_bij, fun_from_I_0_inj. Qed.
Lemma injF_leq : ∀ {n1 n2} {f : 'I_{n1,n2}}, injective f → n1 ≤ n2.
Proof. exact inj_leq. Qed.
Lemma injF_le :
∀ {n1 n2} {f : 'I_{n1,n2}}, injective f → (n1 ≤ n2)%coq_nat.
Proof. move=>> Hf; apply /leP; move: Hf; apply injF_leq. Qed.
Lemma injF_plus_minus_r :
∀ {n1 n2} {f : 'I_{n1,n2}}, injective f → n1 + (n2 - n1) = n2.
Proof. move=>> /injF_leq /leP; apply nat_plus_minus_r. Qed.
Lemma surjF_leq : ∀ {n1 n2} {f : 'I_{n1,n2}}, surjective f → n2 ≤ n1.
Proof. move=>> /surj_has_right_inv [g /can_inj /injF_leq Hg]; easy. Qed.
Lemma surjF_le :
∀ {n1 n2} {f : 'I_{n1,n2}}, surjective f → (n2 ≤ n1)%coq_nat.
Proof. move=>> Hf; apply /leP; move: Hf; apply surjF_leq. Qed.
Lemma surjF_plus_minus_r :
∀ {n1 n2} {f : 'I_{n1,n2}}, surjective f → n2 + (n1 - n2) = n1.
Proof. move=>> /surjF_leq /leP; apply nat_plus_minus_r. Qed.
Definition ord1 {n} : 'I_n.+2 := lift ord0 ord0.
Definition ord_pred_max {n} : 'I_n.+2 := Ordinal ltnSSn.
Lemma ord0_correct : ∀ {n}, (ord0 : 'I_n.+1) = 0 :> nat.
Proof. easy. Qed.
Lemma ord1_correct : ∀ {n}, (ord1 : 'I_n.+2) = 1 :> nat.
Proof. easy. Qed.
Lemma ord_pred_max_correct : ∀ {n}, (ord_pred_max : 'I_n.+2) = n :> nat.
Proof. easy. Qed.
Lemma ord_max_correct : ∀ {n}, (ord_max : 'I_n.+1) = n :> nat.
Proof. easy. Qed.
Lemma ord0_equiv : ∀ {n} (i : 'I_n.+1), i = ord0 ↔ nat_of_ord i = 0.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.
Lemma ord1_equiv : ∀ {n} (i : 'I_n.+2), i = ord1 ↔ nat_of_ord i = 1.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.
Lemma ord_pred_max_equiv :
∀ {n} (i : 'I_n.+2), i = ord_pred_max ↔ nat_of_ord i = n.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.
Lemma ord_max_equiv :
∀ {n} (i : 'I_n.+1), i = ord_max ↔ nat_of_ord i = n.
Proof. intros; split; intros; [subst | apply ord_inj]; easy. Qed.
Lemma ord2_dec : ∀ i : 'I_2, {i = ord0} + {i = ord_max}.
Proof.
intros [i Hi]; destruct (ltn_2_dec Hi); [left | right]; apply ord_inj; easy.
Qed.
Lemma ord3_dec : ∀ i : 'I_3, {i = ord0} + {i = ord1} + {i = ord_max}.
Proof.
intros [i Hi]; destruct (ltn_3_dec Hi) as [[H | H] | H];
[left; left | left; right | right]; apply ord_inj; easy.
Qed.
Lemma ord_lt_0_max :
∀ {n}, ((ord0 : 'I_n.+2) < (ord_max : 'I_n.+2))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.
Lemma ord2_1_max : (ord1 : 'I_2) = (ord_max : 'I_2).
Proof. apply ord_inj; easy. Qed.
Lemma ord2_0_pred_max : (ord0 : 'I_2) = (ord_pred_max : 'I_2).
Proof. apply ord_inj; easy. Qed.
Lemma ord_lt_0_1 : ∀ {n}, ((ord0 : 'I_n.+2) < (ord1 : 'I_n.+2))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.
Lemma ord_lt_0_pred_max :
∀ {n}, ((ord0 : 'I_n.+3) < (ord_pred_max : 'I_n.+3))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.
Lemma ord_lt_1_max :
∀ {n}, ((ord1 : 'I_n.+3) < (ord_max : 'I_n.+3))%coq_nat.
Proof. intros; apply /ltP; easy. Qed.
Lemma ord3_1_pred_max : (ord1 : 'I_3) = (ord_pred_max : 'I_3).
Proof. apply ord_inj; easy. Qed.
Lemma ord_lt_neq : ∀ {n} {i j : 'I_n}, (i < j)%coq_nat → i ≠ j.
Proof. intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; easy. Qed.
Lemma ord_lt_neq_sym : ∀ {n} {i j : 'I_n}, (i < j)%coq_nat → j ≠ i.
Proof. intros; apply not_eq_sym; apply ord_lt_neq; easy. Qed.
Lemma ord_0_not_max : ∀ {n}, (ord0 : 'I_n.+2) ≠ (ord_max : 'I_n.+2).
Proof. intros; apply ord_lt_neq, ord_lt_0_max. Qed.
Lemma ord_max_not_0 : ∀ {n}, (ord_max : 'I_n.+2) ≠ (ord0 : 'I_n.+2).
Proof. intros; apply not_eq_sym, ord_0_not_max. Qed.
Lemma ord_0_not_1 : ∀ {n}, (ord0 : 'I_n.+2) ≠ (ord1 : 'I_n.+2).
Proof. intros; apply ord_lt_neq, ord_lt_0_1. Qed.
Lemma ord_1_not_0 : ∀ {n}, (ord1 : 'I_n.+2) ≠ (ord0 : 'I_n.+2).
Proof. intros; apply not_eq_sym, ord_0_not_1. Qed.
Lemma ord_0_not_pred_max :
∀ {n}, (ord0 : 'I_n.+3) ≠ (ord_pred_max : 'I_n.+3).
Proof. intros; apply ord_lt_neq, ord_lt_0_pred_max. Qed.
Lemma ord_pred_max_not_0 :
∀ {n}, (ord_pred_max : 'I_n.+3) ≠ (ord0 : 'I_n.+3).
Proof. intros; apply not_eq_sym, ord_0_not_pred_max. Qed.
Lemma ord_1_not_max : ∀ {n}, (ord1 : 'I_n.+3) ≠ (ord_max : 'I_n.+3).
Proof. intros; apply ord_lt_neq, ord_lt_1_max. Qed.
Lemma ord_max_not_1 : ∀ {n}, (ord_max : 'I_n.+3) ≠ (ord1 : 'I_n.+3).
Proof. intros; apply not_eq_sym, ord_1_not_max. Qed.
Lemma ord2_lt :
∀ {i0 i1 : 'I_2}, (i0 < i1)%coq_nat → i0 = ord0 ∧ i1 = ord_max.
Proof.
intros i0 i1; destruct (ord2_dec i0) as [H0 | H0], (ord2_dec i1) as [H1 | H1];
rewrite H0 H1; try easy.
intros H; contradict H; apply Nat.nlt_ge; easy.
Qed.
Lemma ord3_lt :
∀ {i0 i1 i2 : 'I_2},
(i0 < i1)%coq_nat → (i1 < i2)%coq_nat →
i0 = ord0 ∧ i1 = ord1 ∧ i2 = ord_max.
Proof.
intros i0 i1 i2; destruct (ord2_dec i0) as [H0 | H0],
(ord2_dec i1) as [H1 | H1], (ord2_dec i2) as [H2 | H2];
rewrite H0 H1 H2; try easy.
intros _ H; contradict H; apply Nat.nlt_ge; easy.
intros H; contradict H; apply Nat.nlt_ge; easy.
Qed.
Lemma ord_compat : ∀ {n} {i j : 'I_n}, i = j → i = j :> nat.
Proof. intros; subst; easy. Qed.
Lemma ord_neq :
∀ {n} {i j : 'I_n}, nat_of_ord i ≠ nat_of_ord j → i ≠ j.
Proof. move=>>; apply contra_not, f_equal. Qed.
Lemma ord_neq_compat :
∀ {n} {i j : 'I_n}, i ≠ j → nat_of_ord i ≠ nat_of_ord j.
Proof. move=>>; apply contra_not, ord_inj. Qed.
Lemma ord_eq_dec : ∀ {n} (i j : 'I_n), {i = j} + {i ≠ j}.
Proof.
intros n [i Hi] [j Hj]; destruct (Nat.eq_dec i j) as [H | H];
[left; apply ord_inj | right; apply ord_neq]; easy.
Qed.
Lemma ord_eq2_dec :
∀ {n} (k i j : 'I_n), {k = i} + {k = j} + {k ≠ i ∧ k ≠ j}.
Proof.
intros n k i j.
destruct (ord_eq_dec k i) as [Hi | Hi]; [left; left; easy |].
destruct (ord_eq_dec k j) as [Hj | Hj]; [left; right | right]; easy.
Qed.
Lemma ord_neq_ex : ∀ {n} (i0 : 'I_n.+2), ∃ i1, i1 ≠ i0.
Proof.
intros n i0; destruct (ord_eq_dec i0 ord0) as [-> | Hi0].
∃ ord_max; apply ord_max_not_0.
∃ ord0; apply not_eq_sym; easy.
Qed.
Lemma ord0_leq_equiv : ∀ m {n} {i : 'I_n.+1}, i = ord0 ↔ i ≤ @ord0 m.
Proof.
intros; rewrite ord0_equiv; destruct i as [i Hi]; simpl.
split; [intros; subst | move⇒ /leP]; auto with arith.
Qed.
Lemma ord0_le_equiv :
∀ m {n} {i : 'I_n.+1}, i = ord0 ↔ (i ≤ @ord0 m)%coq_nat.
Proof.
intros m n i; rewrite (ord0_leq_equiv m); split; move⇒ /leP; easy.
Qed.
Lemma ord_n0_gtn_equiv : ∀ m {n} {i : 'I_n.+1}, i ≠ ord0 ↔ @ord0 m < i.
Proof. intros; rewrite -iff_not_r_equiv ord0_leq_equiv nltn_geq; easy. Qed.
Lemma ord_n0_gt_equiv :
∀ m {n} {i : 'I_n.+1}, i ≠ ord0 ↔ (@ord0 m < i)%coq_nat.
Proof.
intros m n i; rewrite (ord_n0_gtn_equiv m); split; move⇒ /ltP; easy.
Qed.
Lemma ord_n0_nlt_equiv :
∀ {n} {i : 'I_n.+1}, i ≠ ord0 ↔ ¬ (i < 1)%coq_nat.
Proof.
intros; split.
intros H; contradict H; apply ord_inj; simpl; auto with zarith.
rewrite -contra_equiv; intros; subst; apply Nat.lt_0_1.
Qed.
Lemma ord0_lt_equiv : ∀ {n} {i : 'I_n.+1}, i = ord0 ↔ (i < 1)%coq_nat.
Proof. move=>>; rewrite iff_not_equiv; apply ord_n0_nlt_equiv. Qed.
Lemma ord_n0_gt : ∀ {n} {i j : 'I_n.+1}, (i < j)%coq_nat → j ≠ ord0.
Proof.
intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; apply /leP; easy.
Qed.
Lemma ord_max_geq_equiv :
∀ {n} {i : 'I_n.+1}, i = ord_max ↔ @ord_max n ≤ i.
Proof.
intros; rewrite ord_max_equiv; destruct i as [i Hi]; simpl; split;
[intros; subst | move⇒ /leP; move: Hi ⇒ /leP]; auto with zarith.
Qed.
Lemma ord_max_ge_equiv :
∀ {n} {i : 'I_n.+1}, i = ord_max ↔ (@ord_max n ≤ i)%coq_nat.
Proof. intros; rewrite ord_max_geq_equiv; split; move⇒ /leP; easy. Qed.
Lemma ord_nmax_ltn_equiv :
∀ {n} {i : 'I_n.+1}, i ≠ ord_max ↔ i < @ord_max n.
Proof. intros; rewrite -iff_not_r_equiv ord_max_geq_equiv nltn_geq; easy. Qed.
Lemma ord_nmax_lt_equiv :
∀ {n} {i : 'I_n.+1}, i ≠ ord_max ↔ (i < @ord_max n)%coq_nat.
Proof. intros; rewrite ord_nmax_ltn_equiv; split; move⇒ /ltP; easy. Qed.
Lemma ord_nmax_lt :
∀ {n} {i j : 'I_n.+1}, (i < j)%coq_nat → i ≠ ord_max.
Proof.
intros n i [j Hj] H; apply ord_lt_neq; simpl in ×.
apply nat_lt_lt_S with j; try easy; apply /ltP; easy.
Qed.
Lemma ord_lt_S : ∀ {n} (i : 'I_n), i.+1 < n.+1.
Proof.
intros n [i Hi]; apply /ltP; rewrite -Nat.succ_lt_mono; apply /ltP; easy.
Qed.
Lemma ordS_lt_minus_1 :
∀ {n} (i : 'I_n.+1), nat_of_ord i ≠ O → i - 1 < n.
Proof.
intros n [i Hi1] Hi2; simpl in *; rewrite ltn_subLR; try easy.
apply /ltP; apply Nat.neq_0_lt_0; easy.
Qed.
Lemma ord_split_gen :
∀ {n p} (i : 'I_p), (p ≤ n.+1)%coq_nat → n = i + (n - i).
Proof.
intros n p i Hp; rewrite addn_subn; try easy.
apply Nat.lt_le_trans with p; try apply /ltP; easy.
Qed.
Lemma ordS_split_gen :
∀ {n p} (i : 'I_p), (p ≤ n)%coq_nat → n = i.+1 + (n - i.+1).
Proof.
intros n p i Hp; rewrite addn_subn; try easy.
apply → Nat.succ_lt_mono; apply Nat.lt_le_trans with p; try apply /ltP; easy.
Qed.
Lemma ord_splitS_gen :
∀ {n p} (i : 'I_p), (p ≤ n.+1)%coq_nat → n.+1 = i + (n - i).+1.
Proof. move=>> H; rewrite addnS; apply eq_S, ord_split_gen; easy. Qed.
Lemma ordS_splitS_gen :
∀ {n p} (i : 'I_p), (p ≤ n.+1)%coq_nat → n.+1 = i.+1 + (n - i).
Proof. move=>>; rewrite addSnnS; apply ord_splitS_gen. Qed.
Lemma ord_split : ∀ {n} (i : 'I_n.+1), n = i + (n - i).
Proof. intros; apply ord_split_gen; easy. Qed.
Lemma ordS_split : ∀ {n} (i : 'I_n), n = i.+1 + (n - i.+1).
Proof. intros; apply ordS_split_gen; easy. Qed.
Lemma ord_splitS : ∀ {n} (i : 'I_n.+1), n.+1 = i + (n - i).+1.
Proof. intros; apply ord_splitS_gen; easy. Qed.
Lemma ordS_splitS : ∀ {n} (i : 'I_n.+1), n.+1 = i.+1 + (n - i).
Proof. intros; apply ordS_splitS_gen; easy. Qed.
Lemma ord_split_pred : ∀ {n} (i : 'I_n), n = i + (n - i).
Proof. intros; apply ord_split_gen, nat_leS. Qed.
Lemma ord_splitS_pred : ∀ {n} (i : 'I_n), n.+1 = i + (n - i).+1.
Proof. intros; apply ord_splitS_gen, nat_leS. Qed.
Lemma ordS_splitS_pred : ∀ {n} (i : 'I_n), n.+1 = i.+1 + (n - i).
Proof. intros; apply ordS_splitS_gen, nat_leS. Qed.
Lemma bump_l : ∀ i j, (j < i)%coq_nat → bump i j = j.
Proof.
intros i j H; unfold bump.
rewrite (nP_0 (i ≤ j)); try apply idP; try easy.
move /leP; apply /Nat.nle_gt; easy.
Qed.
Lemma bump_r : ∀ i j, (i ≤ j)%coq_nat → bump i j = j.+1.
Proof.
intros i j H; unfold bump; simpl.
rewrite (P_1 (i ≤ j)); try apply idP; try apply /leP; easy.
Qed.
Lemma bump_r_alt : ∀ i j, ¬ (j < i)%coq_nat → bump i j = j.+1.
Proof. intros; apply bump_r, Nat.nlt_ge; easy. Qed.
Lemma bump_inj : ∀ i, injective (bump i).
Proof.
intros i j0 j1;
destruct (lt_dec j0 i) as [Hj0 | Hj0], (lt_dec j1 i) as [Hj1 | Hj1];
try rewrite (bump_l _ _ Hj0); try rewrite (bump_r_alt _ _ Hj0);
try rewrite (bump_l _ _ Hj1); try rewrite (bump_r_alt _ _ Hj1);
auto with zarith.
Qed.
Lemma bump_eq : ∀ h i j, (bump h i == bump h j) = (i == j).
Proof. intros; rewrite (inj_eq (bump_inj h)); easy. Qed.
Lemma bump_neq : ∀ h i j, (bump h i != bump h j) = (i != j).
Proof. intros; rewrite bump_eq; easy. Qed.
Lemma bump_incr : ∀ h i j, (bump h i < bump h j) = (i < j).
Proof.
intros h i j; rewrite 2!ltn_neqAle (inj_eq (bump_inj h)) leq_bump2; easy.
Qed.
Lemma bump_comm :
∀ i0 i1 j0 j1 k,
i0 = bump i1 j0 → i1 = bump i0 j1 →
bump i1 (bump j0 k) = bump i0 (bump j1 k).
Proof.
intros i0 i1 j0 j1 k Hi0 Hi1.
destruct (le_lt_dec j0 k) as [H0 | H0];
[rewrite (bump_r _ _ H0) | rewrite (bump_l _ _ H0)];
(destruct (le_lt_dec j1 k) as [H1 | H1];
[rewrite (bump_r _ _ H1) | rewrite (bump_l _ _ H1)]).
2,4: destruct (le_lt_dec i0 k) as [H2 | H2];
[rewrite (bump_r _ _ H2) | rewrite (bump_l _ _ H2)].
1,6: destruct (le_lt_dec i0 k.+1) as [H3 | H3];
[rewrite (bump_r _ _ H3) | rewrite (bump_l _ _ H3)].
3,4,7,8: destruct (le_lt_dec i1 k) as [H4 | H4];
[rewrite (bump_r _ _ H4) | rewrite (bump_l _ _ H4)].
1,2,11,12: destruct (le_lt_dec i1 k.+1) as [H5 | H5];
[rewrite (bump_r _ _ H5) | rewrite (bump_l _ _ H5)].
all: try easy.
all: exfalso.
all: destruct (le_lt_dec i1 j0) as [H6 | H6];
[rewrite (bump_r _ _ H6) in Hi0 | rewrite (bump_l _ _ H6) in Hi0].
all: destruct (le_lt_dec i0 j1) as [H7 | H7];
[rewrite (bump_r _ _ H7) in Hi1 | rewrite (bump_l _ _ H7) in Hi1].
all: auto with zarith.
Qed.
Lemma lift_l :
∀ {n} {i : 'I_n.+1} {j : 'I_n}, (j < i)%coq_nat → lift i j = j :> nat.
Proof. intros; simpl; apply bump_l; easy. Qed.
Lemma lift_m : ∀ {n} (i : 'I_n.+1) (j : 'I_n), i ≠ lift i j :> nat.
Proof. intros; apply /eqP; apply neq_bump. Qed.
Lemma lift_r :
∀ {n} {i : 'I_n.+1} {j : 'I_n},
(i ≤ j)%coq_nat → lift i j = j.+1 :> nat.
Proof. intros; simpl; apply bump_r; easy. Qed.
Lemma lift_lt_l :
∀ {n} (i : 'I_n.+1) (j : 'I_n),
(lift i j < i)%coq_nat → (j < i)%coq_nat.
Proof.
intros n i j H; destruct (le_lt_dec i j) as [Hj | Hj]; try easy.
rewrite (lift_r Hj) in H; contradict Hj; apply Nat.nle_gt; auto with arith.
Qed.
Lemma lift_lt_r :
∀ {n} (i : 'I_n.+1) (j : 'I_n),
(i < lift i j)%coq_nat → (i ≤ j)%coq_nat.
Proof.
intros n i j H; destruct (le_lt_dec i j) as [Hj | Hj]; try easy.
rewrite (lift_l Hj) in H; contradict Hj; apply Nat.nlt_ge; auto with arith.
Qed.
Lemma lift_m1 :
∀ {n} (i : 'I_n.+1) (j : 'I_n),
nat_of_ord i ≠ O → nat_of_ord j = i.-1 → lift ord0 j = i.
Proof.
intros n i j H1 H2; apply ord_inj; simpl; unfold bump; simpl.
rewrite H2 -Nat.sub_1_r; auto with zarith arith.
Qed.
Lemma widen_ord_inj : ∀ {n p} (H : n ≤ p), injective (widen_ord H).
Proof. move=>> /(f_equal (@nat_of_ord _)) H; apply ord_inj; easy. Qed.
End Ord_compl1.
Section Fun_ord1.
Lemma injF_surj : ∀ {n} (p : 'I_[n]), injective p → surjective p.
Proof. move=>> /injF_bij /bij_surj; easy. Qed.
Lemma surjF_bij : ∀ {n} (p : 'I_[n]), surjective p → bijective p.
Proof.
move=>> /surj_has_right_inv [g Hg1]; move: (canF_sym Hg1) ⇒ Hg2.
apply (Bijective Hg2 Hg1).
Qed.
Lemma surjF_inj : ∀ {n} (p : 'I_[n]), surjective p → injective p.
Proof. move=>> /surjF_bij /bij_inj; easy. Qed.
Lemma injF_surj_equiv : ∀ {n} (p : 'I_[n]), injective p ↔ surjective p.
Proof. intros; split; [apply injF_surj | apply surjF_inj]. Qed.
Lemma bijF_inj_equiv : ∀ {n} (p : 'I_[n]), bijective p ↔ injective p.
Proof. intros; split; [apply bij_inj | apply injF_bij]. Qed.
Lemma bijF_surj_equiv : ∀ {n} (p : 'I_[n]), bijective p ↔ surjective p.
Proof. intros; split; [apply bij_surj | apply surjF_bij]. Qed.
Lemma incl_RgF :
∀ {n} {p : 'I_[n]} (P : 'I_n → Prop), injective p → incl P (Rg p).
Proof. move=>> Hp i _; rewrite -(f_inv_can_r (injF_bij Hp) i); easy. Qed.
End Fun_ord1.
Section Fun_ord2.
Context {T1 T2 : finType}.
Context {P1 : pred T1}.
Context {P2 : pred T2}.
Variable f : T1 → T2.
Definition fun_sub (Hf : funS P1 P2 f) : {x1 | P1 x1} → {x2 | P2 x2} :=
fun y1 ⇒
let x1 := proj1_sig y1 in
let Hx1 := proj2_sig y1 in
let x2 := f x1 in
let Hx2 := Hf (f x1) (Im f P1 x1 Hx1) in
exist _ x2 Hx2.
Lemma bijS_bijF_sub :
∀ (Hf : bijS P1 P2 f), bijective (fun_sub (bijS_funS Hf)).
Proof.
intros Hf1; apply bij_ex_uniq_equiv; destruct (bijS_ex_uniq Hf1) as [_ Hf2].
intros [x2 Hx2]; destruct (Hf2 x2 Hx2) as [x1 [[Hx1a Hx1b] Hx1c]].
∃ (exist _ x1 Hx1a); split; unfold fun_sub; simpl.
apply eq_exist; easy.
move⇒ [y1 Hy1a] /= Hy1b; apply eq_sig_fst in Hy1b.
apply eq_exist, Hx1c; split; easy.
Qed.
Lemma bijS_eq_card :
bijS P1 P2 f → #|[ pred x1 | P1 x1 ]| = #|[ pred x2 | P2 x2 ]|.
Proof.
move=>> Hf; rewrite -2!card_sig; apply (bij_eq_card (bijS_bijF_sub Hf)).
Qed.
End Fun_ord2.
Section Ord_compl2.
Context {T : Type}.
Variable x0 : T.
Lemma size_ord_enum : ∀ {n}, size (ord_enum n) = n.
Proof. intros; rewrite -(size_map val) val_ord_enum; apply size_iota. Qed.
Lemma nth_ord_enum_alt :
∀ {n} i0 {j} (Hj : j < n), nth i0 (ord_enum n) j = Ordinal Hj.
Proof.
intros n i0 j Hj; apply val_inj; rewrite -(nth_map _ (val i0));
[rewrite val_ord_enum nth_iota | rewrite size_ord_enum]; easy.
Qed.
Lemma nth_ord_enum : ∀ {n} i0 {i : 'I_n}, nth i0 (ord_enum n) i = i.
Proof. intros n i0 [j Hj]; apply nth_ord_enum_alt. Qed.
Lemma map_nth_ord_enum :
∀ (l : seq T),
map (fun i : 'I_(size l) ⇒ nth x0 l i) (ord_enum (size l)) = l.
Proof.
intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
rewrite take_size -val_ord_enum -map_comp; easy.
Qed.
Lemma map_nth_invF :
∀ {n l1 l2}, size l1 = n.+1 → size l2 = n.+1 →
∀ {p : 'I_[n.+1]} (Hp : injective p),
let q := f_inv (injF_bij Hp) in
l2 = map ((nth x0 l1) \o p) (ord_enum n.+1) →
l1 = map ((nth x0 l2) \o q) (ord_enum n.+1).
Proof.
intros n l1 l2 Hl1 Hl2 p Hp q H.
apply (@eq_from_nth _ x0); [rewrite size_map size_ord_enum; easy |].
intros i Hi; rewrite Hl1 in Hi; pose (ii := Ordinal Hi).
assert (Hii : val ii < size (ord_enum n.+1)) by now rewrite size_ord_enum.
assert (Hq : ∀ j : 'I_n.+1, q j < size (ord_enum n.+1))
by now rewrite size_ord_enum.
rewrite H; unfold comp; replace i with (val ii) by easy.
rewrite !(nth_map ord0)// !nth_ord_enum f_inv_can_r; easy.
Qed.
Definition in_ordS {n} (j : nat) : 'I_n.+1 :=
match (lt_dec j n.+1) with
| left Hj ⇒ Ordinal (lt_ltn Hj)
| right _ ⇒ ord0
end.
Lemma in_ordS_correct_l : ∀ {n} (i : 'I_n.+1), in_ordS i = i.
Proof.
intros n [j Hj]; simpl; unfold in_ordS; destruct (lt_dec _ _) as [Hj' | Hj'].
apply ord_inj; easy.
contradict Hj'; apply /ltP; easy.
Qed.
Lemma in_ordS_correct_l_alt :
∀ {n} j (Hj : j < n.+1), in_ordS j = Ordinal Hj.
Proof. intros; apply (in_ordS_correct_l (Ordinal _)). Qed.
Lemma in_ordS_correct_r :
∀ {n} j, ¬ j < n.+1 → in_ordS j = (@ord0 n).
Proof.
intros n j Hj; unfold in_ordS; destruct (lt_dec _ _) as [Hj' | Hj']; [| easy].
contradict Hj; apply /ltP; easy.
Qed.
Lemma val_in_ordS : ∀ {n} j, j < n.+1 → val (@in_ordS n j) = j.
Proof. intros; rewrite in_ordS_correct_l_alt; easy. Qed.
Lemma in_ordS_injS : ∀ {n}, injS (fun j ⇒ j < n.+1) (@in_ordS n).
Proof.
move=>> Hj1 Hj2; rewrite !in_ordS_correct_l_alt.
move⇒ /(f_equal (@nat_of_ord _)); easy.
Qed.
Lemma ord_enumS_eq : ∀ {n}, ord_enum n.+1 = map in_ordS (iota 0 n.+1).
Proof.
intros n; apply (@eq_from_nth _ ord0).
rewrite size_ord_enum size_map size_iota; easy.
intros j Hj; rewrite (nth_map 0);
[| rewrite size_ord_enum in Hj; rewrite size_iota; easy].
rewrite size_ord_enum in Hj; apply sym_eq.
rewrite (nth_iota _ _ Hj) -add0n_sym nth_ord_enum_alt.
apply in_ordS_correct_l_alt.
Qed.
End Ord_compl2.
Section Ord_compl3a.
Context {T : Type}.
Variable leT : rel T.
Variable x0 : T.
Lemma perm_ord_enum_sort :
∀ l,
{ il | perm_eq il (ord_enum (size l)) ∧ uniq il &
sort leT l = map (fun i : 'I_(size l) ⇒ nth x0 l i) il }.
Proof.
intros l; pose (n := size l); fold n.
assert (Hl : size l = n) by easy; destruct n as [| n].
∃ ([::]); [| apply size0nil; rewrite size_sort]; easy.
destruct (perm_iota_sort leT x0 l) as [jl Hjl2 Hjl1]; rewrite Hl in Hjl2.
pose (il := map in_ordS jl : seq 'I_n.+1); ∃ il; [split |].
rewrite ord_enumS_eq; apply perm_map; easy.
rewrite map_inj_in_uniq; [rewrite (perm_uniq Hjl2); apply iota_uniq |].
apply injS_seq_equiv; [apply in_ordS_injS |].
rewrite (perm_all _ Hjl2); apply /allPP; [intros; apply /ltP |].
intros j Hj; rewrite mem_iota in Hj; apply /ltP; easy.
rewrite Hjl1; replace jl with (map val il); [rewrite -map_comp; easy |].
apply (@eq_from_nth _ 0); [rewrite !size_map; easy |].
intros j Hj; rewrite !size_map in Hj.
rewrite -map_comp (nth_map 0)// comp_correct val_in_ordS//.
apply (@proj2 (0 ≤ nth 0 jl j)); apply /andP.
rewrite -mem_iota -(perm_mem Hjl2 (nth 0 jl j)); apply mem_nth; easy.
Qed.
End Ord_compl3a.
Section Ord_compl3b.
Context {T : eqType}.
Context {leT : rel T}.
Lemma sorted_ordP :
∀ {l : seq T} x0 x1,
reflect (∀ (i : 'I_(size l)) (Hi1 : i.+1 < size l),
leT (nth x0 l i) (nth x1 l (Ordinal Hi1)))
(sorted leT l).
Proof.
intros l x0 x1; apply (iffP (sortedP x0)); intros H.
intros [i Hi] Hi1; simpl; rewrite (set_nth_default x0 x1)//; apply H; easy.
intros i Hi1; rewrite (set_nth_default x1 x0 Hi1).
assert (Hi : i < size l) by now apply ltn_trans with i.+1.
apply (H (Ordinal Hi) Hi1).
Qed.
Hypothesis HT0 : antisymmetric leT.
Hypothesis HT1 : transitive leT.
Hypothesis HT2 : total leT.
Variable x0 : T.
Lemma perm_EX :
∀ {l1 l2}, perm_eq l1 l2 →
{ p : 'I_[size l2] | injective p &
l1 = map ((nth x0 l2) \o p) (ord_enum (size l2)) }.
Proof.
intros l1 l2 Hla.
assert (Hlb : size l1 = size l2) by now apply perm_size.
pose (n := size l2); assert (Hn : size l2 = n) by easy.
fold n in Hlb; fold n; destruct n as [| n].
∃ (fun_from_I_0 'I_0); [apply fun_from_I_0_inj |].
rewrite (size0nil Hlb) (size0nil size_ord_enum); easy.
pose (In := ord_enum n.+1); fold In.
move: (perm_sortP HT2 HT1 HT0 _ _ Hla) ⇒ Hlc.
pose (s := sort leT l2); assert (Hsa : sort leT l1 = s) by easy.
assert (Hsb : size s = n.+1) by now rewrite size_sort.
destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In in Hil1a; rewrite Hsa in Hil1c.
assert (Hil1d : size il1 = n.+1) by now rewrite (perm_size Hil1a) size_ord_enum.
pose (p1 := fun i : 'I_n.+1 ⇒ nth ord0 il1 i).
assert (Hp1 : injective p1)
by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil1d.
pose (q1 := f_inv (injF_bij Hp1) : 'I_[n.+1]).
assert (Hil1e : il1 = map p1 In).
unfold p1, In; move: (map_nth_ord_enum ord0 il1) ⇒ H.
rewrite -{1}H Hil1d; easy.
rewrite Hil1e -map_comp in Hil1c.
assert (Hs1 : l1 = map ((nth x0 s) \o q1) In) by now apply map_nth_invF.
destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
rewrite Hn in il2, Hil2a, Hil2b, Hil2c; fold In in Hil2a; fold s in Hil2c.
assert (Hil2d : size il2 = n.+1) by now rewrite (perm_size Hil2a) size_ord_enum.
pose (p2 := fun i : 'I_n.+1 ⇒ nth ord0 il2 i).
assert (Hp2 : injective p2)
by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil2d.
pose (q2 := f_inv (injF_bij Hp2) : 'I_[n.+1]).
assert (Hil2e : il2 = map p2 In).
unfold p2, In; move: (map_nth_ord_enum ord0 il2) ⇒ H.
rewrite -{1}H Hil2d; easy.
rewrite Hil2e -map_comp in Hil2c.
assert (Hs2 : l2 = map ((nth x0 s) \o q2) In) by now apply map_nth_invF.
∃ (p2 \o q1); [apply inj_comp_compat; [apply f_inv_inj | easy] |].
rewrite Hs1 Hs2; unfold comp.
apply (@eq_from_nth _ x0); [rewrite !size_map; easy |].
intros i Hi; rewrite size_map size_ord_enum in Hi; pose (ii := Ordinal Hi).
assert (Hii : val ii < size In) by now rewrite size_ord_enum.
replace i with (val ii) by easy.
rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
rewrite !nth_ord_enum; unfold q2; rewrite f_inv_can_l; easy.
Qed.
Lemma sort_perm_EX :
∀ l, { p : 'I_[size l] | injective p &
sort leT l = map (fun i ⇒ nth x0 l (p i)) (ord_enum (size l)) }.
Proof. intros l; apply (perm_EX (permEl (perm_sort leT l))). Qed.
End Ord_compl3b.
Section Ord_compl4a0.
Context {T : Type}.
Variable leT : T → T → Prop.
Definition sortedF {n} (A : 'I_n → T) :=
∀ (i j : 'I_n), (i < j)%coq_nat → leT (A i) (A j).
Definition sortedF_S {n} (A : 'I_n → T) :=
∀ (i : 'I_n) (Hi1 : i.+1 < n), leT (A i) (A (Ordinal Hi1)).
Lemma sortedF_nil : ∀ (A : 'I_0 → T), sortedF A.
Proof. intros A i; destruct i; easy. Qed.
Lemma sortedF_one : ∀ (A : 'I_1 → T), sortedF A.
Proof. move=>> H; contradict H; rewrite !I_1_is_unit; apply Nat.lt_irrefl. Qed.
Lemma sortedF_inj :
∀ {n} {A : 'I_n → T}, (∀ x, ¬ leT x x) → sortedF A → injective A.
Proof.
intros n A HT HA i j H1.
assert (HT' : ∀ x y, leT x y → x ≠ y)
by now move=>>; rewrite contra_not_r_equiv; intro; subst.
destruct (lt_eq_lt_dec i j) as [[H2 | H2] | H2]; [..| apply sym_eq in H1].
1,3: contradict H1; apply HT', HA; easy.
apply ord_inj; easy.
Qed.
Lemma sortedF_sortedF_S :
∀ {n} {A : 'I_n → T}, sortedF A → sortedF_S A.
Proof. move=>> HA i Hi1; apply HA; apply /ltP; apply ltnSn. Qed.
Lemma sortedF_S_sortedF_aux :
∀ {n} {A : 'I_n → T},
(∀ x y z, leT x y → leT y z → leT x z) →
(∀ p (i : 'I_n) (H : i + p + 1 < n), leT (A i) (A (Ordinal H))) →
sortedF A.
Proof.
intros n A HT HA i j H1.
assert (H2 : i ≤ j) by now apply /leP; apply Nat.lt_le_incl.
assert (H3 : i + (j - i - 1) + 1 = j).
rewrite addnBA; [| rewrite subn_gt0; apply /ltP; easy].
rewrite subnK; rewrite subnKC//.
apply leq_ltn_trans with i; [| apply /ltP]; easy.
assert (Hj : (i + (j - i - 1) + 1 < n)) by now rewrite H3.
replace j with (Ordinal Hj); [apply HA | apply ord_inj; easy].
Qed.
Lemma sortedF_S_sortedF :
∀ {n} {A : 'I_n → T},
(∀ x y z, leT x y → leT y z → leT x z) →
sortedF_S A → sortedF A.
Proof.
intros n A HT HA; apply (sortedF_S_sortedF_aux HT).
apply (nat_ind_strong (fun p ⇒ ∀ i H, leT (A i) (A (Ordinal H)))).
intros p; destruct p as [|p]; intros Hp i H1.
assert (H2 : i.+1 = i + 0 + 1) by now rewrite -addn0_sym addn1.
assert (H3 : i.+1 < n) by now rewrite H2.
replace (Ordinal _) with (Ordinal H3); [apply HA | apply ord_inj; easy].
assert (H2 : i + p + 1 < n)
by now apply ltn_trans with (i + p.+1 + 1); [rewrite ltn_add2r ltn_add2l |].
apply HT with (A (Ordinal H2)).
apply Hp; apply /ltP; easy.
assert (H3 : (i + p + 1).+1 = i + p.+1 + 1) by now rewrite -addnA !addn1.
assert (H4 : (i + p + 1).+1 < n) by now rewrite H3.
replace (Ordinal H1) with (Ordinal H4); [apply HA | apply ord_inj; easy].
Qed.
Lemma sortedF_equiv :
∀ {n} {A : 'I_n → T},
(∀ x y z, leT x y → leT y z → leT x z) →
sortedF A ↔ sortedF_S A.
Proof.
move=>> HT; split; [apply sortedF_sortedF_S | apply (sortedF_S_sortedF HT)].
Qed.
End Ord_compl4a0.
Section Ord_compl4a1.
Context {T : Type}.
Variable ltT leT : T → T → Prop.
Lemma sortedF_monot :
∀ {n} {A : 'I_n → T},
(∀ x y, ltT x y → leT x y) →
sortedF ltT A → sortedF leT A.
Proof. move=>> HlT HA i j H; apply HlT, HA; easy. Qed.
End Ord_compl4a1.
Section Ord_compl4b.
Definition ord_le {n} : 'I_n → 'I_n → Prop := fun i j ⇒ (i ≤ j)%coq_nat.
Definition ord_lt {n} : 'I_n → 'I_n → Prop := fun i j ⇒ (i < j)%coq_nat.
Lemma ord_le_refl : ∀ {n} (i : 'I_n), ord_le i i.
Proof. intros; apply Nat.le_refl. Qed.
Lemma ord_le_antisym :
∀ {n} (i j : 'I_n), ord_le i j → ord_le j i → i = j.
Proof. intros; apply ord_inj, Nat.le_antisymm; easy. Qed.
Lemma ord_le_trans :
∀ {n} (i j k : 'I_n), ord_le i j → ord_le j k → ord_le i k.
Proof. move=>>; apply Nat.le_trans. Qed.
Lemma ord_le_total : ∀ {n} (i j : 'I_n), ord_le i j ∨ ord_le j i.
Proof. intros; apply nat_le_total. Qed.
Lemma ord_lt_irrefl : ∀ {n} (i : 'I_n), ¬ ord_lt i i.
Proof. intros; apply Nat.lt_irrefl. Qed.
Lemma ord_lt_asym :
∀ {n} (i j : 'I_n), ord_lt i j → ¬ ord_lt j i.
Proof. move=>>; apply Nat.lt_asymm. Qed.
Lemma ord_lt_trans :
∀ {n} (i j k : 'I_n), ord_lt i j → ord_lt j k → ord_lt i k.
Proof. move=>>; apply Nat.lt_trans. Qed.
Lemma ord_lt_total_strict :
∀ {n} (i j : 'I_n), i ≠ j → ord_lt i j ∨ ord_lt j i.
Proof. intros; apply nat_lt_total_strict, ord_neq_compat; easy. Qed.
Definition ord_leq {n} : rel 'I_n := fun i j ⇒ i ≤ j.
Definition ord_ltn {n} : rel 'I_n := fun i j ⇒ i < j.
Lemma ord_leq_refl : ∀ {n}, reflexive (@ord_leq n).
Proof. move=>>; apply leqnn. Qed.
Lemma ord_leq_antisym : ∀ {n}, antisymmetric (@ord_leq n).
Proof. move=>> H; apply ord_inj, anti_leq; easy. Qed.
Lemma ord_leq_trans : ∀ {n}, transitive (@ord_leq n).
Proof. move=>>; apply leq_trans. Qed.
Lemma ord_leq_total : ∀ {n} (i j : 'I_n), ord_leq i j || ord_leq j i.
Proof. intros; apply leq_total. Qed.
Lemma ord_ltn_irrefl : ∀ {n}, irreflexive (@ord_ltn n).
Proof. move=>>; apply ltnn. Qed.
Lemma ord_ltn_asym :
∀ {n} (i j : 'I_n), ord_ltn i j && ord_ltn j i = false.
Proof. move=>>; apply ltn_asym. Qed.
Lemma ord_ltn_trans : ∀ {n}, transitive (@ord_ltn n).
Proof. move=>>; apply ltn_trans. Qed.
Lemma ord_ltn_total_strict :
∀ {n} (i j : 'I_n), i != j = ord_ltn i j || ord_ltn j i.
Proof. move=>>; apply neq_ltn. Qed.
Lemma sorted_enum_ord : ∀ {n}, sorted ord_ltn (enum 'I_n).
Proof.
intros [| n]; [rewrite (size0nil (size_enum_ord _)); easy |].
apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
Qed.
Lemma sorted_filter_enum_ord :
∀ {n} (P : 'I_n → Prop),
sorted ord_ltn (filter (fun i ⇒ asbool (P i)) (enum 'I_n)).
Proof.
intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
Qed.
End Ord_compl4b.
Section Ord_compl4c.
Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF ord_lt f.
Definition incrF_S {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF_S ord_lt f.
Definition nondecrF {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF ord_le f.
Lemma incrF_nil : ∀ {n} (f : 'I_{0,n}), incrF f.
Proof. intros; apply sortedF_nil. Qed.
Lemma incrF_one : ∀ {n} (f : 'I_{1,n}), incrF f.
Proof. intros; apply sortedF_one. Qed.
Lemma incrF_inj :
∀ {n1 n2} {f : 'I_{n1,n2}}, incrF f → injective f.
Proof. move=>>; apply sortedF_inj, ord_lt_irrefl. Qed.
Lemma incrF_equiv : ∀ {n1 n2} (f : 'I_{n1,n2}), incrF f ↔ incrF_S f.
Proof. intros; apply sortedF_equiv, ord_lt_trans. Qed.
Lemma incrF_comp :
∀ {n1 n2 n3} {f : 'I_{n1,n2}} {g : 'I_{n2,n3}},
incrF f → incrF g → incrF (g \o f).
Proof. move=>> Hf Hg i1 j1 H1; apply Hg, Hf; easy. Qed.
Lemma incrF_0 :
∀ {n1 n2} (f : 'I_{n1.+1,n2.+1}) (i2 : 'I_n2.+1),
incrF f → Rg f i2 → (f ord0 ≤ i2)%coq_nat.
Proof.
intros n1 n2 f i2 Hf [i1 _];
destruct (ord_eq_dec i1 ord0) as [-> | Hi1]; [easy |].
apply Nat.lt_le_incl, Hf, ord_n0_gt_equiv; easy.
Qed.
Lemma incrF_max :
∀ {n1 n2} (f : 'I_{n1.+1,n2.+1}) (i2 : 'I_n2.+1),
incrF f → Rg f i2 → (i2 ≤ f ord_max)%coq_nat.
Proof.
intros n1 n2 f i2 Hf [i1 _];
destruct (ord_eq_dec i1 ord_max) as [-> | Hi1]; [easy |].
apply Nat.lt_le_incl, Hf, ord_nmax_lt_equiv; easy.
Qed.
Lemma incrF_nondecrF :
∀ {n1 n2} {f : 'I_{n1,n2}}, incrF f → nondecrF f.
Proof. move=>>; apply sortedF_monot; move=>>; apply Nat.lt_le_incl. Qed.
End Ord_compl4c.
Section Cast_ord.
Lemma cast_ord_0_equiv :
∀ {n m} (H : n = m.+1) (i : 'I_n),
cast_ord H i = ord0 ↔ nat_of_ord i = 0.
Proof.
intros; split; intros Hi.
apply (f_equal (@nat_of_ord _)) in Hi; easy.
apply ord_inj; easy.
Qed.
Lemma cast_ord_n0_equiv :
∀ {n m} (H : n = m.+1) (i : 'I_n),
cast_ord H i ≠ ord0 ↔ nat_of_ord i ≠ 0.
Proof. intros; rewrite -iff_not_equiv; apply cast_ord_0_equiv. Qed.
Lemma cast_ord_max_equiv :
∀ {n m} (H : n = m.+1) (i : 'I_n),
cast_ord H i = ord_max ↔ nat_of_ord i = m.
Proof.
intros; split; intros Hi.
apply (f_equal (@nat_of_ord _)) in Hi; easy.
apply ord_inj; easy.
Qed.
Lemma cast_ord_nmax_equiv :
∀ {n m} (H : n = m.+1) (i : 'I_n),
cast_ord H i ≠ ord_max ↔ nat_of_ord i ≠ m.
Proof. intros; rewrite -iff_not_equiv; apply cast_ord_max_equiv. Qed.
Lemma cast_ordS_0 :
∀ {n m} (H : n.+1 = m.+1) i,
i = ord0 → cast_ord H i = ord0.
Proof. intros; subst; apply ord_inj; easy. Qed.
Lemma cast_ordS_0_rev :
∀ {n m} (H : n.+1 = m.+1) i,
cast_ord H i = ord0 → i = ord0.
Proof.
move⇒ n m H i /(f_equal (cast_ord (sym_eq H))); rewrite cast_ordK;
intros; subst; apply ord_inj; easy.
Qed.
Lemma cast_ordS_0_equiv :
∀ {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
cast_ord H i = ord0 ↔ i = ord0.
Proof. intros; split; [apply cast_ordS_0_rev | apply cast_ordS_0]. Qed.
Lemma cast_ordS_n0 :
∀ {n m} (H : n.+1 = m.+1) i,
i ≠ ord0 → cast_ord H i ≠ ord0.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_0_rev. Qed.
Lemma cast_ordS_n0_rev :
∀ {n m} (H : n.+1 = m.+1) i,
cast_ord H i ≠ ord0 → i ≠ ord0.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_0. Qed.
Lemma cast_ordS_n0_equiv :
∀ {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
cast_ord H i ≠ ord0 ↔ i ≠ ord0.
Proof. intros; split; [apply cast_ordS_n0_rev | apply cast_ordS_n0]. Qed.
Lemma cast_ordS_max :
∀ {n m} (H : n.+1 = m.+1) i,
i = ord_max → cast_ord H i = ord_max.
Proof.
intros n m H i Hi; subst; apply ord_inj; simpl; apply Nat.succ_inj in H; easy.
Qed.
Lemma cast_ordS_max_rev :
∀ {n m} (H : n.+1 = m.+1) i,
cast_ord H i = ord_max → i = ord_max.
Proof.
move⇒ n m H i /(f_equal (cast_ord (sym_eq H))); rewrite cast_ordK;
intros; subst; apply ord_inj; simpl; apply Nat.succ_inj in H; easy.
Qed.
Lemma cast_ordS_max_equiv :
∀ {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
cast_ord H i = ord_max ↔ i = ord_max.
Proof. intros; split; [apply cast_ordS_max_rev | apply cast_ordS_max]. Qed.
Lemma cast_ordS_nmax :
∀ {n m} (H : n.+1 = m.+1) i,
i ≠ ord_max → cast_ord H i ≠ ord_max.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_max_rev. Qed.
Lemma cast_ordS_nmax_rev :
∀ {n m} (H : n.+1 = m.+1) i,
cast_ord H i ≠ ord_max → i ≠ ord_max.
Proof. move=>>; rewrite -contra_equiv; apply cast_ordS_max. Qed.
Lemma cast_ordS_nmax_equiv :
∀ {n m} (H : n.+1 = m.+1) (i : 'I_n.+1),
cast_ord H i ≠ ord_max ↔ i ≠ ord_max.
Proof. intros; split; [apply cast_ordS_nmax_rev | apply cast_ordS_nmax]. Qed.
Lemma cast_ord_bij : ∀ {n m} (H : n = m), bijective (cast_ord H).
Proof. intros; subst; apply injF_bij, cast_ord_inj. Qed.
Lemma cast_ord_surj : ∀ {n m} (H : n = m), surjective (cast_ord H).
Proof. intros; subst; apply injF_surj, cast_ord_inj. Qed.
Lemma cast_ord_val :
∀ {n m} (H : n = m) (i : 'I_n), i = cast_ord H i :> nat.
Proof. easy. Qed.
Lemma cast_ordP :
∀ (P : nat → Prop) {n m} (H : n = m) (i : 'I_n),
P i ↔ P (cast_ord H i).
Proof. easy. Qed.
Lemma cast_ordb :
∀ (b : nat → bool) {n m} (H : n = m) (i : 'I_n),
b i = b (cast_ord H i).
Proof. easy. Qed.
Lemma ord_max_alt_equiv :
∀ {n} (H : 0 < n) (i : 'I_n),
¬ (i < n.-1)%coq_nat ↔ i = Ordinal (subn1_lt H).
Proof.
intros n Hn1 i; generalize (prednK Hn1); intros Hn2.
rewrite (cast_ordP (fun i ⇒ ¬ (i < _)%coq_nat) (sym_eq Hn2)).
rewrite Nat.nlt_ge -ord_max_ge_equiv ord_max_equiv; simpl; split.
intros Hi; apply ord_inj; simpl; rewrite Hi subn1 //.
move=>> ->; simpl; rewrite subn1 //.
Qed.
Lemma cast_ord0_leq_equiv :
∀ {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
cast_ord H i = ord0 ↔ i ≤ Ordinal H0.
Proof.
intros m n p H0 H i; rewrite (cast_ord_val H) (ord0_leq_equiv m); easy.
Qed.
Lemma cast_ord0_le_equiv :
∀ {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
cast_ord H i = ord0 ↔ (i ≤ Ordinal H0)%coq_nat.
Proof.
intros m n p H0 H i; rewrite (cast_ord0_leq_equiv H0); split; move⇒ /leP; easy.
Qed.
Lemma cast_ord_n0_gtn_equiv :
∀ {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
cast_ord H i ≠ ord0 ↔ Ordinal H0 < i.
Proof.
intros; rewrite -iff_not_r_equiv nltn_geq; apply cast_ord0_leq_equiv.
Qed.
Lemma cast_ord_n0_gt_equiv :
∀ {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
cast_ord H i ≠ ord0 ↔ (Ordinal H0 < i)%coq_nat.
Proof.
intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord0_le_equiv.
Qed.
Lemma cast_ord_max_geq_equiv :
∀ {n p} (H : n = p.+1) {i : 'I_n},
cast_ord H i = ord_max ↔ Ordinal (ltnSn p) ≤ i.
Proof. intros n p H i; rewrite (cast_ord_val H) ord_max_geq_equiv; easy. Qed.
Lemma cast_ord_max_ge_equiv :
∀ {n p} (H : n = p.+1) {i : 'I_n},
cast_ord H i = ord_max ↔ (Ordinal (ltnSn p) ≤ i)%coq_nat.
Proof.
intros n p H i; rewrite cast_ord_max_geq_equiv; split; move⇒ /leP; easy.
Qed.
Lemma cast_ord_nmax_ltn_equiv :
∀ {n p} (H : n = p.+1) {i : 'I_n},
cast_ord H i ≠ ord_max ↔ i < Ordinal (ltnSn p).
Proof.
intros; rewrite -iff_not_r_equiv nltn_geq; apply cast_ord_max_geq_equiv.
Qed.
Lemma cast_ord_nmax_lt_equiv :
∀ {n p} (H : n = p.+1) {i : 'I_n},
cast_ord H i ≠ ord_max ↔ (i < Ordinal (ltnSn p))%coq_nat.
Proof.
intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord_max_ge_equiv.
Qed.
Lemma cast_ord_incrF : ∀ {n1 n2} (H : n1 = n2), incrF (cast_ord H).
Proof. easy. Qed.
Lemma incrF_cast_ord_0 :
∀ {m1 n1 n2} (H1 : m1 = n1.+1) (f : 'I_{m1,n2.+1}) (i2 : 'I_n2.+1),
incrF f → Rg f i2 → (f (cast_ord (sym_eq H1) ord0) ≤ i2)%coq_nat.
Proof.
intros m1 n1 n2 H1 f i2 Hf [i1 _]; rewrite -(comp_correct _ f).
pose (g := f \o (cast_ord (sym_eq H1))); fold g; apply incrF_0; [| unfold g].
apply incrF_comp; [apply cast_ord_incrF | easy].
apply Rg_ex; ∃ (cast_ord H1 i1); rewrite comp_correct cast_ordK; easy.
Qed.
Lemma incrF_cast_ord_max :
∀ {m1 n1 n2} (H1 : m1 = n1.+1) (f : 'I_{m1,n2.+1}) (i2 : 'I_n2.+1),
incrF f → Rg f i2 → (i2 ≤ f (cast_ord (sym_eq H1) ord_max))%coq_nat.
Proof.
intros m1 n1 n2 H1 f i2 Hf [i1 _]; rewrite -(comp_correct _ f).
pose (g := f \o (cast_ord (sym_eq H1))); fold g; apply incrF_max; [| unfold g].
apply incrF_comp; [apply cast_ord_incrF | easy].
apply Rg_ex; ∃ (cast_ord H1 i1); rewrite comp_correct cast_ordK; easy.
Qed.
Definition and properties of cast_f_ord.
Definition cast_f_ord {n1 n2} (H : n1 = n2) (p1 : 'I_[n1]) : 'I_[n2] :=
fun i2 ⇒ cast_ord H (p1 (cast_ord (sym_eq H) i2)).
Lemma cast_f_ord_refl :
∀ {n} (H : n = n) (p : 'I_[n]), cast_f_ord H p = p.
Proof.
intros; apply fun_ext; intro; unfold cast_f_ord; rewrite !cast_ord_id; easy.
Qed.
Lemma cast_f_ord_id :
∀ {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
same_fun p1 id → cast_f_ord H p1 = id.
Proof. move=>>; subst; rewrite cast_f_ord_refl; apply fun_ext. Qed.
Lemma cast_f_ord_inj :
∀ {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
injective p1 → injective (cast_f_ord H p1).
Proof. intros; subst; rewrite cast_f_ord_refl; easy. Qed.
Lemma cast_f_ord_bij :
∀ {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
injective p1 → bijective (cast_f_ord H p1).
Proof. intros; apply injF_bij, cast_f_ord_inj; easy. Qed.
Lemma cast_f_ord_surj :
∀ {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]},
injective p1 → surjective (cast_f_ord H p1).
Proof. intros; apply injF_surj, cast_f_ord_inj; easy. Qed.
Lemma cast_f_ord_comp :
∀ {n1 n2} (H : n1 = n2) {p1 q1 : 'I_[n1]},
cast_f_ord H (p1 \o q1) = (cast_f_ord H p1) \o (cast_f_ord H q1).
Proof. intros; subst; rewrite !cast_f_ord_refl; easy. Qed.
Lemma cast_f_ord_f_inv :
∀ {n1 n2} (H : n1 = n2) {p1 : 'I_[n1]} (Hp1 : bijective p1),
cast_f_ord H (f_inv Hp1) = f_inv (cast_f_ord_bij H (bij_inj Hp1)).
Proof.
intros; subst; apply f_inv_uniq_l; intro;
rewrite !cast_f_ord_refl; apply f_inv_can_l.
Qed.
End Cast_ord.
Section Widen_Lift_S.
Lemma narrow_S_proof : ∀ {n} {i : 'I_n.+1}, i ≠ ord_max → i < n.
Proof.
move⇒ n [i Hi1] /ord_neq_compat Hi2; simpl in *; apply ltnSE in Hi1.
apply /ltP; apply Nat.nle_gt; contradict Hi2.
apply Nat.le_antisymm; [apply /leP | ]; easy.
Qed.
Lemma lower_S_proof : ∀ {n} {i : 'I_n.+1}, i ≠ ord0 → i - 1 < n.
Proof.
move=>> Hi; apply ordS_lt_minus_1; contradict Hi; apply ord_inj; easy.
Qed.
Definition widen_S {n} (i : 'I_n) : 'I_n.+1 := widen_ord (leqnSn n) i.
Definition narrow_S {n} {i : 'I_n.+1} (H : i ≠ ord_max) : 'I_n :=
Ordinal (narrow_S_proof H).
Definition lift_S {n} (i : 'I_n) : 'I_n.+1 := lift ord0 i.
Definition lower_S {n} {i : 'I_n.+1} (H : i ≠ ord0) : 'I_n :=
Ordinal (lower_S_proof H).
Lemma widen_S_correct : ∀ {n} (i : 'I_n), widen_S i = i :> nat.
Proof. easy. Qed.
Lemma narrow_S_correct :
∀ {n} {i : 'I_n.+1} (H : i ≠ ord_max), narrow_S H = i :> nat.
Proof. easy. Qed.
Lemma lift_S_correct : ∀ {n} (i : 'I_n), lift_S i = i.+1 :> nat.
Proof. exact lift0. Qed.
Lemma lower_S_correct :
∀ {n} {i : 'I_n.+1} (H : i ≠ ord0), lower_S H = i.-1 :> nat.
Proof. intros n [i Hi] H; simpl; apply subn1. Qed.
Lemma widen_S_0 : ∀ {n}, widen_S (ord0 : 'I_n.+1) = (ord0 : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.
Lemma widen_S_max : ∀ {n}, widen_S (ord_max : 'I_n.+1) = (ord_pred_max : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.
Lemma lift_S_0 : ∀ {n}, lift_S (ord0 : 'I_n.+1) = (ord1 : 'I_n.+2).
Proof. easy. Qed.
Lemma lift_S_max : ∀ {n}, lift_S (ord_max : 'I_n.+1) = (ord_max : 'I_n.+2).
Proof. intros; apply ord_inj; easy. Qed.
Lemma widen_S_not_last : ∀ {n} (i : 'I_n), widen_S i ≠ ord_max.
Proof. intros; apply ord_lt_neq; simpl; apply /ltP; easy. Qed.
Lemma narrow_widen_S :
∀ {n} {i : 'I_n} (H : widen_S i ≠ ord_max), narrow_S H = i.
Proof. intros; apply ord_inj; easy. Qed.
Lemma widen_narrow_S :
∀ {n} {i : 'I_n.+1} (H : i ≠ ord_max), widen_S (narrow_S H) = i.
Proof. intros; apply ord_inj; easy. Qed.
Lemma lift_S_not_first : ∀ {n} (i : 'I_n), (lift_S i) ≠ ord0.
Proof. intros; apply not_eq_sym; apply ord_lt_neq; simpl; apply /ltP; easy. Qed.
Lemma lower_lift_S :
∀ {n} {i : 'I_n} (H : lift_S i ≠ ord0), lower_S H = i.
Proof. intros; apply ord_inj; simpl; unfold bump; auto with arith. Qed.
Lemma lower_lift_S_cast_ord :
∀ {n1 n2} (H12 : n1 = n2) (H21 : n2.+1 = n1.+1)
{i1 : 'I_n1} (Hi1 : lift_S (cast_ord H12 i1) ≠ ord0),
lower_S (cast_ordS_n0 H21 (lift_S (cast_ord H12 i1)) Hi1) = i1.
Proof. intros; apply ord_inj; simpl; unfold bump; auto with arith. Qed.
Lemma lift_lower_S :
∀ {n} {i : 'I_n.+1} (H : i ≠ ord0), lift_S (lower_S H) = i.
Proof.
intros n i H; apply ord_inj; simpl; apply ord_n0_nlt_equiv, Nat.nlt_ge in H.
rewrite bump_r subn1; auto with zarith.
Qed.
Lemma lift_lower_S_cast_ord :
∀ {n1 n2} (H12 : n1.+1 = n2.+1) (H21 : n2 = n1)
{i1 : 'I_n1.+1} (Hi1 : i1 ≠ ord0),
lift_S (cast_ord H21 (lower_S (cast_ordS_n0 H12 _ Hi1))) = i1.
Proof.
move⇒ n1 n2 H12 H21 i1 Hi1; apply ord_inj; simpl; rewrite -minusE.
apply ord_n0_nlt_equiv, Nat.nlt_ge in Hi1.
rewrite → bump_r, subn1; auto with zarith.
Qed.
Lemma lift_widen_S :
∀ {n} (i : 'I_n), lift_S (widen_S i) = widen_S (lift_S i).
Proof. intros; apply ord_inj; easy. Qed.
Lemma widen_lt_lift_S : ∀ {n} (i : 'I_n), (widen_S i < lift_S i)%coq_nat.
Proof. intros; rewrite widen_S_correct lift_S_correct; lia. Qed.
Lemma widen_not_lift_S : ∀ {n} (i : 'I_n), widen_S i ≠ lift_S i.
Proof. intros; apply ord_lt_neq, widen_lt_lift_S. Qed.
Lemma lift_not_widen_S : ∀ {n} (i : 'I_n), lift_S i ≠ widen_S i.
Proof. intros; apply not_eq_sym, widen_not_lift_S. Qed.
Lemma widen_S_inj : ∀ {n}, injective (@widen_S n).
Proof. intros; apply widen_ord_inj. Qed.
Lemma narrow_S_inj :
∀ {n},
injective (fun i : {k : 'I_n.+1 | k ≠ ord_max} ⇒ narrow_S (proj2_sig i)).
Proof.
move⇒ n [i Hi] [j Hj] /(f_equal widen_S);
rewrite !widen_narrow_S; apply eq_exist.
Qed.
Lemma narrow_S_injS :
∀ {n} {i j : 'I_n.+1} (Hi : i ≠ ord_max) (Hj : j ≠ ord_max),
narrow_S Hi = narrow_S Hj → i = j.
Proof. move=>> /(f_equal widen_S); rewrite !widen_narrow_S; easy. Qed.
Lemma lift_S_inj : ∀ {n}, injective (@lift_S n).
Proof.
intros n; replace (injective lift_S) with (injective (@lift_S n.+1.-1));
[apply lift_inj | easy].
Qed.
Lemma lower_S_inj :
∀ {n},
injective (fun i : {k : 'I_n.+1 | k ≠ ord0} ⇒ lower_S (proj2_sig i)).
Proof.
move⇒ n [i Hi] [j Hj] /(f_equal lift_S);
rewrite !lift_lower_S; apply eq_exist.
Qed.
Lemma lower_S_injS :
∀ {n} {i j : 'I_n.+1} (Hi : i ≠ ord0) (Hj : j ≠ ord0),
lower_S Hi = lower_S Hj → i = j.
Proof. move=>> /(f_equal lift_S); rewrite !lift_lower_S; easy. Qed.
Lemma widen_S_incrF : ∀ {n}, incrF (@widen_S n).
Proof. easy. Qed.
Lemma narrow_S_incrF :
∀ {n}, incrF (fun i : 'I_n ⇒ narrow_S (widen_S_not_last (widen_S i))).
Proof. move=>>; rewrite !narrow_widen_S; apply widen_S_incrF. Qed.
Lemma narrow_S_incrS :
∀ {n} {i j : 'I_n.+1} (Hi : i ≠ ord_max) (Hj : j ≠ ord_max),
(i < j)%coq_nat → (narrow_S Hi < narrow_S Hj)%coq_nat.
Proof. easy. Qed.
Lemma lift_S_incrF : ∀ {n}, incrF (@lift_S n).
Proof. move=>> /ltP ⇒ H; apply /ltP; rewrite bump_incr; easy. Qed.
Lemma lower_S_incrF :
∀ {n}, incrF (fun i : 'I_n ⇒ lower_S (lift_S_not_first (lift_S i))).
Proof. move=>>; rewrite !lower_lift_S; apply lift_S_incrF. Qed.
Lemma lower_S_incrS :
∀ {n} {i j : 'I_n.+1} (Hi : i ≠ ord0) (Hj : j ≠ ord0),
(i < j)%coq_nat → (lower_S Hi < lower_S Hj)%coq_nat.
Proof.
move⇒ n i j Hi Hj /ltP H; apply /ltP; apply ltn_sub2r; [| easy].
apply: (leq_ltn_trans _ H); apply (ord_n0_gtn_equiv n) in Hi; easy.
Qed.
Lemma extF_widenF_S :
∀ {E : Type} {n} (A B : 'I_n.+1 → E),
(fun i ⇒ A (widen_S i)) = (fun i ⇒ B (widen_S i)) → A ord_max = B ord_max →
A = B.
Proof.
move=>> /fun_ext_rev H0 H1; apply fun_ext; intros i.
destruct (ord_eq_dec i ord_max) as [-> | Hi];
[| rewrite -!(widen_narrow_S Hi)]; easy.
Qed.
Lemma extF_liftF_S :
∀ {E : Type} {n} (A B : 'I_n.+1 → E),
A ord0 = B ord0 → (fun i ⇒ A (lift_S i)) = (fun i ⇒ B (lift_S i)) →
A = B.
Proof.
move=>> H0 /fun_ext_rev H1; apply fun_ext; intros i.
destruct (ord_eq_dec i ord0) as [-> | Hi];
[| rewrite -!(lift_lower_S Hi)]; easy.
Qed.
End Widen_Lift_S.
Section Ord_compl5.
Lemma Rg_0_liftF_S :
∀ {n1 n2} {f : 'I_{n1.+1,n2}},
Rg f = union (eq^~ (f ord0)) (Rg (fun j1 ⇒ f (lift_S j1))).
Proof.
intros n1 n2 f; apply subset_ext_equiv; split.
intros i2 [i1 _]; destruct (ord_eq_dec i1 ord0) as [-> | Hi1]; [left; easy |].
right; rewrite -(lift_lower_S Hi1); apply (Rg_correct (lower_S Hi1)); easy.
intros i2 [-> | [i1 _]]; easy.
Qed.
Lemma incrF_Rg_le_0 :
∀ {n1 n2} {f g : 'I_{n1.+1,n2}},
incrF f → incrF g → Rg f = Rg g → (f ord0 ≤ g ord0)%coq_nat.
Proof.
intros n1 n2 f g Hf Hg H1;
destruct (Nat.le_gt_cases (f ord0) (g ord0)) as [H0 | H0]; [easy |].
assert (H2 : Rg f (g ord0)) by now rewrite H1.
induction H2 as [i _]; contradict H0; apply Nat.le_ngt.
destruct (ord_eq_dec i ord0) as [-> | Hi]; [easy |].
apply (incrF_nondecrF Hf), ord_n0_gt_equiv; easy.
Qed.
Lemma fun_ext_incrF_Rg :
∀ {n1 n2} {f g : 'I_{n1,n2}},
incrF f → incrF g → Rg f = Rg g → f = g.
Proof.
intros n1; induction n1; [intros; apply fun_ext; intros [i Hi]; easy |].
intros n2 f g Hf Hg HRg.
assert (H0 : f ord0 = g ord0)
by now apply ord_inj, Nat.le_antisymm; apply incrF_Rg_le_0.
apply extF_liftF_S; [easy | apply IHn1].
move=>> /ltP H; apply Hf; apply /ltP; easy.
move=>> /ltP H; apply Hg; apply /ltP; easy.
apply union_inj_r with (eq^~ (f ord0)); [| rewrite H0 |].
move⇒ i2 → H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hf) in Hi1; easy.
move⇒ i2 → H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hg) in Hi1; easy.
apply trans_eq with (Rg f); [apply sym_eq | rewrite HRg H0]; apply Rg_0_liftF_S.
Qed.
End Ord_compl5.
Section First_Last_Concat_ord.
Definition first_ord {n1} n2 (i : 'I_n1) : 'I_(n1 + n2) := lshift n2 i.
Definition last_ord n1 {n2} (i : 'I_n2) : 'I_(n1 + n2) := rshift n1 i.
Lemma concat_l_ord_proof :
∀ {n1 n2} (i : 'I_(n1 + n2)), (i < n1)%coq_nat → i < n1.
Proof. move=>> /ltP; easy. Qed.
Lemma concat_r_ord_proof :
∀ {n1 n2} (i : 'I_(n1 + n2)), ¬ (i < n1)%coq_nat → i - n1 < n2.
Proof.
intros; apply /ltP; rewrite <- minusE.
apply nat_lt2_add_lt1_sub_l; try now apply Nat.nlt_ge.
apply /ltP; rewrite plusE; easy.
Qed.
Definition concat_l_ord {n1 n2}
{i : 'I_(n1 + n2)} (H : (i < n1)%coq_nat) : 'I_n1 :=
Ordinal (concat_l_ord_proof i H).
Definition concat_r_ord {n1 n2}
{i : 'I_(n1 + n2)} (H : ¬ (i < n1)%coq_nat) : 'I_n2 :=
Ordinal (concat_r_ord_proof i H).
Lemma concat_l_first :
∀ {n1 n2} {i1 : 'I_n1} (H : (first_ord n2 i1 < n1)%coq_nat),
concat_l_ord H = i1.
Proof. intros; apply ord_inj; easy. Qed.
Lemma first_concat_l :
∀ {n1 n2} {i : 'I_(n1 + n2)} (H : (i < n1)%coq_nat),
first_ord n2 (concat_l_ord H) = i.
Proof. intros; apply ord_inj; easy. Qed.
Lemma concat_r_last :
∀ {n1 n2} {i2 : 'I_n2} (H : ¬ (last_ord n1 i2 < n1)%coq_nat),
concat_r_ord H = i2.
Proof. intros; apply ord_inj; simpl; auto with arith. Qed.
Lemma last_concat_r :
∀ {n1 n2} {i : 'I_(n1 + n2)} (H : ¬ (i < n1)%coq_nat),
last_ord n1 (concat_r_ord H) = i.
Proof. intros; apply ord_inj; simpl; auto with zarith arith. Qed.
End First_Last_Concat_ord.
Section Skip_Insert_ord.
Definition skip_ord {n} (i0 : 'I_n.+1) (j : 'I_n) : 'I_n.+1 :=
lift i0 (cast_ord (pred_Sn n) j).
Definition insert_ord {n} {i0 i : 'I_n.+1} (H : i ≠ i0) : 'I_n :=
proj1_sig (unlift_some (neqP (not_eq_sym H))).
Lemma insert_ord_inj :
∀ {n} {i0 i1 i2 : 'I_n.+2} (H1 : i1 ≠ i0) (H2 : i2 ≠ i0),
insert_ord H1 = insert_ord H2 → i1 = i2.
Proof.
intros n i0 i1 i2 H1 H2 H; unfold insert_ord in H.
destruct (unlift_some (neqP (not_eq_sym H1))) as [j1 Hj1a Hj1b],
(unlift_some (neqP (not_eq_sym H2))) as [j2 Hj2a Hj2b]; simpl in H.
rewrite Hj2a -H; easy.
Qed.
Lemma insert_ord_neq_compat :
∀ {n} {i0 i1 i2 : 'I_n.+2} (H1 : i1 ≠ i0) (H2 : i2 ≠ i0),
i2 ≠ i1 → insert_ord H2 ≠ insert_ord H1.
Proof. move=>>; apply contra_not, insert_ord_inj. Qed.
Lemma skip_ord_correct_l :
∀ {n} (i0 : 'I_n.+1) (j : 'I_n),
(j < i0)%coq_nat → skip_ord i0 j = widen_S j.
Proof. intros n i0 j Hj; apply ord_inj; simpl; apply bump_l; easy. Qed.
Lemma skip_ord_correct_m :
∀ {n} (i0 : 'I_n.+1) (j : 'I_n), skip_ord i0 j ≠ i0.
Proof. intros; apply not_eq_sym; apply /eqP; apply neq_lift. Qed.
Lemma skip_ord_correct_r :
∀ {n} (i0 : 'I_n.+1) (j : 'I_n),
¬ (j < i0)%coq_nat → skip_ord i0 j = lift_S j.
Proof.
intros; apply ord_inj; simpl.
rewrite !bump_r; [ | apply Nat.le_0_l | apply Nat.nlt_ge]; easy.
Qed.
Lemma skip_ord_0 :
∀ {n} (i0 : 'I_n.+2), i0 ≠ ord0 → skip_ord i0 ord0 = ord0.
Proof.
intros n i0 Hi0; rewrite skip_ord_correct_l; try apply widen_S_0.
apply ord_n0_nlt_equiv in Hi0; destruct i0; simpl in *; auto with zarith.
Qed.
Lemma skip_ord_max :
∀ {n} (i0 : 'I_n.+2), i0 ≠ ord_max → skip_ord i0 ord_max = ord_max.
Proof.
intros n i0 Hi0; rewrite skip_ord_correct_r; try apply lift_S_max.
apply ord_nmax_lt_equiv in Hi0; destruct i0; simpl in *; auto with zarith.
Qed.
Lemma skip_ord_inj : ∀ {n} (i0 : 'I_n.+1), injective (skip_ord i0).
Proof. intros; apply: inj_comp_compat lift_inj; apply cast_ord_inj. Qed.
Lemma insert_ord_compat_P :
∀ {n} {i0 i : 'I_n.+1} (H H' : i ≠ i0), insert_ord H = insert_ord H'.
Proof. intros; f_equal; apply proof_irrel. Qed.
Lemma skip_insert_ord :
∀ {n} {i0 i : 'I_n.+1} (H : i ≠ i0), skip_ord i0 (insert_ord H) = i.
Proof.
intros n i0 i H; unfold skip_ord, insert_ord.
destruct (unlift_some (neqP (not_eq_sym H))) as [j Hj1 Hj2]; simpl.
rewrite Hj1; f_equal; apply ord_inj; easy.
Qed.
Lemma insert_skip_ord :
∀ {n} {i0 : 'I_n.+1} {j : 'I_n} (H : skip_ord i0 j ≠ i0),
insert_ord H = j.
Proof. intros n i0 j H; apply (skip_ord_inj i0), skip_insert_ord. Qed.
Lemma skip_insert_ord_eq :
∀ {n} {i0 i : 'I_n.+1} (Hi : i ≠ i0) (j : 'I_n),
skip_ord i0 j = i ↔ j = insert_ord Hi.
Proof.
intros n i0 i Hi j; split.
intros Hj; apply (skip_ord_inj i0); rewrite skip_insert_ord; easy.
move⇒ ->; apply skip_insert_ord.
Qed.
Lemma skip_insert_ord_neq :
∀ {n} {i0 i : 'I_n.+1} (Hi : i ≠ i0) (j : 'I_n),
skip_ord i0 j ≠ i ↔ j ≠ insert_ord Hi.
Proof. intros; rewrite -iff_not_equiv; apply skip_insert_ord_eq. Qed.
Lemma skip_insert_ord_gen :
∀ {n} (j0 : 'I_n.+1) {j1 j i0 i1}
(Hj1 : j ≠ j1) (Hj2 : skip_ord i0 j ≠ i1),
i0 = skip_ord i1 j0 → i1 = skip_ord i0 j1 →
skip_ord j0 (insert_ord Hj1) = insert_ord Hj2.
Proof.
intros n j0 j1 j i0 i1 Hj1 Hj2 Hi0 Hi1.
apply skip_insert_ord_eq; unfold skip_ord, insert_ord; simpl.
apply ord_inj; simpl.
destruct (unlift_some (neqP (not_eq_sym Hj1))) as [k Hk1 Hk2]; simpl in ×.
unfold lift in Hk1.
apply (f_equal (@nat_of_ord _)) in Hi0, Hi1, Hk1; simpl in ×.
rewrite Hk1; apply bump_comm; easy.
Qed.
Lemma skip_ord_first : ∀ {n} (j : 'I_n), skip_ord ord0 j = lift_S j.
Proof. intros; apply skip_ord_correct_r; easy. Qed.
Lemma skip_ord_last :
∀ {n} (j : 'I_n), skip_ord ord_max j = widen_S j.
Proof. intros; apply skip_ord_correct_l; apply /ltP; easy. Qed.
Lemma insert_ord_correct_l :
∀ {n} {i0 i : 'I_n.+1} (H : i ≠ i0) (H' : (i < i0)%coq_nat),
insert_ord H = narrow_S (ord_nmax_lt H').
Proof.
intros n i0 i H H'; apply (skip_ord_inj i0); rewrite skip_insert_ord.
rewrite -{1}(widen_narrow_S (ord_nmax_lt H')).
rewrite skip_ord_correct_l; easy.
Qed.
Lemma insert_ord_correct_r :
∀ {n} {i0 i : 'I_n.+1} (H : i ≠ i0) (H' : (i0 < i)%coq_nat),
insert_ord H = lower_S (ord_n0_gt H').
Proof.
intros n i0 i H H'; apply (skip_ord_inj i0); rewrite skip_insert_ord.
rewrite -{1}(lift_lower_S (ord_n0_gt H')).
rewrite skip_ord_correct_r; try easy; simpl.
apply Nat.nlt_ge, Nat.lt_succ_r; rewrite subn1 (Nat.lt_succ_pred i0); easy.
Qed.
Lemma insert_ord_monot :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0),
(i < i1)%coq_nat → (insert_ord H0 < insert_ord H)%coq_nat.
Proof.
intros n i0 i1 i H H0 H1.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Ha | Ha] | Ha].
2: contradict Ha; apply ord_neq_compat; easy.
assert (H0a : (i < i0)%coq_nat) by auto with zarith.
rewrite 2!insert_ord_correct_l 2!narrow_S_correct; easy.
destruct (nat_lt_eq_gt_dec i i0) as [[H0a | H0a] | H0a].
2: contradict H0a; apply ord_neq_compat; easy.
rewrite insert_ord_correct_l insert_ord_correct_r.
rewrite narrow_S_correct lower_S_correct; auto with zarith.
rewrite 2!insert_ord_correct_r 2!lower_S_correct; auto with zarith.
Qed.
Lemma insert_ord_0 :
∀ {n} {i0 : 'I_n.+2} (Hi0 : ord0 ≠ i0), insert_ord Hi0 = ord0.
Proof. intros; apply sym_eq, skip_insert_ord_eq, skip_ord_0; intuition. Qed.
Lemma insert_ord_max :
∀ {n} {i0 : 'I_n.+2} (Hi0 : ord_max ≠ i0), insert_ord Hi0 = ord_max.
Proof. intros; apply sym_eq, skip_insert_ord_eq, skip_ord_max; intuition. Qed.
Lemma insert_concat_r_ord_0 :
∀ {n} {i : 'I_n.+1}
(Hi1 : i ≠ ord0) (Hi2 : ¬ (cast_ord (sym_eq (add1n n)) i < 1)%coq_nat),
insert_ord Hi1 = concat_r_ord Hi2.
Proof.
intros n i Hi1 Hi2; rewrite insert_ord_correct_r.
apply Nat.nle_gt; contradict Hi2; auto with arith.
intros Hi3; apply ord_inj; easy.
Qed.
Lemma insert_concat_l_ord_max :
∀ {n} {i : 'I_n.+1}
(Hi1 : i ≠ ord_max) (Hi2 : (cast_ord (sym_eq (addn1 n)) i < n)%coq_nat),
insert_ord Hi1 = concat_l_ord Hi2.
Proof. intros; rewrite insert_ord_correct_l; apply ord_inj; easy. Qed.
Definition and properties of skip_f_ord.
Lemma skip_f_not :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0 j,
p (skip_ord i0 j) ≠ p i0.
Proof. move⇒ n p Hp i0 j /Hp Hj; contradict Hj; apply skip_ord_correct_m. Qed.
Definition skip_f_ord {n} {p : 'I_[n.+1]} (Hp : injective p) i0 : 'I_[n] :=
fun j ⇒ insert_ord (skip_f_not Hp i0 j).
Lemma skip_f_ord_correct :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0 j,
skip_ord (p i0) (skip_f_ord Hp i0 j) = p (skip_ord i0 j).
Proof. intros; rewrite skip_insert_ord; easy. Qed.
Lemma skip_f_ord_id :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
same_fun p id → skip_f_ord Hp i0 = id.
Proof.
intros n p Hp1 i0 Hp2; apply fun_ext; intros j.
apply (skip_ord_inj (p i0)); rewrite skip_f_ord_correct !Hp2; easy.
Qed.
Lemma skip_f_ord_inj :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
injective (skip_f_ord Hp i0).
Proof.
move⇒ n p Hp i0 j1 j2 /(f_equal (skip_ord (p i0))) Hj.
rewrite !skip_f_ord_correct in Hj; apply (skip_ord_inj i0), Hp; easy.
Qed.
Lemma skip_f_ord_bij :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
bijective (skip_f_ord Hp i0).
Proof. intros; apply injF_bij, skip_f_ord_inj. Qed.
Lemma skip_f_ord_surj :
∀ {n} {p : 'I_[n.+1]} (Hp : injective p) i0,
surjective (skip_f_ord Hp i0).
Proof. intros; apply injF_surj, skip_f_ord_inj. Qed.
Lemma skip_f_ord_comp :
∀ {n} {p q : 'I_[n.+1]}
(Hp : injective p) (Hq : injective q) (H : injective (p \o q)) i0 j,
skip_f_ord H i0 j = skip_f_ord Hp (q i0) (skip_f_ord Hq i0 j).
Proof.
intros n p q Hp Hq H i0 j; apply (skip_ord_inj (p (q i0))).
rewrite !skip_f_ord_correct; easy.
Qed.
Lemma skip_f_ord_comp_alt :
∀ {n} {p q : 'I_[n.+1]}
(Hp : injective p) (Hq : injective q) i0 j,
skip_f_ord (inj_comp_compat Hq Hp) i0 j =
skip_f_ord Hp (q i0) (skip_f_ord Hq i0 j).
Proof. intros; apply skip_f_ord_comp. Qed.
Lemma skip_f_ord_f_inv :
∀ {n} {p : 'I_[n.+1]} (Hp : bijective p) i0,
skip_f_ord (f_inv_inj Hp) i0 =
f_inv (skip_f_ord_bij (bij_inj Hp) (f_inv Hp i0)).
Proof.
intros n p Hp i0; apply f_inv_uniq_l; intros j.
rewrite -{1}(f_inv_can_r Hp i0) -skip_f_ord_comp_alt skip_f_ord_id//.
apply f_inv_can_l.
Qed.
Definition and properties of insert_f_ord.
Definition insert_f_ord {n} (p : 'I_[n]) i0 : 'I_[n.+1] :=
fun i ⇒ match (ord_eq_dec i i0) with
| left _ ⇒ i0
| right H ⇒ skip_ord i0 (p (insert_ord H))
end.
Lemma insert_f_ord_correct_l :
∀ {n} (p : 'I_[n]) i0 i, i = i0 → insert_f_ord p i0 i = i0.
Proof. intros; unfold insert_f_ord; destruct (ord_eq_dec _ _); easy. Qed.
Lemma insert_f_ord_correct_r :
∀ {n} (p : 'I_[n]) {i0 i} (H : i ≠ i0),
insert_f_ord p i0 i = skip_ord i0 (p (insert_ord H)).
Proof.
intros; unfold insert_f_ord; destruct (ord_eq_dec _ _);
[easy | repeat f_equal; apply proof_irrel].
Qed.
Definition and properties of extend_f_S.
Definition extend_f_S {n1 n2} (p : 'I_{n1,n2}) : 'I_{n1.+1,n2.+1} :=
fun i ⇒ match (ord_eq_dec i ord_max) with
| left _ ⇒ ord_max
| right H ⇒ widen_S (p (narrow_S H))
end.
Lemma extend_f_S_correct_l :
∀ {n1 n2} (p : 'I_{n1,n2}) i, i = ord_max → extend_f_S p i = ord_max.
Proof. intros; unfold extend_f_S; destruct (ord_eq_dec _ _); easy. Qed.
Lemma extend_f_S_correct_r :
∀ {n1 n2} (p : 'I_{n1,n2}) {i} (H : i ≠ ord_max),
extend_f_S p i = widen_S (p (narrow_S H)).
Proof.
intros; unfold extend_f_S; destruct (ord_eq_dec _ _);
[easy | repeat f_equal; apply proof_irrel].
Qed.
End Skip_Insert_ord.
Section Skip2_Insert2_ord.
Definition skip2_ord
{n} {i0 i1 : 'I_n.+2} (H : i1 ≠ i0) (j : 'I_n) : 'I_n.+2 :=
skip_ord i0 (skip_ord (insert_ord H) j).
Definition insert2_ord
{n} {i0 i1 i : 'I_n.+2}
(H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1) : 'I_n :=
insert_ord (insert_ord_neq_compat H H0 H1).
Lemma skip2_ord_compat_P :
∀ {n} {i0 i1 : 'I_n.+2} (H H' : i1 ≠ i0), skip2_ord H = skip2_ord H'.
Proof.
intros; apply fun_ext; intro; unfold skip2_ord; do 2 f_equal.
apply insert_ord_compat_P.
Qed.
Lemma skip2_ord_sym_lt :
∀ {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat),
skip2_ord (ord_lt_neq_sym H) = skip2_ord (ord_lt_neq H).
Proof.
intros n i0 i1 H; apply fun_ext; intros j; apply ord_inj; simpl.
destruct (le_dec (insert_ord (ord_lt_neq_sym H)) j) as [H1 | H1];
[rewrite (bump_r _ j); try easy | rewrite (bump_l _ j); try now apply Nat.nle_gt];
rewrite insert_ord_correct_r in H1;
(destruct (le_dec (insert_ord (ord_lt_neq H)) j) as [H2 | H2];
[rewrite (bump_r (insert_ord _) j); try easy |
rewrite (bump_l (insert_ord _) j); try now apply Nat.nle_gt];
rewrite insert_ord_correct_l in H2);
destruct j as [j Hj]; simpl in *; rewrite -minusE in H1.
rewrite (bump_r i0).
rewrite (bump_r i1); auto with zarith.
apply (Nat.le_trans _ j); try apply le_S; easy.
contradict H2; auto with zarith.
rewrite (bump_r i0); try easy.
rewrite (bump_l i1); auto with zarith.
rewrite (bump_l i0); auto with zarith.
rewrite (bump_l i1); auto with zarith.
Qed.
Lemma skip2_ord_sym :
∀ {n} {i0 i1 : 'I_n.+2} (H10 : i1 ≠ i0) (H01 : i0 ≠ i1),
skip2_ord H10 = skip2_ord H01.
Proof.
intros n i0 i1 H10 H01.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Hi | Hi] | Hi].
rewrite (skip2_ord_compat_P _ (ord_lt_neq_sym Hi)) skip2_ord_sym_lt.
apply skip2_ord_compat_P.
contradict H10; apply ord_inj, sym_eq; easy.
rewrite (skip2_ord_compat_P _ (ord_lt_neq_sym Hi)) skip2_ord_sym_lt.
apply skip2_ord_compat_P.
Qed.
Lemma skip2_ord_sym_alt :
∀ {n} {i0 i1 : 'I_n.+2} (H : i1 ≠ i0),
skip2_ord H = skip2_ord (not_eq_sym H).
Proof. intros; apply skip2_ord_sym. Qed.
Lemma skip2_ord_correct_l :
∀ {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
(j < i0)%coq_nat → skip2_ord (ord_lt_neq_sym H) j = widen_S (widen_S j).
Proof.
intros n i0 i1 H j Hj; unfold skip2_ord; rewrite skip_ord_correct_l.
f_equal; apply skip_ord_correct_l.
1,2: unfold skip_ord, insert_ord;
destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym H))))
as [k Hk1 Hk2]; simpl.
2: rewrite bump_l; try easy.
1,2: apply Nat.lt_le_trans with i0; try easy.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.
Lemma skip2_ord_correct_m0 :
∀ {n} {i0 i1 : 'I_n.+2} (H : i1 ≠ i0) (j : 'I_n), skip2_ord H j ≠ i0.
Proof. intros; apply skip_ord_correct_m. Qed.
Lemma skip2_ord_correct_m :
∀ {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
(i0 ≤ j)%coq_nat → (j < i1.-1)%coq_nat →
skip2_ord (ord_lt_neq_sym H) j = lift_S (widen_S j).
Proof.
intros n i0 i1 H j Hj1 Hj2; unfold skip2_ord; rewrite skip_ord_correct_r.
f_equal; apply skip_ord_correct_l.
1,2: unfold skip_ord, insert_ord;
destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym H))))
as [k Hk1 Hk2]; simpl.
2: rewrite bump_l; try now apply Nat.nlt_ge.
1,2: apply Nat.lt_le_trans with i1.-1; try easy.
1,2: apply Nat.eq_le_incl; rewrite Hk1; apply nat_succ_to_pred, lift_r.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.
Lemma skip2_ord_correct_m1 :
∀ {n} {i0 i1 : 'I_n.+2} (H : i1 ≠ i0) (j : 'I_n), skip2_ord H j ≠ i1.
Proof.
intros; rewrite (skip2_ord_sym _ (not_eq_sym _)); apply skip_ord_correct_m.
Qed.
Lemma skip2_ord_correct_r :
∀ {n} {i0 i1 : 'I_n.+2} (H : (i0 < i1)%coq_nat) (j : 'I_n),
(i1.-1 ≤ j)%coq_nat →
skip2_ord (ord_lt_neq_sym H) j = lift_S (lift_S j).
Proof.
intros n i0 i1 Hi j Hj; unfold skip2_ord; rewrite skip_ord_correct_r.
f_equal; apply skip_ord_correct_r, Nat.nlt_ge.
1,2: unfold skip_ord, insert_ord;
destruct (unlift_some (neqP (not_eq_sym (ord_lt_neq_sym Hi))))
as [k Hk1 Hk2]; simpl.
2: rewrite bump_r; auto with zarith.
1,2: apply Nat.le_trans with i1.-1; try easy; rewrite Hk1 lift_r; try easy.
1,2: apply lift_lt_r; rewrite -Hk1; easy.
Qed.
Lemma skip2_ord_inj :
∀ {n} {i0 i1 : 'I_n.+2} (H : i1 ≠ i0), injective (skip2_ord H).
Proof. intros; apply: (inj_comp_compat (skip_ord_inj _)) (skip_ord_inj _). Qed.
Lemma insert_ord2_eq_lt :
∀ {n} {i0 i1 i : 'I_n.+2}
(H10 : i1 ≠ i0) (H01 : i0 ≠ i1) (H0 : i ≠ i0) (H1 : i ≠ i1)
(H0' : insert_ord H1 ≠ insert_ord H01)
(H1' : insert_ord H0 ≠ insert_ord H10),
(i0 < i1)%coq_nat → insert_ord H0' = insert_ord H1'.
Proof.
intros n i0 i1 i H10 H01 H0 H1 H0' H1' H.
destruct (nat_lt_eq_gt_dec i0 i) as [[H0a | H0a] | H0a].
2: contradict H0a; apply ord_neq_compat, not_eq_sym; easy.
destruct (nat_lt_eq_gt_dec i1 i) as [[H1a | H1a] | H1a].
2: contradict H1a; apply ord_neq_compat, not_eq_sym; easy.
assert (H1b : (insert_ord H10 < insert_ord H0)%coq_nat)
by now apply insert_ord_monot.
assert (H0b : (insert_ord H01 < insert_ord H1)%coq_nat)
by now apply insert_ord_monot.
rewrite (insert_ord_correct_r H1') (insert_ord_correct_r H0').
apply ord_inj; rewrite 2!lower_S_correct.
rewrite 2!insert_ord_correct_r; easy.
assert (H1b : (insert_ord H0 < insert_ord H10)%coq_nat)
by now apply insert_ord_monot.
assert (H0b : (insert_ord H01 < insert_ord H1)%coq_nat)
by now apply insert_ord_monot.
rewrite (insert_ord_correct_l H1') (insert_ord_correct_r H0').
apply ord_inj; rewrite narrow_S_correct lower_S_correct.
rewrite insert_ord_correct_l insert_ord_correct_r.
rewrite lower_S_correct narrow_S_correct; easy.
assert (H1b : (i < i1)%coq_nat) by now apply Nat.lt_trans with i0.
assert (H1b' : (insert_ord H0 < insert_ord H10)%coq_nat)
by now apply insert_ord_monot.
assert (H0b : (insert_ord H1 < insert_ord H01)%coq_nat)
by now apply insert_ord_monot.
rewrite (insert_ord_correct_l H1') (insert_ord_correct_l H0').
apply ord_inj; rewrite 2!narrow_S_correct.
rewrite 2!insert_ord_correct_l; easy.
Qed.
Lemma insert_ord2_eq :
∀ {n} {i0 i1 i : 'I_n.+2}
(H10 : i1 ≠ i0) (H01 : i0 ≠ i1) (H0 : i ≠ i0) (H1 : i ≠ i1)
(H0' : insert_ord H1 ≠ insert_ord H01)
(H1' : insert_ord H0 ≠ insert_ord H10),
insert_ord H0' = insert_ord H1'.
Proof.
intros n i0 i1 i H10 H01 H0 H1 H1' H0'.
destruct (nat_lt_eq_gt_dec i1 i0) as [[Ha | Ha] | Ha].
2: contradict Ha; apply ord_neq_compat; easy.
symmetry; apply insert_ord2_eq_lt; easy.
apply insert_ord2_eq_lt; easy.
Qed.
Lemma insert_ord2_eq_alt :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1)
(H0' : insert_ord H1 ≠ insert_ord (not_eq_sym H))
(H1' : insert_ord H0 ≠ insert_ord H),
insert_ord H0' = insert_ord H1'.
Proof. intros; apply insert_ord2_eq. Qed.
Lemma insert2_ord_eq :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1)
(H1' : insert_ord H0 ≠ insert_ord H),
insert2_ord H H0 H1 = insert_ord H1'.
Proof. intros; apply insert_ord_compat_P. Qed.
Lemma insert2_ord_compat_P :
∀ {n} {i0 i1 i : 'I_n.+2}
(H H' : i1 ≠ i0) (H0 H0' : i ≠ i0) (H1 H1' : i ≠ i1),
insert2_ord H H0 H1 = insert2_ord H' H0' H1'.
Proof. intros; f_equal; apply proof_irrel. Qed.
Lemma insert2_ord_sym :
∀ {n} {i0 i1 i : 'I_n.+2}
(H10 : i1 ≠ i0) (H01 : i0 ≠ i1) (H0 : i ≠ i0) (H1 : i ≠ i1),
insert2_ord H10 H0 H1 = insert2_ord H01 H1 H0.
Proof. intros; apply insert_ord2_eq. Qed.
Lemma insert2_ord_sym_alt :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1),
insert2_ord H H0 H1 = insert2_ord (not_eq_sym H) H1 H0.
Proof. intros; apply insert2_ord_sym. Qed.
Lemma insert2_ord_eq_sym :
∀ {n} {i0 i1 i : 'I_n.+2} (H10 : i1 ≠ i0) (H01 : i0 ≠ i1)
(H0 : i ≠ i0) (H1 : i ≠ i1) (H0' : insert_ord H1 ≠ insert_ord H01),
insert2_ord H10 H0 H1 = insert_ord H0'.
Proof. intros; rewrite insert2_ord_sym; apply insert_ord_compat_P. Qed.
Lemma insert2_ord_eq_sym_alt :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1)
(H0' : insert_ord H1 ≠ insert_ord (not_eq_sym H)),
insert2_ord H H0 H1 = insert_ord H0'.
Proof. intros; apply insert2_ord_eq_sym. Qed.
Lemma skip2_insert2_ord :
∀ {n} {i0 i1 i : 'I_n.+2} (H : i1 ≠ i0) (H0 : i ≠ i0) (H1 : i ≠ i1),
skip2_ord H (insert2_ord H H0 H1) = i.
Proof. intros; unfold skip2_ord; rewrite 2!skip_insert_ord; easy. Qed.
Lemma insert2_skip2_ord :
∀ {n} {i0 i1 : 'I_n.+2} {j : 'I_n}
(H : i1 ≠ i0) (H0 : skip2_ord H j ≠ i0) (H1 : skip2_ord H j ≠ i1),
insert2_ord H H0 H1 = j.
Proof.
intros n i0 i1 j H H0 H1; apply (skip2_ord_inj H), skip2_insert2_ord.
Qed.
End Skip2_Insert2_ord.
Section Rev_ord.
Lemma rev_ord_correct : ∀ {n} (i : 'I_n), rev_ord i = n - i.+1 :> nat.
Proof. easy. Qed.
Lemma rev_ord_0 : ∀ {n}, rev_ord (@ord0 n) = ord_max.
Proof. intros; apply ord_inj; simpl; rewrite subn1; easy. Qed.
Lemma rev_ord_r :
∀ {n} (i : 'I_n), rev_ord (lift_S i) = widen_S (rev_ord i).
Proof. intros; apply ord_inj; simpl; rewrite bump_r; auto with zarith. Qed.
Lemma rev_ord_l :
∀ {n} (i : 'I_n), rev_ord (widen_S i) = lift_S (rev_ord i).
Proof.
intros; apply ord_inj; simpl; rewrite bump_r; auto with zarith.
rewrite subSS subnSK; easy.
Qed.
Lemma rev_ord_bij : ∀ {n}, bijective (@rev_ord n).
Proof. intros; apply injF_bij, rev_ord_inj. Qed.
Lemma rev_ord_surj : ∀ {n}, surjective (@rev_ord n).
Proof. intros; apply injF_surj, rev_ord_inj. Qed.
Lemma rev_ord_max : ∀ {n}, rev_ord (@ord_max n) = ord0.
Proof. intros; apply ord_inj; simpl; apply subnn. Qed.
Lemma cast_f_rev_ord :
∀ {n1 n2} (H : n1 = n2), cast_f_ord H (@rev_ord n1) = @rev_ord n2.
Proof. intros; subst; apply fun_ext; intro; apply ord_inj; easy. Qed.
End Rev_ord.
Section Move_ord.
Definition and properties of move_ord.
Definition move_ord {n} (i0 i1 i : 'I_n.+1) : 'I_n.+1 :=
match (ord_eq_dec i i1) with
| left _ ⇒ i0
| right H ⇒ skip_ord i0 (insert_ord H)
end.
Lemma move_ord_correct_l :
∀ {n} {i0 i1 i : 'I_n.+1}, i = i1 → move_ord i0 i1 i = i0.
Proof. intros; unfold move_ord; destruct (ord_eq_dec _ _); easy. Qed.
Lemma move_ord_correct_r :
∀ {n} (i0 : 'I_n.+1) {i1 i} (Hi : i ≠ i1),
move_ord i0 i1 i = skip_ord i0 (insert_ord Hi).
Proof.
intros; unfold move_ord; destruct (ord_eq_dec _ _); try easy; f_equal.
apply insert_ord_compat_P.
Qed.
Lemma move_ord_inj : ∀ {n} (i0 i1 : 'I_n.+1), injective (move_ord i0 i1).
Proof.
intros n i0 i1 i i'; unfold move_ord; destruct (ord_eq_dec _ _) as [Hi | Hi],
(ord_eq_dec _ _) as [Hi' | Hi']; try now rewrite Hi Hi'.
intros H; contradict H; apply not_eq_sym, skip_ord_correct_m.
intros H; contradict H; apply skip_ord_correct_m.
destruct n as [| n]; [exfalso; rewrite !I_1_is_unit in Hi; easy |].
move⇒ /skip_ord_inj /insert_ord_inj; easy.
Qed.
Lemma move_ord_bij : ∀ {n} (i0 i1 : 'I_n.+1), bijective (move_ord i0 i1).
Proof. intros; apply injF_bij, move_ord_inj. Qed.
Lemma move_ord_surj : ∀ {n} (i0 i1 : 'I_n.+1), surjective (move_ord i0 i1).
Proof. intros; apply injF_surj, move_ord_inj. Qed.
Lemma move_ord_orth :
∀ {n} (i0 i1 : 'I_n.+1), cancel (move_ord i0 i1) (move_ord i1 i0).
Proof.
intros n i0 i1 i; destruct (ord_eq_dec (move_ord i0 i1 i) i0) as [Hi0 | Hi0].
rewrite Hi0 move_ord_correct_l//;
apply (move_ord_inj i0 i1); rewrite move_ord_correct_l; easy.
rewrite (move_ord_correct_r i1).
unfold skip_ord, insert_ord at 1;
destruct (unlift_some (neqP (not_eq_sym Hi0))) as [j0 Hj0a Hj0b]; simpl in ×.
apply ord_inj; simpl; unfold move_ord in Hj0a;
destruct (ord_eq_dec i i1) as [Hi1 | Hi1].
contradict Hi0; rewrite Hi1 move_ord_correct_l; easy.
unfold skip_ord, insert_ord, lift in Hj0a;
destruct (unlift_some (neqP (not_eq_sym Hi1))) as [j1 Hj1a Hj1b]; simpl in ×.
unfold lift in Hj1a; destruct i1 as [i1 H1], i as [i Hi],
j0 as [j0 Hj0], j1 as [j1 Hj1]; simpl in ×.
apply (f_equal (@nat_of_ord n.+1)) in Hj1a, Hj0a; simpl in ×.
rewrite Hj1a; f_equal; apply (bump_inj i0); easy.
Qed.
Lemma cast_f_move_ord :
∀ {n1 n2} (H : n1.+1 = n2.+1) (i0 i1 : 'I_n1.+1),
cast_f_ord H (move_ord i0 i1) = move_ord (cast_ord H i0) (cast_ord H i1).
Proof.
intros n1 n2 H i0 i1; assert (H' : n1 = n2) by lia. subst.
apply fun_ext; intro; unfold cast_f_ord; rewrite !cast_ord_id; easy.
Qed.
End Move_ord.
Section Transp_ord.
Definition and properties of transp_ord.
Definition transp_ord {n} (i0 i1 i : 'I_n) : 'I_n :=
if ord_eq_dec i i0 then i1 else if ord_eq_dec i i1 then i0 else i.
Lemma transp_ord_sym :
∀ {n} {i0 i1 : 'I_n}, transp_ord i0 i1 = transp_ord i1 i0.
Proof.
intros n i0 i1; apply fun_ext; intros i; unfold transp_ord.
destruct (ord_eq_dec i i0) as [Hi0 | Hi0],
(ord_eq_dec i i1) as [Hi1 | Hi1]; simpl; try easy.
rewrite -Hi0; easy.
Qed.
Lemma transp_ord_correct_l0 :
∀ {n} {i0 i1 i : 'I_n}, i = i0 → transp_ord i0 i1 i = i1.
Proof. intros; unfold transp_ord; destruct (ord_eq_dec _ _); easy. Qed.
Lemma transp_ord_correct_l1 :
∀ {n} {i0 i1 i : 'I_n}, i = i1 → transp_ord i0 i1 i = i0.
Proof. move=>>; rewrite transp_ord_sym; apply transp_ord_correct_l0. Qed.
Lemma transp_ord_correct_r :
∀ {n} {i0 i1 i : 'I_n}, i ≠ i0 → i ≠ i1 → transp_ord i0 i1 i = i.
Proof.
intros; unfold transp_ord; destruct (ord_eq_dec _ _), (ord_eq_dec _ _); easy.
Qed.
Lemma transp_ord_inj : ∀ {n} (i0 i1 : 'I_n), injective (transp_ord i0 i1).
Proof.
intros n i0 i1 i i'.
destruct (ord_eq2_dec i i0 i1) as [[Hi | Hi] | [Hi1 Hi2]];
[rewrite (transp_ord_correct_l0 Hi) | rewrite (transp_ord_correct_l1 Hi) |
rewrite (transp_ord_correct_r Hi1 Hi2)];
(destruct (ord_eq2_dec i' i0 i1) as [[Hi' | Hi'] | [Hi'1 Hi'2]];
[rewrite (transp_ord_correct_l0 Hi') | rewrite (transp_ord_correct_l1 Hi') |
rewrite (transp_ord_correct_r Hi'1 Hi'2)]);
try rewrite Hi; try rewrite Hi'; try easy; intros H; subst; easy.
Qed.
Lemma transp_ord_bij : ∀ {n} (i0 i1 : 'I_n), bijective (transp_ord i0 i1).
Proof. intros; apply injF_bij, transp_ord_inj. Qed.
Lemma transp_ord_surj : ∀ {n} (i0 i1 : 'I_n), surjective (transp_ord i0 i1).
Proof. intros; apply injF_surj, transp_ord_inj. Qed.
Lemma transp_ord_orth :
∀ {n} (i0 i1 : 'I_n), cancel (transp_ord i0 i1) (transp_ord i1 i0).
Proof.
intros n i0 i1 i; destruct (ord_eq2_dec i i0 i1) as [[H | H] | [H1 H2]].
rewrite !transp_ord_correct_l0//.
rewrite !transp_ord_correct_l1//.
rewrite !transp_ord_correct_r//.
Qed.
Lemma transp_ord_invol :
∀ {n} (i0 i1 : 'I_n), involutive (transp_ord i0 i1).
Proof. move=>>; rewrite {1}transp_ord_sym; apply transp_ord_orth. Qed.
Lemma cast_f_transp_ord :
∀ {n1 n2} (H : n1 = n2) (i0 i1 : 'I_n1),
cast_f_ord H (transp_ord i0 i1) = transp_ord (cast_ord H i0) (cast_ord H i1).
Proof.
intros; subst; apply fun_ext; intro; unfold cast_f_ord;
rewrite !cast_ord_id; easy.
Qed.
End Transp_ord.
Section FilterP_ord.
Definition lenPF {n} (P : 'I_n → Prop) : nat := #|fun i ⇒ asbool (P i)|.
Definition filterP_ord
{n} {P : 'I_n → Prop} (j : 'I_(lenPF P)) : 'I_n := enum_val j.
Definition unfilterP_ord
{n} {P : 'I_n → Prop} {i0} (HP0 : P i0) (i : 'I_n) : 'I_(lenPF P) :=
enum_rank_in (in_asboolP HP0) i.
Lemma lenPF_ext_gen :
∀ {n1 n2} (H : n1 = n2) {P1 : 'I_n1 → Prop} {P2 : 'I_n2 → Prop},
(∀ i1, P1 i1 ↔ P2 (cast_ord H i1)) → lenPF P1 = lenPF P2.
Proof.
move=>> H; subst; apply eq_card; intro; apply asbool_equiv_eq.
rewrite H cast_ord_id; easy.
Qed.
Lemma lenPF_ext :
∀ {n} {P Q : 'I_n → Prop},
(∀ i, P i ↔ Q i) → lenPF P = lenPF Q.
Proof.
intros; apply (lenPF_ext_gen (erefl n)); intros; rewrite cast_ord_id //.
Qed.
Lemma lenPF_extb :
∀ {n} {P : 'I_n → Prop} (b : 'I_n → bool),
(∀ i, P i ↔ is_true (b i)) → lenPF P = #|b|.
Proof.
move=>> /lenPF_ext ->; unfold lenPF; do 2 f_equal.
apply fun_ext; intro; apply asboolb.
Qed.
Lemma lenPF_le : ∀ {n} (P : 'I_n → Prop), lenPF P ≤ n.
Proof.
intros n P; apply /leP; replace n with (#|'I_n|) by apply card_ord; apply /leP.
apply max_card.
Qed.
Lemma lenPF_nil : ∀ (P : 'I_0 → Prop), lenPF P = 0.
Proof.
intros; apply eq_card0; apply /pred0P; apply negbNE; apply /pred0Pn.
intros [[i Hi1] Hi2]; easy.
Qed.
Lemma lenPF_nil_alt : ∀ {n} (P : 'I_n → Prop), n = 0 → lenPF P = 0.
Proof. intros; subst; apply lenPF_nil. Qed.
Lemma lenPF0_alt :
∀ {n} (P : 'I_n → Prop), (∀ i, ¬ P i) → lenPF P = 0.
Proof.
intros n P HP; rewrite (lenPF_extb (fun⇒ false)); try apply card0.
intros; rewrite falseE; split; [apply HP | easy].
Qed.
Lemma lenPF0 : ∀ {n}, lenPF (fun _ : 'I_n ⇒ False) = 0.
Proof. intros; apply lenPF0_alt; easy. Qed.
Lemma lenPF0_rev :
∀ {n} (P : 'I_n → Prop), lenPF P = 0 → ∀ i, ¬ P i.
Proof.
move=>> /card0_eq HP i /asboolP Hi; apply (eq_true_false_abs _ Hi (HP i)).
Qed.
Lemma lenPF0_equiv :
∀ {n} (P : 'I_n → Prop), lenPF P = 0 ↔ ∀ i, ¬ P i.
Proof. intros; split; [apply lenPF0_rev | apply lenPF0_alt]. Qed.
Lemma lenPF_n0 :
∀ {n} {P : 'I_n → Prop}, 0 < lenPF P → ∃ i0, P i0.
Proof.
move=>>; rewrite contra_equiv not_ex_all_not_equiv; intros.
apply /negP; rewrite -eqn0Ngt; apply /eqP; apply lenPF0_alt; easy.
Qed.
Lemma lenPF_n0_rev : ∀ {n} {P : 'I_n → Prop} {i0}, P i0 → 0 < lenPF P.
Proof.
move=>>; rewrite -nleq_gtn contra_not_r_equiv leqn0.
move⇒ /eqP HP; apply lenPF0_rev; easy.
Qed.
Lemma lenPF_n0_equiv :
∀ {n} {P : 'I_n → Prop}, 0 < lenPF P ↔ ∃ i0, P i0.
Proof.
intros; split; [apply lenPF_n0 | intros [i0 HP]; apply (lenPF_n0_rev HP)].
Qed.
Lemma lenPF_n0_alt :
∀ {n} {P : 'I_n → Prop} (j : 'I_(lenPF P)), ∃ i0, P i0.
Proof.
intros n P j; apply lenPF_n0; destruct (le_lt_dec (lenPF P) 0) as [HP | HP].
rewrite Nat.le_0_r in HP; rewrite HP in j; destruct j; easy.
apply /ltP; easy.
Qed.
Lemma lenPFS :
∀ {n} {P : 'I_n → Prop} i0, P i0 → lenPF P = (lenPF P).-1.+1.
Proof. move=>> HP0; rewrite prednK; [easy | apply (lenPF_n0_rev HP0)]. Qed.
Lemma lenPFmax_alt :
∀ {n} (P : 'I_n → Prop), (∀ i, P i) → lenPF P = n.
Proof.
intros n P HP; rewrite (lenPF_extb (fun⇒ true)); [apply card_ord | easy].
Qed.
Lemma lenPFmax : ∀ {n}, lenPF (fun _ : 'I_n ⇒ True) = n.
Proof. intros; apply lenPFmax_alt; easy. Qed.
Lemma lenPF_nmax :
∀ {n} {P : 'I_n → Prop}, lenPF P < n → ∃ i0, ¬ P i0.
Proof.
move=>>; rewrite contra_equiv not_ex_not_all_equiv; intros.
apply /negP; rewrite -leqNgt; apply eq_leq, sym_eq, lenPFmax_alt; easy.
Qed.
Lemma lenPF1_in : ∀ {P : 'I_1 → Prop}, P ord0 → lenPF P = 1.
Proof.
intros; erewrite lenPF_ext; [apply lenPFmax | intros; rewrite I_1_is_unit; easy].
Qed.
Lemma lenPF1_out : ∀ {P : 'I_1 → Prop}, ¬ P ord0 → lenPF P = 0.
Proof.
intros; erewrite lenPF_ext; [apply lenPF0 | intros; rewrite I_1_is_unit; easy].
Qed.
Lemma lenPF_cast_ord :
∀ {n1 n2} (H : n1 = n2) (P1 : 'I_n1 → Prop),
lenPF P1 = lenPF (fun i2 ⇒ P1 (cast_ord (sym_eq H) i2)).
Proof.
intros; apply: lenPF_ext_gen; intros; rewrite cast_ord_comp cast_ord_id //.
Qed.
Lemma lenPF_ind_l_in :
∀ {n} {P : 'I_n.+1 → Prop},
P ord0 → lenPF P = 1 + lenPF (fun i ⇒ P (lift_S i)).
Proof.
intros [| n] P; [intros HP; rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
[apply /asboolP; easy | apply neqP, lift_S_not_first].
move=>> _ _; apply: lift_inj.
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; ∃ (lower_S Hi); rewrite lift_lower_S; easy.
Qed.
Lemma lenPF_ind_l_in_S :
∀ {n} {P : 'I_n.+1 → Prop},
P ord0 → lenPF P = (lenPF (fun i ⇒ P (lift_S i))).+1.
Proof. move=>> HP0; rewrite (lenPF_ind_l_in HP0); apply add1n. Qed.
Lemma lenPF_ind_l_out :
∀ {n} {P : 'I_n.+1 → Prop},
¬ P ord0 → lenPF P = lenPF (fun i ⇒ P (lift_S i)).
Proof.
intros [| n] P HP; [rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty);
[apply funS_correct; easy | move=>> _ _; apply: lift_inj |].
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; ∃ (lower_S Hi); rewrite lift_lower_S; easy.
Qed.
Lemma lenPF_ind_r_in :
∀ {n} {P : 'I_n.+1 → Prop},
P ord_max → lenPF P = lenPF (fun i ⇒ P (widen_S i)) + 1.
Proof.
intros [| n] P; [rewrite I_1_is_unit; intros HP;
rewrite (lenPF1_in HP) lenPF_nil add0n; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP) addnC; f_equal.
apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
[apply /asboolP; easy | apply neqP, widen_S_not_last].
move=>> _ _; apply: widen_ord_inj.
intros i; destruct (ord_eq_dec i ord_max) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; ∃ (narrow_S Hi); rewrite widen_narrow_S; easy.
Qed.
Lemma lenPF_ind_r_in_S :
∀ {n} {P : 'I_n.+1 → Prop},
P ord_max → lenPF P = (lenPF (fun i ⇒ P (widen_S i))).+1.
Proof. move=>> HP; rewrite (lenPF_ind_r_in HP); apply addn1. Qed.
Lemma lenPF_ind_r_in_S_alt :
∀ {n} {P : 'I_n.+1 → Prop},
P ord_max → lenPF (fun i ⇒ P (widen_S i)) < lenPF P.
Proof. intros; rewrite lenPF_ind_r_in_S; easy. Qed.
Lemma lenPF_ind_r_out :
∀ {n} {P : 'I_n.+1 → Prop},
¬ P ord_max → lenPF P = lenPF (fun i ⇒ P (widen_S i)).
Proof.
intros [| n] P HP; [rewrite I_1_is_unit in HP;
rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty);
[apply funS_correct; easy | move=>> _ _; apply widen_ord_inj |].
intros i; destruct (ord_eq_dec i ord_max) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; ∃ (narrow_S Hi); rewrite widen_narrow_S; easy.
Qed.
Lemma lenPF_skip_in :
∀ {n} {P : 'I_n.+1 → Prop} {i0},
P i0 → lenPF P = 1 + lenPF (fun i ⇒ P (skip_ord i0 i)).
Proof.
intros [| n] P i0; [rewrite I_1_is_unit; intros HP;
rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
move⇒ /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty).
apply funS_correct; intro; destruct (pselect _); [| easy].
intros _; apply /andP; split;
[apply /asboolP; easy | apply neqP, skip_ord_correct_m].
move=>> _ _; apply skip_ord_inj.
intros i; destruct (ord_eq_dec i i0) as [-> | Hi]; move⇒ /andP.
move⇒ [_ /negP Hi]; contradict Hi; easy.
move⇒ [HP' _]; ∃ (insert_ord Hi); rewrite skip_insert_ord; easy.
Qed.
Lemma lenPF_skip_out :
∀ {n} {P : 'I_n.+1 → Prop} {i0},
¬ P i0 → lenPF P = lenPF (fun i ⇒ P (skip_ord i0 i)).
Proof.
intros [| n] P i0 HP; [rewrite I_1_is_unit in HP;
rewrite (lenPF1_out HP) lenPF_nil; easy |].
apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty);
[apply funS_correct; easy | move=>> _ _; apply skip_ord_inj |].
intros i; destruct (ord_eq_dec i i0) as [-> | Hi].
rewrite ifF; [| destruct (pselect _)]; easy.
intros; ∃ (insert_ord Hi); rewrite skip_insert_ord; easy.
Qed.
Lemma unfilterP_filterP_ord :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) (j : 'I_(lenPF P)),
unfilterP_ord HP0 (filterP_ord j) = j.
Proof. intros; apply enum_valK_in. Qed.
Lemma filterP_unfilterP_ord_in :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) i,
P i → filterP_ord (unfilterP_ord HP0 i) = i.
Proof. intros; apply enum_rankK_in, in_asboolP; easy. Qed.
Lemma filterP_unfilterP_ord_in_equiv :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) {i} (HP : P i) j,
filterP_ord j = i ↔ j = unfilterP_ord HP0 i.
Proof.
intros; split; intros; subst.
rewrite unfilterP_filterP_ord; easy.
rewrite filterP_unfilterP_ord_in; easy.
Qed.
Lemma unfilterP_ord_out :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) i,
¬ P i → unfilterP_ord HP0 i = Ordinal (lenPF_n0_rev HP0).
Proof.
intros n P i0 HP0 i HP; apply val_inj;
unfold unfilterP_ord; rewrite enum_rank_in.unlock val_insubd; simpl.
rewrite ifF; [easy | rewrite memNindex].
unfold lenPF; rewrite cardE; apply ltnn.
rewrite mem_enum; apply /negP; contradict HP; apply /asboolP; easy.
Qed.
Lemma filterP_unfilterP_ord_out :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) i, ¬ P i →
filterP_ord (unfilterP_ord HP0 i) =
filterP_ord (Ordinal (lenPF_n0_rev HP0)).
Proof. intros; rewrite unfilterP_ord_out; easy. Qed.
Lemma unfilterP_ord_correct_in :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0) {i},
P i → ∃ j, i = filterP_ord j ∧ unfilterP_ord HP0 i = j.
Proof.
intros n P i0 HP0 i Hi; ∃ (unfilterP_ord HP0 i); split; [| easy].
rewrite filterP_unfilterP_ord_in; easy.
Qed.
Lemma filterP_ord_correct :
∀ {n} (P : 'I_n → Prop) (j : 'I_(lenPF P)), P (filterP_ord j).
Proof. intros n P j; generalize (enum_valP j); apply asboolW. Qed.
Lemma filterP_ord_incl_Rg :
∀ {n} (P : 'I_n → Prop), incl P (Rg (@filterP_ord _ P)).
Proof.
move=>> Hi; destruct (unfilterP_ord_correct_in Hi Hi) as [j [-> _]]; easy.
Qed.
Lemma filterP_ord_Rg_eq :
∀ {n} (P : 'I_n → Prop), Rg (@filterP_ord _ P) = P.
Proof.
intros; apply subset_ext_equiv; split; intro;
[intros [j _]; apply filterP_ord_correct | apply filterP_ord_incl_Rg].
Qed.
Lemma filterP_ord_inj :
∀ {n} (P : 'I_n → Prop),
injective (fun j : 'I_(lenPF P) ⇒ filterP_ord j).
Proof. intros; apply enum_val_inj. Qed.
Lemma unfilterP_ord_inj :
∀ {n} {P : 'I_n → Prop} {i0} (HP0 : P i0),
∀ i j, P i → P j →
unfilterP_ord HP0 i = unfilterP_ord HP0 j → i = j.
Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.
Lemma filterP_ord_incrF_S :
∀ {n} (P : 'I_n → Prop),
incrF_S (fun j : 'I_(lenPF P) ⇒ filterP_ord j).
Proof.
intros n P j Hj1.
apply /ltP; fold (ord_ltn (filterP_ord j) (filterP_ord (Ordinal Hj1))).
unfold filterP_ord, enum_val, enum_mem; rewrite -enumT; simpl.
move: (sorted_filter_enum_ord P) ⇒ /sorted_ordP H0.
assert (H1 : lenPF P = size (filter (fun i ⇒ asbool (P i)) (enum 'I_n))).
unfold lenPF; rewrite cardE; unfold enum_mem; do 2 f_equal.
rewrite filter_predT; easy.
pose (jj := cast_ord H1 j).
assert (Hjj1 : jj.+1 < size (filter (fun i ⇒ asbool (P i)) (enum 'I_n)))
by now unfold jj; simpl; rewrite -H1.
apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
Qed.
Lemma filterP_ord_incrF :
∀ {n} (P : 'I_n → Prop), incrF (fun j : 'I_(lenPF P) ⇒ filterP_ord j).
Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.
Lemma filterP_cast_ord_incrF :
∀ {m n} {P : 'I_n → Prop} (H : m = lenPF P),
incrF (filterP_ord \o (cast_ord H)).
Proof.
intros; apply incrF_comp; [apply cast_ord_incrF | apply filterP_ord_incrF].
Qed.
Lemma filterP_cast_ord_eq :
∀ {n m} {P : 'I_n → Prop} (H1 H2 : m = lenPF P) (j : 'I_m),
filterP_ord (cast_ord H1 j) = filterP_ord (cast_ord H2 j).
Proof.
intros [| n] m P H1 H2.
intros [j Hj]; exfalso; rewrite H1 lenPF_nil in Hj; easy.
intros; unfold filterP_ord; rewrite !(enum_val_nth ord0); easy.
Qed.
Lemma filterP_cast_ord_eq_alt :
∀ {n} {P Q : 'I_n → Prop} (H1 H2 : lenPF P = lenPF Q) (j : 'I_(lenPF P)),
filterP_ord (cast_ord H1 j) = filterP_ord (cast_ord H2 j).
Proof. intros; apply filterP_cast_ord_eq. Qed.
Lemma filterP_ord_ext_gen :
∀ {n1 n2} {Hn : n1 = n2} {P1 : 'I_n1 → Prop} {P2 : 'I_n2 → Prop}
(HP : ∀ i1, P1 i1 ↔ P2 (cast_ord Hn i1)) (j1 : 'I_(lenPF P1)),
filterP_ord j1 =
cast_ord (sym_eq Hn) (filterP_ord (cast_ord (lenPF_ext_gen Hn HP) j1)).
Proof.
intros n1 n2 Hn P1 P2 HP j1; subst; rewrite cast_ord_id; destruct n2 as [| n2].
exfalso; destruct j1 as [j1 Hj1]; rewrite lenPF_nil in Hj1; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0); repeat f_equal.
apply fun_ext; intro; f_equal; apply prop_ext.
rewrite HP cast_ord_id; easy.
Qed.
Lemma filterP_ord_ext :
∀ {n} {P Q : 'I_n → Prop}
(H : ∀ i, P i ↔ Q i) (j : 'I_(lenPF P)),
filterP_ord j = filterP_ord (cast_ord (lenPF_ext H) j).
Proof.
intros n P Q H j.
assert (H' : ∀ i, P i ↔ Q (cast_ord erefl i))
by now intros; rewrite cast_ord_id.
rewrite (filterP_ord_ext_gen H') cast_ord_id.
repeat f_equal; apply proof_irrel.
Qed.
Lemma filterP_cast_ord :
∀ {n1 n2} (H : n1 = n2) {P1 : 'I_n1 → Prop} {j1 : 'I_(lenPF P1)},
filterP_ord (cast_ord (lenPF_cast_ord H P1) j1) =
cast_ord H (filterP_ord j1).
Proof.
intros n1 n2 H P1 j1; subst.
assert (H' : ∀ i1, P1 i1 ↔ P1 (cast_ord erefl i1))
by now intros; rewrite cast_ord_id.
rewrite cast_ord_id (filterP_ord_ext H').
repeat f_equal; apply proof_irrel.
Qed.
Lemma filterP_ord_ind_l_in_0 :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord0) (j : 'I_(lenPF P)),
cast_ord (lenPF_ind_l_in HP) j = ord0 → filterP_ord j = ord0.
Proof.
intros n P HP j Hj; apply (@ord0_le_equiv n.+1).
pose (f := filterP_ord \o cast_ord (sym_eq (lenPF_ind_l_in HP))).
replace (filterP_ord _) with (f ord0);
[| unfold f; rewrite -Hj comp_correct cast_ordK; easy].
apply (incrF_cast_ord_0 (lenPF_ind_l_in HP) filterP_ord ord0);
[apply filterP_ord_incrF | rewrite filterP_ord_Rg_eq; easy].
Qed.
Lemma filterP_ord_ind_l_in_0_rev :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord0) (j : 'I_(lenPF P)),
filterP_ord j = ord0 → cast_ord (lenPF_ind_l_in HP) j = ord0.
Proof.
intros n P HP j Hj.
destruct (ord_eq_dec (cast_ord (lenPF_ind_l_in HP) j) ord0)
as [-> | Hj']; [easy | exfalso; move: Hj'].
move⇒ /(cast_ord_n0_gt_equiv (lenPF_n0_rev HP)) /filterP_ord_incrF.
rewrite Hj; easy.
Qed.
Lemma filterP_ord_ind_l_in_0_equiv :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord0) (j : 'I_(lenPF P)),
filterP_ord j = ord0 ↔ cast_ord (lenPF_ind_l_in HP) j = ord0.
Proof.
intros; split;
[apply filterP_ord_ind_l_in_0_rev | apply filterP_ord_ind_l_in_0].
Qed.
Lemma filterP_ord_ind_l_in_n0 :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord0)
(j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_l_in HP) j ≠ ord0),
filterP_ord j = lift_S (filterP_ord (lower_S Hj)).
Proof.
assert (H : ∀ {U1 U2 : Type} (f g : U1 → U2) x1, f = g → f x1 = g x1)
by move=>> → //.
intros n P HP j Hj.
replace (filterP_ord j) with
(filterP_ord (cast_ord (sym_eq (lenPF_ind_l_in HP)) (lift_S (lower_S Hj))))
by now rewrite !lift_lower_S cast_ordK.
rewrite -(comp_correct (cast_ord _)) -(comp_correct lift_S (_ \o _))
-(comp_correct filterP_ord).
apply H, fun_ext_incrF_Rg; clear j Hj.
apply incrF_comp; [apply lift_S_incrF | apply filterP_cast_ord_incrF].
apply incrF_comp; [apply filterP_ord_incrF | apply lift_S_incrF].
apply eq_trans with (fun i : 'I_n.+1 ⇒ i ≠ ord0 ∧ P i);
apply subset_ext_equiv; split; unfold comp.
intros i [j _]; split; [move: (lift_S_not_first j) | apply filterP_ord_correct].
rewrite -(filterP_ord_ind_l_in_0 _
(cast_ord (sym_eq (lenPF_ind_l_in HP)) ord0)); [| apply cast_ordKV].
rewrite -!(comp_correct _ filterP_ord); apply inj_contra.
apply inj_comp_compat; [apply cast_ord_inj | apply filterP_ord_inj].
intros i [Hi1 Hi2].
assert (Hj : cast_ord (lenPF_ind_l_in HP) (unfilterP_ord HP i) ≠ ord0).
contradict Hi1; rewrite -(filterP_unfilterP_ord_in HP _ Hi2).
apply (filterP_ord_ind_l_in_0 _ _ Hi1).
apply (Rg_correct (lower_S Hj));
rewrite lift_lower_S cast_ordK filterP_unfilterP_ord_in; easy.
intros i [Hi1 Hi2].
assert (HP' : P (lift_S (lower_S Hi1))) by now rewrite lift_lower_S.
apply (Rg_correct (unfilterP_ord HP' (lower_S Hi1)));
rewrite filterP_unfilterP_ord_in// lift_lower_S; easy.
intros i [j _]; split; [apply lift_S_not_first | apply filterP_ord_correct].
Qed.
Lemma filterP_ord_ind_l_out :
∀ {n} {P : 'I_n.+1 → Prop} (HP : ¬ P ord0) (j : 'I_(lenPF P)),
filterP_ord j = lift_S (filterP_ord (cast_ord (lenPF_ind_l_out HP) j)).
Proof.
intros [| n] P HP j.
exfalso; destruct j as [j Hj];
rewrite (lenPF_ind_l_out HP) lenPF_nil in Hj; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0).
unfold enum_val, enum_mem, mem; simpl; rewrite -!enumT enum_ordSl; simpl.
unfold in_mem; simpl; case_eq (asbool (P ord0)); intros HP'.
move: HP' ⇒ /(elimT (asboolP _)) //.
rewrite filter_map (nth_map ord0); unfold lift_S; f_equal.
destruct j as [j Hj]; simpl.
replace (size _) with (lenPF (fun i ⇒ P (lift ord0 i)));
try now rewrite -lenPF_ind_l_out.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
Qed.
Lemma filterP_ord_ind_r_in_max :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
cast_ord (lenPF_ind_r_in_S HP) j = ord_max → filterP_ord j = ord_max.
Proof.
intros n P HP j Hj; apply ord_max_ge_equiv.
pose (f := filterP_ord \o cast_ord (sym_eq (lenPF_ind_r_in_S HP))).
replace (filterP_ord _) with (f ord_max);
[| unfold f; rewrite -Hj comp_correct cast_ordK; easy].
apply (incrF_cast_ord_max (lenPF_ind_r_in_S HP) filterP_ord ord_max);
[apply filterP_ord_incrF | rewrite filterP_ord_Rg_eq; easy].
Qed.
Lemma filterP_ord_ind_r_in_max_rev :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
filterP_ord j = ord_max → cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
Proof.
intros n P HP j Hj.
destruct (ord_eq_dec (cast_ord (lenPF_ind_r_in_S HP) j) ord_max)
as [-> | Hj']; [easy | exfalso; move: Hj'].
move⇒ /cast_ord_nmax_lt_equiv.
replace (j < _)%coq_nat with
(j < cast_ord (sym_eq (lenPF_ind_r_in_S HP))
(Ordinal (ltnSn (lenPF (fun i ⇒ P (widen_S i))))))%coq_nat by easy.
move⇒ /filterP_ord_incrF; rewrite Hj filterP_ord_ind_r_in_max;
[apply ord_lt_irrefl | apply ord_inj; easy].
Qed.
Lemma filterP_ord_ind_r_in_max_equiv :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
filterP_ord j = ord_max ↔ cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
Proof.
intros; split;
[apply filterP_ord_ind_r_in_max_rev | apply filterP_ord_ind_r_in_max].
Qed.
Lemma filterP_ord_ind_r_in_nmax :
∀ {n} {P : 'I_n.+1 → Prop} (HP : P ord_max)
(j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_r_in_S HP) j ≠ ord_max),
filterP_ord j = widen_S (filterP_ord (narrow_S Hj)).
Proof.
intros [| n] P HP j Hj.
exfalso; destruct (leq_1_dec (lenPF_le P)) as [HP' | HP'].
clear Hj; destruct j as [j Hj]; rewrite HP' in Hj; easy.
contradict Hj; destruct j as [j Hj]; apply ord_inj; simpl.
rewrite HP' in Hj; rewrite lenPF_nil; apply lt_1; apply /ltP; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0) narrow_S_correct.
unfold enum_val, enum_mem, mem; simpl.
rewrite -!enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
case_eq (asbool (P ord_max)); intros HP'.
2: move: HP' ⇒ /(elimF (asboolP _)) //.
apply cast_ord_nmax_equiv in Hj; rewrite nth_rcons_l.
rewrite filter_map (nth_map ord0); unfold widen_S; f_equal.
destruct j as [j Hj1]; simpl in ×.
replace (size _) with (lenPF (fun i ⇒ P (widen_S i))).
rewrite lenPF_ind_r_in_S// in Hj1; apply ltnS_neq_ltn; easy.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
replace (size _) with (lenPF (fun i ⇒ P (widen_S i))); try easy.
clear j Hj; unfold lenPF; rewrite cardE; unfold enum_mem, mem; simpl.
rewrite !size_filter -!sumn_count -map_comp filter_predT; easy.
Qed.
Lemma filterP_ord_ind_r_out :
∀ {n} {P : 'I_n.+1 → Prop} (HP : ¬ P ord_max) (j : 'I_(lenPF P)),
filterP_ord j = widen_S (filterP_ord (cast_ord (lenPF_ind_r_out HP) j)).
Proof.
intros [| n] P HP j.
exfalso; destruct j as [j Hj].
rewrite (lenPF_ind_r_out HP) lenPF_nil in Hj; easy.
unfold filterP_ord; rewrite !(enum_val_nth ord0).
unfold enum_val, enum_mem, mem; simpl.
rewrite -!enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
case_eq (asbool (P ord_max)); intros HP'.
move: HP' ⇒ /(elimT (asboolP _)) //.
rewrite filter_map (nth_map ord0); unfold widen_S; f_equal.
destruct j as [j Hj]; simpl.
replace (size _) with (lenPF (fun i ⇒ P (widen_S i)));
try now rewrite -lenPF_ind_r_out.
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
Qed.
End FilterP_ord.