Skip to content

Commit

Permalink
Exp cleaning (wip)
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jan 31, 2025
1 parent ff89725 commit c543060
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 47 deletions.
20 changes: 8 additions & 12 deletions ecc_classic/bch.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,7 @@ Unset Printing Implicit Defensive.

Import GRing.Theory.
Local Open Scope ring_scope.

Local Open Scope vec_ext_scope.

Local Open Scope dft_scope.

Module BCH.
Expand Down Expand Up @@ -140,15 +138,14 @@ apply/idP/idP.
apply BCH_PCM_altP1 => i.
move/eqP/rowP : H => /(_ i).
rewrite !mxE => H; rewrite -[RHS]H.
apply eq_bigr => /= k _; by rewrite !mxE /= mulrC.
by apply eq_bigr => /= k _; rewrite !mxE /= mulrC.
- rewrite /BCH.PCM_alt /BCH.PCM /syndrome => H.
apply/eqP/rowP => i.
have @j : 'I_t.*2.
refine (@Ordinal _ i.*2 _); by rewrite -!muln2 ltn_pmul2r.
move/eqP : H => /matrixP/(_ ord0 j).
rewrite !mxE => {2}<-.
apply eq_bigr => k _.
by rewrite !mxE.
by apply eq_bigr => k _; rewrite !mxE.
Qed.

End BCH_PCM_alt.
Expand Down Expand Up @@ -206,7 +203,7 @@ Lemma BCH_syndromep_is_GRS_syndromep y :
GRS.syndromep (rVexp a n) (rVexp a n) t.*2 (F2_to_GF2 m y).
Proof.
apply/polyP => i.
rewrite !coef_poly; case: ifPn => // it; by rewrite fdcoor_syndrome_coord.
by rewrite !coef_poly; case: ifPn => // it; rewrite fdcoor_syndrome_coord.
Qed.

End BCH_is_GRS.
Expand Down Expand Up @@ -252,7 +249,7 @@ apply/idP/idP.
rewrite -(@ltn_pmul2r 2) // !muln2 -(ltn_add2r 1) !addn1.
move/leq_trans; apply.
move: tn.
rewrite -divn2 leq_divRL // muln2 => /leq_ltn_trans; exact.
by rewrite -divn2 leq_divRL // muln2 => /leq_ltn_trans; exact.
Qed.

End BCH_PCM_checksum.
Expand Down Expand Up @@ -328,7 +325,7 @@ transitivity (\det (\matrix_(i, j) (h i j * g j))).
apply/matrixP => i j.
by rewrite !mxE /h /g /BCH.PCM_alt !mxE -!exprD /= -exprM mul1n addn1.
rewrite det_mlinear; congr (_ * _).
congr (\det _); apply/matrixP => i j; by rewrite !mxE /h -exprM.
by congr (\det _); apply/matrixP => i j; rewrite !mxE /h -exprM.
Qed.

Hypothesis a_neq0 : distinct_non_zero a.
Expand Down Expand Up @@ -419,7 +416,7 @@ have {}Hf : \sum_(i < r'.+1) GF2_of_F2 x ``_ (f i) *:
move/colP : Hf => /(_ (widen_ord (ltnW Hr') j)).
rewrite !mxE summxE => Hf.
rewrite -[RHS]Hf.
apply eq_bigr => /= i _; by rewrite !mxE.
by apply eq_bigr => /= i _; rewrite !mxE.
have /negP := det_B_neq0 Hr' Hinj.
rewrite -det_tr; apply.
apply/det0P; exists (\row_i GF2_of_F2 x ``_ (f i)).
Expand All @@ -437,13 +434,12 @@ apply/det0P; exists (\row_i GF2_of_F2 x ``_ (f i)).
apply/rowP => i; rewrite !mxE.
move/colP : Hf => /(_ i).
rewrite !mxE => Hf; rewrite -[RHS]Hf.
rewrite summxE; apply eq_bigr=> k _; by rewrite !mxE.
by rewrite summxE; apply eq_bigr=> k _; rewrite !mxE.
Qed.

End BCH_minimum_distance_lb.

Section BCH_erreval.

Variables (F : fieldType) (n : nat) (a : 'rV[F]_n).

Definition BCH_erreval := erreval (const_mx 1) a.
Expand Down Expand Up @@ -676,7 +672,7 @@ have [M HM] : exists M, `[ 'X * rVpoly x' ]_ n = 'X * rVpoly x' + M * ('X^n - 1)
rewrite HM /fdcoor poly_rV_K //; last first.
rewrite -HM.
move: (ltn_modp ('X * rVpoly x') ('X^n - 1)).
rewrite size_Xn_sub_1 // ltnS => ->.
rewrite size_XnsubC // ltnS => ->.
by rewrite monic_neq0 // monic_Xn_sub_1.
rewrite !(hornerE,hornerXn(*TODO(rei): not necessary since mc1.16.0*)).
move: (Hx i); rewrite /fdcoor => /eqP ->; rewrite mulr0 add0r.
Expand Down
10 changes: 4 additions & 6 deletions information_theory/channel_coding_converse.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,9 @@ Section channel_coding_converse_intermediate_lemma.
Let R := Rdefinitions.R.
Variables (A B : finType) (W : `Ch*(A, B)).
Variable minRate : R.
Hypothesis HminRate : (minRate > capacity W)%R.
Hypothesis HminRate : minRate > capacity W.
Hypothesis set_of_I_has_ubound :
classical_sets.has_ubound (fun y => exists P, `I(P, W) = y).
classical_sets.has_ubound (fun y => exists P, `I(P, W) = y)(*TODO*).

Let Anot0 : (0 < #|A|)%nat. Proof. by case: W. Qed.

Expand Down Expand Up @@ -149,7 +149,7 @@ rewrite expr_div_n -mulrA ler_wpM2l//.
by rewrite mulr_gt0// ?exp.ln_gt0 ?ltr1n// mulr_gt0//.
rewrite /exp.powR(* TODO *) pnatr_eq0/=.
apply/ltW.
apply: (le_lt_trans _ (exp_strict_lb (K.+1) nDeltaln2)) => {nDeltaln2}.
apply: (le_lt_trans _ (exp_strict_lb K.+1 nDeltaln2)) => {nDeltaln2}.
apply/eqW.
rewrite invfM invrK.
rewrite /aux.
Expand All @@ -159,9 +159,7 @@ rewrite expr_div_n -mulrA ler_wpM2l//.
rewrite invrK.
rewrite mulrCA.
rewrite invrK -exprSr.
rewrite -exprMn_comm//; last first.
rewrite /GRing.comm.
by rewrite [in RHS]mulrC.
rewrite -exprMn_comm//; last by rewrite /GRing.comm [in RHS]mulrC.
by rewrite mulrC mulrA.
Qed.

Expand Down
2 changes: 1 addition & 1 deletion information_theory/shannon_fano.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ have Pi0 : 0 < P i by rewrite lt0r Pr0/=.
apply (@le_trans _ _ (#|T|%:R `^ (- Log #|T|%:R (P i)^-1))%R); last first.
by rewrite LogV// opprK natn LogK// card_ord.
rewrite pow_Exp; last by rewrite card_ord.
rewrite Exp_oppr card_ord lef_pV2// ?posrE ?Exp_gt0//.
rewrite powRN card_ord lef_pV2// ?posrE ?Exp_gt0//.
rewrite Exp_le_increasing// ?ltr1n//.
rewrite (le_trans (mathcomp_extra.ceil_ge _))//.
by rewrite natr_absz// ler_int ler_norm.
Expand Down
35 changes: 11 additions & 24 deletions information_theory/types.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,13 @@ Import GRing.Theory Num.Theory.

Local Open Scope entropy_scope.
Local Open Scope num_occ_scope.
(*Local Open Scope R_scope.*)
Local Open Scope ring_scope.
Local Open Scope fdist_scope.

Module type.

Section type_def.

Variable A : finType.
Variable n : nat.
Variables (A : finType) (n : nat).

Record type : predArgType := mkType {
d :> {fdist A} ;
Expand Down Expand Up @@ -379,19 +376,6 @@ Qed.

End typed_tuples_facts.

(* TODO: move *)
Lemma Exp2_pow (r : Rdefinitions.R) n k :
(r `^ (k%:R * n) = (r `^ n) ^+ k)%R.
Proof. by rewrite -powR_mulrn ?powR_ge0// mulrC powRrM. Qed.

(* TODO: move *)
Lemma morph_exp2_plus : {morph (fun x => (2%:R:Rdefinitions.R) `^ x)%R : x y / x + y >-> x * y}.
Proof. by move=> ? ? /=; rewrite powRD// pnatr_eq0// implybT. Qed.

(* TODO: rm *)
Lemma exp2_Ropp x : ((2%:R:Rdefinitions.R) `^ (- x) = ((2%:R:Rdefinitions.R) `^ x)^-1)%R.
Proof. by rewrite powRN. Qed.

Section typed_tuples_facts_continued.
Variables (A : finType) (n : nat).
Hypothesis Hn : n != O.
Expand Down Expand Up @@ -485,7 +469,7 @@ Qed.

Lemma card_typed_tuples : (#| T_{ P } |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `H P))%R.
Proof.
rewrite -(@invrK _ ((2%:R:Rdefinitions.R) `^ (n%:R * `H P))%R) -exp2_Ropp -mulNr.
rewrite -(@invrK _ ((2%:R:Rdefinitions.R) `^ (n%:R * `H P))%R) -powRN -mulNr.
set aux := - n%:R * `H P.
rewrite -div1r ler_pdivlMr // {}/aux ?Exp_gt0//.
case/boolP : [exists x, x \in T_{P}] => x_T_P.
Expand Down Expand Up @@ -636,12 +620,13 @@ by rewrite eqr_nat => /eqP.
Qed.

Lemma sum_messages_types f :
\sum_(P : P_ n ( A )) (\sum_(m |m \in enc_pre_img c P) f m) = \sum_ (m : M) (f m) :> Rdefinitions.R.
\sum_(P : P_ n ( A )) (\sum_(m |m \in enc_pre_img c P) f m)
= \sum_ (m : M) (f m) :> Rdefinitions.R.
Proof.
transitivity (\sum_ (m in [set: M]) (f m)); last by apply eq_bigl => b; rewrite in_set.
transitivity (\sum_ (m in [set: M]) (f m)); last first.
by apply: eq_bigl => b; rewrite in_set.
rewrite -(cover_enc_pre_img c) /enc_pre_img_partition sum_messages_types'.
symmetry.
by apply big_trivIset, trivIset_enc_pre_img.
exact/esym/big_trivIset/trivIset_enc_pre_img.
Qed.

End sum_messages_types.
Expand All @@ -668,9 +653,11 @@ Definition Hdef := proj2_sig (typed_tuples_not_empty P).
Definition tcode_untyped_code := mkCode
[ffun m => if tuple_of_row (enc c m) \in T_{P} then enc c m else def] (dec c).

Lemma tcode_typed_prop (m : M) : tuple_of_row ((enc tcode_untyped_code) m) \in T_{P}.
Lemma tcode_typed_prop (m : M) :
tuple_of_row ((enc tcode_untyped_code) m) \in T_{P}.
Proof.
rewrite /= ffunE; case: ifP => [//| _]; rewrite /def row_of_tupleK; exact Hdef.
rewrite /= ffunE; case: ifP => [//| _]; rewrite /def row_of_tupleK.
exact Hdef.
Qed.

Definition tcode : typed_code B M P := mkTypedCode tcode_typed_prop.
Expand Down
12 changes: 8 additions & 4 deletions lib/realType_logb.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,10 @@ Implicit Type x : R.
Lemma pow_Exp (x : R) n : (0 <= x) -> x ^+ n = x `^ n%:R.
Proof. by move=> x0; rewrite powR_mulrn. Qed.

(* TODO: rename *)
Lemma Exp2_pow x n k : x `^ (k%:R * n) = (x `^ n) ^+ k.
Proof. by rewrite -powR_mulrn ?powR_ge0// mulrC powRrM. Qed.

Lemma LogK n x : (1 < n)%N -> 0 < x -> n%:R `^ (Log n x) = x.
Proof.
move=> n1 x0.
Expand All @@ -129,10 +133,6 @@ rewrite ln_powR mulrCA mulVf//.
by rewrite gt_eqF// -ln1 ltr_ln ?posrE// ?ltr1n// ltr0n ltnW.
Qed.

(* TODO: rm *)
Lemma Exp_oppr n x : n `^ (- x) = (n `^ x)^-1.
Proof. by rewrite -powRN. Qed.

(* TODO: rm *)
Lemma Exp_gt0 n x : 0 < n -> 0 < n `^ x.
Proof. by move=> ?; rewrite powR_gt0. Qed.
Expand All @@ -154,6 +154,10 @@ Qed.
Lemma Exp_le_increasing n x y : 1 < n -> x <= y -> n `^ x <= n `^ y.
Proof. by move=> n1 xy; rewrite ler_powR// ltW. Qed.

(* TODO: move *)
Lemma morph_exp2_plus : {morph (fun x => 2 `^ x)%R : x y / x + y >-> x * y}.
Proof. by move=> ? ? /=; rewrite powRD// pnatr_eq0// implybT. Qed.

End Exp.

Hint Extern 0 (0 <= _ `^ _) => solve [exact/Exp_ge0] : core.
Expand Down

0 comments on commit c543060

Please sign in to comment.