Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

change the notation for tnth from \_ to avoid a conflict with mca #110

Merged
merged 3 commits into from
Dec 8, 2023
Merged

change the notation for tnth from \_ to avoid a conflict with mca #110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2f9f5c6
modify the notation for tnth
t6s Dec 7, 2023
30bb2f3
!_
t6s Dec 8, 2023
c092788
remove unnecessary parentheses
t6s Dec 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions ecc_modern/ldpc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -820,7 +820,7 @@ Local Open Scope ring_scope.
Local Open Scope tuple_ext_scope.

Definition sumproduct_init : 'M[R]_(m, n) * 'M[R]_(m, n) :=
let init (x : 'F_2) := \matrix_(m0 < m, n0 < n) W `(y \_ n0 | x) in
let init (x : 'F_2) := \matrix_(m0 < m, n0 < n) W `(y !_ n0 | x) in
(init 0, init 1).

Definition alpha_fun (m0 : 'I_m) (n0 : 'I_n) (beta : 'M[R]_(m, n) * 'M[R]_(m, n))
Expand All @@ -830,7 +830,7 @@ Definition alpha_fun (m0 : 'I_m) (n0 : 'I_n) (beta : 'M[R]_(m, n) * 'M[R]_(m, n)
\prod_(n1 in 'V m0 :\ n0) if t ``_ n1 == Zp0 then beta.1 m0 n1 else beta.2 m0 n1)%R.

Definition beta_fun (m0 : 'I_m) (n0 : 'I_n) (x : 'F_2) (alpha : 'M[R]_(m, n)) : R :=
(W `(y \_ n0 | x) * \prod_(m1 in 'F n0 :\ m0) alpha m1 n0)%R.
(W `(y !_ n0 | x) * \prod_(m1 in 'F n0 :\ m0) alpha m1 n0)%R.

Fixpoint sumproduct_loop (lmax : nat) (beta0 beta1 : 'M_(m, n)) : option ('rV['F_2]_n) :=
match lmax with
Expand All @@ -847,7 +847,7 @@ Fixpoint sumproduct_loop (lmax : nat) (beta0 beta1 : 'M_(m, n)) : option ('rV['F
(K * beta_fun m0 n0 x alpha)%R in
let beta0 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 0 alpha0 in
let beta1 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 1 alpha1 in
let estimation x n0 alpha := (W x (y \_ n0) * \prod_(m1 in 'F n0) alpha m1 n0)%R in
let estimation x n0 alpha := (W x (y !_ n0) * \prod_(m1 in 'F n0) alpha m1 n0)%R in
let gamma0 n0 := estimation Zp0 n0 alpha0 in
let gamma1 n0 := estimation Zp1 n0 alpha1 in
let chat := \matrix_(i < 1, n0 < n) if (gamma0 n0 >= gamma1 n0)%mcR then 0 else 1 in
Expand Down
6 changes: 3 additions & 3 deletions ecc_modern/summary.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,9 +154,9 @@ Lemma summary_powersetE (s : {set 'I_n}) (d : 'rV['F_2]_n) (e : 'rV['F_2]_n -> R
Proof.
rewrite /summary_powerset.
transitivity (\sum_(f in {ffun 'I_n -> 'F_2} | freeon s (\row_i f i) d)
e (\row_(k0 < n) if k0 \in s then (fgraph f) \_ (cast_ord (esym (@card_ord n)) k0)
e (\row_(k0 < n) if k0 \in s then (fgraph f) !_ (cast_ord (esym (@card_ord n)) k0)
else d ``_ k0))%R.
rewrite (reindex_onto (fun p => [ffun x => p \_ (cast_ord (esym (@card_ord n)) x)])
rewrite (reindex_onto (fun p => [ffun x => p !_ (cast_ord (esym (@card_ord n)) x)])
(fun y => fgraph y)) /=; last first.
move=> /= f Hf.
apply/ffunP => /= k0.
Expand Down Expand Up @@ -188,7 +188,7 @@ transitivity (\sum_(f in {ffun 'I_n -> 'F_2} | freeon s (\row_i f i) d)
by rewrite /row_of_tuple mxE tcastE.
transitivity (\sum_(f in {ffun 'I_n -> bool} | freeon s d (\row_i F2_of_bool (f i)))
e (\row_k0 (if k0 \in s
then F2_of_bool ((fgraph f) \_ (cast_ord (esym (card_ord n)) k0))
then F2_of_bool ((fgraph f) !_ (cast_ord (esym (card_ord n)) k0))
else d ``_ k0)))%R.
rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [ffun x => F2_of_bool (f x)])
(fun f : {ffun 'I_n -> 'F_2} => [ffun x => bool_of_F2 (f x)])); last first.
Expand Down
30 changes: 15 additions & 15 deletions information_theory/channel_coding_direct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,10 +286,10 @@ Qed.

(* TODO: move? *)
Lemma rsum_rmul_tuple_pmf_tnth {C : finType} n k (Q : {fdist C}) :
\sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t \_ m = 1.
\sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t !_ m = 1.
Proof.
transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) Q `^ _ (j m)).
rewrite (reindex_onto (fun p => [ffun x => p\_(enum_rank x)])
rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)])
(fun x => fgraph x)) //=; last first.
by move=> f _; apply/ffunP => /= i; rewrite ffunE tnth_fgraph enum_rankK.
rewrite (big_tcast (esym (card_ord k))) esymK.
Expand Down Expand Up @@ -350,7 +350,7 @@ transitivity (\sum_(v : 'rV[A]_n)
(\sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0])
(W ``(| v)) y) *
\sum_(j in {: #|M|.-1.-tuple ('rV[A]_n)})
(\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) \_ (enum_rank m)))).
(\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) !_ (enum_rank m)))).
rewrite (reindex_onto (fun y : {ffun _ -> 'rV__} => \row_(i < _) y (enum_val i))
(fun p : 'rV_ _ => [ffun x => p ``_ (enum_rank x)])) //=; last first.
move=> v _; by apply/rowP => i; rewrite mxE ffunE enum_valK.
Expand All @@ -371,7 +371,7 @@ transitivity (\sum_(v : 'rV[A]_n)
(\sum_(y in ~: [set y0 | prod_rV (yn, y0) \in `JTS P W n epsilon0])
W ``(y | yn))) (\row_(i < n) a) ord0)%R.
transitivity (\sum_(j : _)
(\prod_(m : M) P `^ n ((tcast M_prednK j) \_ (enum_rank m))) *
(\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) *
(\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in
`JTS P W n epsilon0])
W ``(y | nth (\row_(i < n) a) j 0))).
Expand All @@ -384,19 +384,19 @@ transitivity (\sum_(v : 'rV[A]_n)
by rewrite tcastE /= cast_ord_id.
apply eq_big => m; by rewrite !inE H.
rewrite -(@big_tuple_cons_behead _ #|M|.-1
(fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) \_ (enum_rank m))) *
(fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) *
(\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in
`JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0)))) xpredT xpredT).
apply eq_bigr => ta _ /=; by rewrite -big_distrl /= mulRC.
transitivity ((\sum_(ta in 'rV[A]_n) P `^ _ ta *
(\sum_(y in ~: [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0])
(W ``(| ta ) ) y)) *
\sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j \_ m)))%R.
\sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j !_ m)))%R.
rewrite big_distrl /=.
apply eq_bigr => ta _.
rewrite -mulRA mulRCA; congr Rmult.
transitivity (\sum_(j in {: #|'I_k|.-tuple ('rV[A]_n) })
P `^ _ ta * \prod_(m < k) P `^ _ (j \_ (enum_rank m)))%R.
P `^ _ ta * \prod_(m < k) P `^ _ (j !_ (enum_rank m)))%R.
have k_prednK : #|'I_k.+1|.-1 = #|'I_k| by rewrite !card_ord.
rewrite (big_tcast (esym k_prednK)) esymK.
apply eq_bigr => i0 Hi0.
Expand Down Expand Up @@ -486,22 +486,22 @@ transitivity (
\sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)})
\sum_(j0 in 'rV[A]_n)
\sum_(ji in 'rV[A]_n)
Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])\_x] *
Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] *
\sum_(y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0])
(W ``(| j0)) y)%R.
transitivity (
\sum_(j0 in 'rV[A]_n)
\sum_(j1 in {: i.-1.-tuple ('rV[A]_n)})
\sum_(ji in 'rV[A]_n)
\sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)})
Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])\_x] *
Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] *
\sum_( y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0])
(W ``(| j0) ) y)%R.
rewrite (reindex_onto (fun p => [ffun x => p\_(enum_rank x)]) (fun y => fgraph y)) /=; last first.
rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun y => fgraph y)) /=; last first.
move=> f _; apply/ffunP => m; by rewrite ffunE tnth_fgraph enum_rankK.
transitivity ( \sum_(j : _)
(Wght.d P [ffun x => j\_(enum_rank x)] *
Pr (W ``(| [ffun x => j\_(enum_rank x)] ord0)) (E_F_N [ffun x => j\_(enum_rank x)] i)))%R.
(Wght.d P [ffun x => j!_(enum_rank x)] *
Pr (W ``(| [ffun x => j!_(enum_rank x)] ord0)) (E_F_N [ffun x => j!_(enum_rank x)] i)))%R.
apply eq_big => //= x; apply/eqP/eq_from_tnth => j.
by rewrite tnth_fgraph ffunE enum_valK.
rewrite (big_tcast (card_ord k.+1)).
Expand All @@ -524,14 +524,14 @@ transitivity (
rewrite (reindex_onto enum_rank enum_val); last by move=> *; rewrite enum_valK.
apply eq_big => /=; first by move=> x; rewrite enum_rankK eqxx inE.
move=> i4 _; congr (P `^ _ _).
rewrite !ffunE; congr (_ \_ _).
rewrite !ffunE; congr (_ !_ _).
apply/val_inj => /=.
rewrite [LHS]eq_tcast /= !eq_tcast /= [RHS]eq_tcast eq_tcast /=; congr (_ :: _ ++ _ :: _).
by rewrite eq_tcast.
- apply eq_big.
+ move=> x /=.
rewrite !inE ffunE.
rewrite (_ : (_ \_ _) = i2) //=.
rewrite (_ : (_ !_ _) = i2) //=.
rewrite enum_rank_ord /= tcastE !cast_ord_comp (tnth_nth i0) /=.
rewrite eq_tcast /=.
rewrite -cat_cons nth_cat /= size_tuple prednK ?lt0n // ltnn subnn.
Expand Down Expand Up @@ -571,7 +571,7 @@ transitivity (
by rewrite big_cat /= mulRC.
rewrite [in RHS](big_nth j0) /= big_mkord.
transitivity (\prod_(j < #|@predT M|)
P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])\_(enum_rank x)] (enum_val j)))%R.
P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])!_(enum_rank x)] (enum_val j)))%R.
rewrite ffunE; apply eq_big => ? //= _.
by rewrite !ffunE enum_valK.
have j_M : (size (j1 ++ j3 :: j2)).+1 = #|M|.
Expand Down
4 changes: 2 additions & 2 deletions information_theory/jtypes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -553,7 +553,7 @@ rewrite size_drop size_take size_tuple -/(minn (sum_num_occ ta k.+1) n) minn_sum
rewrite nth_drop nth_take => //.
have Hsumk : sum_num_occ ta k + i < n by apply (leq_trans Hi (sum_num_occ_leq_n ta k.+1)).
transitivity (enum_val k).
transitivity (ta\_(Ordinal Hsumk)).
transitivity (ta!_(Ordinal Hsumk)).
by rewrite [in X in _ = X](tnth_nth (enum_val k)).
apply sum_num_occ_enum_val => //=; by rewrite Hi andbT leq_addr.
rewrite -ltn_subRL (sum_num_occ_sub ta k) in Hi.
Expand All @@ -574,7 +574,7 @@ rewrite drop_take_iota; last by rewrite sum_num_occ_inc_loc sum_num_occ_leq_n.
apply eq_in_filter => /= i.
rewrite mem_iota leq0n add0n /= => Hi.
rewrite nth_zip /=; last by rewrite 2!size_tuple.
transitivity (ta\_(Ordinal Hi) == a); by [rewrite -sum_num_occ_is_enum_val | rewrite (tnth_nth a)].
transitivity (ta!_(Ordinal Hi) == a); by [rewrite -sum_num_occ_is_enum_val | rewrite (tnth_nth a)].
Qed.

Local Close Scope tuple_ext_scope.
Expand Down
12 changes: 6 additions & 6 deletions lib/hamming.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -567,7 +567,7 @@ Variable n : nat.

Local Open Scope tuple_ext_scope.
Lemma card_dH (x y : n.-tuple 'F_2) :
(#| [pred i | y \_ i != x \_ i ] |)%N = dH (row_of_tuple x) (row_of_tuple y).
(#| [pred i | y !_ i != x !_ i ] |)%N = dH (row_of_tuple x) (row_of_tuple y).
Proof.
rewrite /dH wH_num_occ num_occ_alt /=.
apply eq_card => /= i.
Expand Down Expand Up @@ -691,7 +691,7 @@ case/(_ erefl) => i [] [] H1 H2 H3.
exists (Ordinal H1); split.
transitivity (F2_of_bool true) => //.
rewrite -H2 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
rewrite (_ : _ _ _ i = (tuple_of_row x) \_ (Ordinal H1)); last first.
rewrite (_ : _ _ _ i = (tuple_of_row x) !_ (Ordinal H1)); last first.
apply set_nth_default; by rewrite size_tuple.
rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H1))); by case: (x ``_ _ != 0%R).
move=> j Hj.
Expand All @@ -701,7 +701,7 @@ rewrite -(H3 j) //; last first.
by apply/Hj/val_inj.
rewrite /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
suff -> : x ``_ j = nth ord0 (tuple_of_row x) j by apply: F2_0_1.
rewrite (_ : _ _ _ j = (tuple_of_row x) \_ j); last by rewrite tnth_mktuple.
rewrite (_ : _ _ _ j = (tuple_of_row x) !_ j); last by rewrite tnth_mktuple.
exact: tnth_nth.
Qed.

Expand Down Expand Up @@ -759,13 +759,13 @@ exists (Ordinal H1), (Ordinal H3); split.
split.
transitivity (F2_of_bool true) => //.
rewrite -H2 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
rewrite (_ : _ _ _ i = (tuple_of_row x) \_ (Ordinal H1)); last first.
rewrite (_ : _ _ _ i = (tuple_of_row x) !_ (Ordinal H1)); last first.
apply set_nth_default; by rewrite size_tuple.
rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H1))); by case: (x ``_ _ != 0%R).
split.
transitivity (F2_of_bool true) => //.
rewrite -H4 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
rewrite (_ : _ _ _ k = (tuple_of_row x) \_ (Ordinal H3)); last first.
rewrite (_ : _ _ _ k = (tuple_of_row x) !_ (Ordinal H3)); last first.
apply set_nth_default; by rewrite size_tuple.
rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H3))); by case: (x ``_ _ != 0%R).
move=> j ij kj.
Expand All @@ -777,7 +777,7 @@ rewrite -(H6 j) //; last first.
by apply/ij/val_inj.
rewrite /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
suff -> : x ``_ j = nth ord0 (tuple_of_row x) j by apply: F2_0_1.
rewrite (_ : _ _ _ j = (tuple_of_row x) \_ j); last by rewrite tnth_mktuple.
rewrite (_ : _ _ _ j = (tuple_of_row x) !_ j); last by rewrite tnth_mktuple.
exact: tnth_nth.
Qed.

Expand Down
42 changes: 21 additions & 21 deletions lib/num_occ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ Proof. by rewrite /num_occ -[X in _ <= X](size_tuple t) count_size. Qed.

Variables (A : finType) (n : nat) (a : A) (t : n.-tuple A).

Definition set_occ := [set i | t \_ i == a].
Definition set_occ := [set i | t !_ i == a].

Lemma num_occ_alt : N(a | t) = #| set_occ |.
Proof.
Expand Down Expand Up @@ -227,7 +227,7 @@ Section num_co_occ_tuple.

Variables (A B : finType) (n : nat) (a : A) (b : B) (ta : n.-tuple A) (tb : n.-tuple B).

Definition set_co_occ := [set i | (ta \_ i == a) && (tb \_ i == b)].
Definition set_co_occ := [set i | (ta !_ i == a) && (tb !_ i == b)].

Lemma num_co_occ_leq_n : N(a, b | ta, tb) <= n.
Proof. rewrite /num_co_occ ; by apply num_occ_leq_n. Qed.
Expand Down Expand Up @@ -267,7 +267,7 @@ rewrite cover_imset.
apply/bigcupP.
case : ifP; last by move=> /negP H1 H ; move: H1; apply/negP; case H => {H} y0 ; rewrite 3!in_set => _ /andP [].
rewrite in_set => /eqP Hi.
exists (tb\_i) ; last by rewrite in_set Hi eqxx andTb.
exists (tb!_i) ; last by rewrite in_set Hi eqxx andTb.
rewrite in_set; apply/andP; split => //.
apply/existsP; exists i; by rewrite in_set Hi eqxx andTb.
Qed.
Expand Down Expand Up @@ -452,7 +452,7 @@ apply/andP; split; by [rewrite addnS ltnS leq_addr | rewrite ltn_add2r].
Qed.

Lemma sum_num_occ_enum_val (k : 'I_#|A|) (l : 'I_n) :
sum_num_occ k <= l < sum_num_occ k.+1 -> ta\_l = enum_val k.
sum_num_occ k <= l < sum_num_occ k.+1 -> ta!_l = enum_val k.
Proof.
move: (ltnSn k).
set k':= {2}k.+1.
Expand All @@ -464,22 +464,22 @@ have : m = k by apply/eqP; rewrite eqn_leq; apply/andP.
rewrite {Hcase} => ?; subst m.
case/andP => [Hlm1 Hlm2].
apply/eqP/negPn/negP; move=> abs.
case/boolP : (lt_rank ta\_l (enum_val k)) => Hcase.
- have Hrank : enum_rank ta\_l < k by rewrite lt_rank_alt enum_valK in Hcase.
have Hcontr : #|[set i | (i==l) || (sum_num_occ (enum_rank ta\_l)<= i < sum_num_occ (enum_rank ta\_l).+1)]| <= N(ta\_l|ta).
case/boolP : (lt_rank ta!_l (enum_val k)) => Hcase.
- have Hrank : enum_rank ta!_l < k by rewrite lt_rank_alt enum_valK in Hcase.
have Hcontr : #|[set i | (i==l) || (sum_num_occ (enum_rank ta!_l)<= i < sum_num_occ (enum_rank ta!_l).+1)]| <= N(ta!_l|ta).
rewrite num_occ_alt subset_leq_card // subsetE; apply/pred0P => i /=.
rewrite !in_set /=.
apply/negbTE; rewrite negb_and.
case/boolP : (ta\_i == ta\_l) => ta_il //.
case/boolP : (ta!_i == ta!_l) => ta_il //.
rewrite negb_or; apply/andP; split.
- move: ta_il; apply contra => /eqP ->; by rewrite eqxx.
- move: ta_il; apply contra => ta_il.
apply/eqP; rewrite -(enum_rankK (ta\_l)); by apply IH.
rewrite (_ : #|[set i | (i == l) || (sum_num_occ (enum_rank ta\_l) <= i < sum_num_occ (enum_rank ta\_l).+1)]| = N(ta\_l | ta).+1) in Hcontr; first by rewrite ltnn in Hcontr.
apply/eqP; rewrite -(enum_rankK (ta!_l)); by apply IH.
rewrite (_ : #|[set i | (i == l) || (sum_num_occ (enum_rank ta!_l) <= i < sum_num_occ (enum_rank ta!_l).+1)]| = N(ta!_l | ta).+1) in Hcontr; first by rewrite ltnn in Hcontr.
symmetry; rewrite -addn1 sum_num_occ_rec -sum1_card.
rewrite (bigD1 l) /=; last by rewrite in_set; apply/orP; apply or_introl.
rewrite addnC; apply/eqP; rewrite eqn_add2l; apply/eqP.
transitivity (\sum_(i in [set i0 : 'I_n | nat_of_ord i0 \in iota (sum_num_occ (enum_rank ta\_l)) N(enum_val (enum_rank ta\_l) | ta)]) 1); last first.
transitivity (\sum_(i in [set i0 : 'I_n | nat_of_ord i0 \in iota (sum_num_occ (enum_rank ta!_l)) N(enum_val (enum_rank ta!_l) | ta)]) 1); last first.
apply eq_bigl => i; rewrite !in_set.
case/boolP : (i != l) => Hcase2.
- rewrite mem_iota.
Expand All @@ -489,18 +489,18 @@ case/boolP : (lt_rank ta\_l (enum_val k)) => Hcase.
apply/negP; case/andP => H1.
rewrite -sum_num_occ_rec; apply/negP; rewrite -leqNgt.
by rewrite (leq_trans _ Hlm1) // sum_num_occ_inc.
by rewrite sum1_card set_predleq_size enum_rankK // -{2}(enum_rankK ta\_l) -sum_num_occ_rec sum_num_occ_leq_n.
- have {abs} {}Hcase : lt_rank (enum_val k) ta\_l.
by rewrite sum1_card set_predleq_size enum_rankK // -{2}(enum_rankK ta!_l) -sum_num_occ_rec sum_num_occ_leq_n.
- have {abs} {}Hcase : lt_rank (enum_val k) ta!_l.
rewrite lt_rank_alt; rewrite lt_rank_alt -leqNgt in Hcase.
rewrite ltn_neqAle; apply/andP; split => //.
rewrite enum_valK.
suff : k != enum_rank ta\_l by move=> ->.
suff : k != enum_rank ta!_l by move=> ->.
apply/negP ; move/eqP.
move=> abs2; symmetry in abs2; rewrite -abs2 enum_rankK {abs2} in abs.
contradict abs ; by apply/negP/negPn/eqP.
move/negP : (ltnn N(enum_val k | ta)) => abs; contradict abs.
rewrite {1}num_occ_alt.
have H : #|[set i | ta\_i == enum_val k]| <= #|[set i : 'I_n | (sum_num_occ k <= i < l)]|.
have H : #|[set i | ta!_i == enum_val k]| <= #|[set i : 'I_n | (sum_num_occ k <= i < l)]|.
apply subset_leq_card.
rewrite subsetE; apply/pred0P => i /=.
rewrite !in_set /=.
Expand All @@ -517,7 +517,7 @@ case/boolP : (lt_rank ta\_l (enum_val k)) => Hcase.
have lt0m : 0 < k.
rewrite ltnNge leqn0 ; apply/eqP => abs2.
contradict Hcase2 ; by rewrite abs2 sum_num_occ_0 ltn0.
have H2 : forall (k' : 'I_#|A|) (l : 'I_n), k'.-1 < k -> l < sum_num_occ k' -> lt_rank ta\_l (enum_val k'). (* nested induction *)
have H2 : forall (k' : 'I_#|A|) (l : 'I_n), k'.-1 < k -> l < sum_num_occ k' -> lt_rank ta!_l (enum_val k'). (* nested induction *)
case; elim.
- move=> H0 l0 /= _ abs2 ; contradict abs2 ; by rewrite sum_num_occ_0 ltn0.
- move=> k' HR' HSk l0 /= k'k Hl0.
Expand All @@ -539,18 +539,18 @@ case/boolP : (lt_rank ta\_l (enum_val k)) => Hcase.
Qed.

Lemma enum_val_sum_num_occ (k : 'I_#|A|) (l : 'I_n) :
ta\_l = enum_val k -> sum_num_occ k <= l < sum_num_occ k.+1.
ta!_l = enum_val k -> sum_num_occ k <= l < sum_num_occ k.+1.
Proof.
move=> Hkl; apply/negP => /negP abs.
have : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| <= N(ta\_l | ta).
have : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| <= N(ta!_l | ta).
rewrite num_occ_alt subset_leq_card // subsetE.
apply/pred0P => /= i /=; rewrite !in_set /=.
case/boolP : (ta\_i == ta\_l) => ta_il //=.
case/boolP : (ta!_i == ta!_l) => ta_il //=.
apply/negbTE; rewrite negb_or; apply/andP; split.
- move: ta_il; apply: contra => /eqP ?; subst l; by rewrite eqxx.
- move: ta_il; apply: contra => Hsum_num_occ.
apply/eqP; rewrite Hkl; by apply sum_num_occ_enum_val.
suff -> : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| = N(ta\_l | ta).+1.
suff -> : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| = N(ta!_l | ta).+1.
by rewrite ltnn.
symmetry; rewrite -addn1 sum_num_occ_rec -sum1_card.
rewrite (bigD1 l) /=; last by rewrite in_set; apply/orP; apply or_introl.
Expand All @@ -567,7 +567,7 @@ case/boolP : (i != l) => [/negPf |] il.
Qed.

Lemma sum_num_occ_is_enum_val (k : 'I_#|A|) (l : 'I_n) :
sum_num_occ k <= l < sum_num_occ k.+1 = (ta\_l == enum_val k).
sum_num_occ k <= l < sum_num_occ k.+1 = (ta!_l == enum_val k).
Proof.
case/boolP : (sum_num_occ k <= l < sum_num_occ k.+1) => Hcase.
- exact/esym/eqP/sum_num_occ_enum_val.
Expand Down
Loading
Loading