Skip to content

Commit

Permalink
only grs left?
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Apr 21, 2024
1 parent 2a71a75 commit 87c6499
Show file tree
Hide file tree
Showing 21 changed files with 177 additions and 152 deletions.
18 changes: 10 additions & 8 deletions ecc_classic/cyclic_code.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,10 +122,12 @@ Lemma rcs'_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : rcs' x = rcs x.
Proof.
rewrite /rcs' /rcs; apply/rowP => i; rewrite !mxE.
case: ifPn => [/eqP -> |i0].
congr (x _ _); apply val_inj => /=.
by rewrite PermDef.fun_of_permE ffunE /= inordK.
congr (x _ _).
rewrite /rcs_perm/= unlock/= ffunE eqxx.
apply/val_inj => /=.
by rewrite inordK.
congr (x _ _); apply val_inj => /=.
rewrite PermDef.fun_of_permE ffunE /= inordK.
rewrite unlock ffunE /= inordK.
by rewrite (negPf i0) inordK // (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
by rewrite (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
Qed.
Expand All @@ -138,7 +140,7 @@ rewrite coef_add_poly coefXM coefCM coef_add_poly coefXn 2!coef_opp_poly coefC.
case: ifPn => [/eqP ->|i0]; last rewrite subr0.
rewrite 2!add0r mulrN1 coef_rVpoly /=.
case: insubP => //= j _ j0.
rewrite mxE PermDef.fun_of_permE ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
rewrite mxE unlock ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
by apply val_inj => /=; rewrite inordK.
case/boolP : (i == n.+1) => [/eqP ->|in0].
rewrite mulr1 2!coef_rVpoly /=.
Expand All @@ -148,7 +150,7 @@ case/boolP : (i == n.+1) => [/eqP ->|in0].
rewrite mulr0 2!coef_rVpoly; case: insubP => /= [j|].
rewrite ltnS => in0' ji; case: insubP => /= [k _ ki|].
apply/eqP; rewrite subr_eq0; apply/eqP.
rewrite mxE PermDef.fun_of_permE ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
rewrite mxE unlock ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
apply/val_inj => /=; by rewrite inordK.
rewrite ltnS -ltnNge => n0i; exfalso.
rewrite -ltnS prednK // in in0'; last by rewrite lt0n.
Expand Down Expand Up @@ -234,20 +236,20 @@ rewrite (reindex_onto (@rcs_perm n) (perm_inv (@rcs_perm n))) /=; last first.
move=> i1 _; by rewrite permKV.
rewrite (eq_bigl xpredT); last by move=> i1; rewrite permK eqxx.
apply eq_bigr => i1 _.
rewrite coef_rVpoly PermDef.fun_of_permE ffunE.
rewrite coef_rVpoly unlock ffunE.
case: ifPn => [/eqP ->|].
case: insubP => [j _ jn0|]; last by rewrite ltnS leqnn.
rewrite /= in jn0.
rewrite coef_rVpoly; case: insubP => // k _ k0.
rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE k0 /= expr0 mulr1.
rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE k0 /= expr0 mulr1.
by rewrite exprAC an1 expr1n mulr1; congr (x _ _); apply val_inj => /=.
case: insubP => /= [j|].
rewrite ltnS => i1n0 ji1 i10; rewrite coef_rVpoly.
case: insubP => /= [k|].
rewrite ltnS => i1n0' ki1.
rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
rewrite inordK; last by rewrite ltnW // ltnS prednK // lt0n.
rewrite prednK // ?lt0n //; congr (x _ _ * _).
by apply/val_inj.
Expand Down
4 changes: 2 additions & 2 deletions ecc_classic/decoding.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ Section maximum_likelihood_decoding_prop.
Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
Variables (n : nat) (C : {vspace 'rV[A]_n}).
Variable repair : decT B [finType of 'rV[A]_n] n.
Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
Let P := fdist_uniform_supp R (vspace_not_empty C).
Hypothesis ML_dec : ML_decoding W C repair P.

Local Open Scope channel_code_scope.
Expand Down Expand Up @@ -288,7 +288,7 @@ Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
Variables (n : nat) (C : {vspace 'rV[A]_n}).
Variable dec : decT B [finType of 'rV[A]_n] n.
Variable dec_img : oimg dec \subset C.
Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
Let P := fdist_uniform_supp R (vspace_not_empty C).

Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P.
Proof.
Expand Down
50 changes: 25 additions & 25 deletions ecc_classic/hamming_code.v
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp.
From mathcomp Require Import matrix mxalgebra vector.
From mathcomp Require Import Rstruct.
From mathcomp Require Import Rstruct reals.
Require Import realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming.
Require Import bigop_ext fdist proba channel channel_code decoding.
Require Import binary_symmetric_channel.
Expand Down Expand Up @@ -78,13 +78,13 @@ rewrite /n /len !expnS -subn1 doubleB -muln2 -subSn; last first.
by rewrite -muln2 mul1n subn2 /= mulnC.
Qed.

Lemma two_len : 2 < n.
Lemma two_len : (2 < n)%N.
Proof. by rewrite len_dim -subn1 ltn_subRL (@leq_exp2l 2 2). Qed.

Lemma dim_len : m <= n.
Lemma dim_len : (m <= n)%N.
Proof. by rewrite len_dim -ltnS prednK ?expn_gt0 // ltn_expl. Qed.

Lemma len_two_m (i : 'I_n) : i.+1 < 2 ^ m.
Lemma len_two_m (i : 'I_n) : (i.+1 < 2 ^ m)%N.
Proof.
by rewrite (leq_ltn_trans (ltn_ord i)) // len_dim -ltnS prednK // expn_gt0.
Qed.
Expand Down Expand Up @@ -216,9 +216,9 @@ Proof.
move: (min_dist_is_min hamming_not_trivial) => Hforall.
move: (min_dist_achieved hamming_not_trivial) => Hexists.
move: (min_dist_neq0) => H3.
suff : min_dist hamming_not_trivial <> 1%N /\
min_dist hamming_not_trivial <> 2%N /\
min_dist hamming_not_trivial <= 3%N.
suff : (min_dist hamming_not_trivial <> 1 /\
min_dist hamming_not_trivial <> 2 /\
min_dist hamming_not_trivial <= 3)%N.
move : H3.
move/(_ _ _ _ hamming_not_trivial).
destruct (min_dist hamming_not_trivial) as [|p]=> //.
Expand Down Expand Up @@ -253,7 +253,7 @@ Definition hamming_err y :=
let i := nat_of_rV (syndrome (Hamming.PCM m) y) in
if i is O then 0 else rV_of_nat n (2 ^ (n - i)).

Lemma wH_hamming_err_ub y : wH (hamming_err y) <= 1.
Lemma wH_hamming_err_ub y : (wH (hamming_err y) <= 1)%N.
Proof.
rewrite /hamming_err.
move Hy : (nat_of_rV _) => [|p /=].
Expand All @@ -266,13 +266,13 @@ Definition alt_hamming_err (y : 'rV_n) : 'rV['F_2]_n :=
let n0 := nat_of_rV s in
if n0 is O then 0 else (\row_(j < n) if n0.-1 == j then 1 else 0).

Lemma alt_hamming_err_ub y : wH (alt_hamming_err y) <= 1.
Lemma alt_hamming_err_ub y : (wH (alt_hamming_err y) <= 1)%N.
Proof.
rewrite /alt_hamming_err.
destruct (nat_of_rV _); first by rewrite wH0.
clearbody n; clear.
rewrite wH_sum.
case/boolP : (n0 < n) => n0n.
case/boolP : (n0 < n)%N => n0n.
rewrite (bigD1 (Ordinal n0n)) //= mxE eqxx (eq_bigr (fun x => O)); last first.
move=> i Hi; rewrite mxE ifF //.
apply: contraNF Hi => /eqP Hi; by apply/eqP/val_inj.
Expand All @@ -291,7 +291,7 @@ case/boolP : (s == 0) => [/eqP ->|s0].
have [k ks] : exists k : 'I_n, nat_of_rV s = k.+1.
move: s0; rewrite -nat_of_rV_eq0 -lt0n => s0.
move: (nat_of_rV_up s) => sup.
have sn1up : (nat_of_rV s).-1 < n.
have sn1up : ((nat_of_rV s).-1 < n)%N.
by rewrite /n Hamming.len_dim -ltnS prednK // prednK // expn_gt0.
exists (Ordinal sn1up); by rewrite /= prednK.
rewrite ks /= /syndrome.
Expand Down Expand Up @@ -369,13 +369,13 @@ Variable m' : nat.
Let m := m'.+2.
Let n := Hamming.len m'.

Lemma cols_PCM : [set c | wH c^T >= 1] = [set col i (Hamming.PCM m) | i : 'I_n].
Lemma cols_PCM : [set c | (wH c^T >= 1)%N] = [set col i (Hamming.PCM m) | i : 'I_n].
Proof.
apply/setP => i.
rewrite in_set.
case Hi : (0 < wH i^T).
case Hi : (0 < wH i^T)%N.
apply/esym/imsetP.
have H0 : nat_of_rV i^T - 1 < n.
have H0 : (nat_of_rV i^T - 1 < n)%N.
have iup := nat_of_rV_up i^T.
rewrite /n Hamming.len_dim -subn1 ltn_sub2r //.
by rewrite -{1}(expn0 2) ltn_exp2l // ltnW.
Expand Down Expand Up @@ -436,14 +436,14 @@ rewrite !mxE eqxx /=.
by case Hji : (j == i) => // _; apply/esym/eqP.
Qed.

Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1].
Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1]%N.

Definition unit_cols := [set c : 'cV['F_2]_m | wH c^T == 1%nat].

Lemma card_all_cols : #|non_unit_cols :|: unit_cols| = n.
Proof.
rewrite /non_unit_cols /unit_cols.
transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|.
transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1]%N|.
apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt.
by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj.
Qed.
Expand Down Expand Up @@ -521,7 +521,7 @@ Qed.
Lemma idsA_ids1 (i : 'I_(n - m)) (j : 'I_m) : idsA `_ i <> sval (ids1 j).
Proof.
destruct (ids1 j) => /= Hij.
have Hlti : i < size idsA by rewrite size_idsA.
have Hlti : (i < size idsA)%N by rewrite size_idsA.
move: (mem_nth 0 Hlti).
rewrite Hij => Hi.
move: (imset_f (fun i => col i (Hamming.PCM m)) Hi).
Expand Down Expand Up @@ -571,7 +571,7 @@ Lemma PCM_A_1 : PCM = castmx (erefl, subnK (Hamming.dim_len m')) (row_mx CSM 1).
Proof.
apply/matrixP => i j.
rewrite mxE castmxE /=.
case/boolP : (j < n - m) => Hcond.
case/boolP : (j < n - m)%N => Hcond.
have -> : cast_ord (esym (subnK (Hamming.dim_len m'))) j =
lshift m (Ordinal Hcond) by apply val_inj.
rewrite row_mxEl [in X in _ = X]mxE.
Expand Down Expand Up @@ -792,7 +792,7 @@ rewrite -mulmxA.
have [Y1 [Y2 HY]] : exists (Y1 : 'cV_ _) Y2, (row_perm systematic y^T) =
castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 Y2).
exists (\matrix_(j < 1, i < n - m) (y j (systematic (widen_ord (leq_subr m n) i))))^T.
have dim_len_new i (Hi : i < m) : n - m + i < n.
have dim_len_new i (Hi : (i < m)%N) : (n - m + i < n)%N.
by rewrite -ltn_subRL subnBA ?Hamming.dim_len // addnC addnK.
exists (\matrix_(j < 1, i < m) (y j (systematic (Ordinal (dim_len_new _ (ltn_ord i))))))^T.
apply/colP => a /=.
Expand Down Expand Up @@ -910,7 +910,7 @@ move=> ->.
Defined.

Lemma encode_decode c y : c \in lcode ->
repair y != None -> dH c y <= 1 -> repair y = Some c.
repair y != None -> (dH c y <= 1)%N -> repair y = Some c.
Proof.
move=> Hc Hy cy.
apply: (@mddP _ _ lcode _ decoder (hamming_not_trivial r')) => //.
Expand All @@ -919,7 +919,7 @@ by rewrite /mdd_err_cor hamming_min_dist.
Qed.

Lemma repair_failure2 e c : c \in lcode ->
~~ (if repair e is Some y0 then y0 != c else true) -> wH (c + e) <= 1.
~~ (if repair e is Some y0 then y0 != c else true) -> (wH (c + e) <= 1)%N.
Proof.
move=> Hc H.
suff : dH e c = O \/ dH e c = 1%N by rewrite dHE F2_mx_opp addrC; case=> ->.
Expand All @@ -933,7 +933,7 @@ rewrite dH_wH leq_eqVlt ?ltnS ?leqn0 => /orP[|] /eqP ->; by auto.
Qed.

Lemma repair_failure1 e c : c \in lcode ->
(if repair e is Some x then x != c else true) -> 1 < wH (c + e).
(if repair e is Some x then x != c else true) -> (1 < wH (c + e))%N.
Proof.
move=> Hc.
move xc : (repair e) => [x ex |]; last first.
Expand All @@ -947,7 +947,7 @@ rewrite leq_eqVlt ltnS leqn0 orbC => /orP[|/eqP cy1].
Qed.

Lemma repair_failure e c : c \in lcode ->
(if repair e is Some x then x != c else true) = (1 < wH (c + e)).
(if repair e is Some x then x != c else true) = (1 < wH (c + e))%N.
Proof.
move=> Hc.
apply/idP/idP; first by move/repair_failure1; apply.
Expand All @@ -963,7 +963,7 @@ Require Import Reals Reals_ext.
Section hamming_code_error_rate.

Variable M : finType.
Hypothesis M_not_0 : 0 < #|M|.
Hypothesis M_not_0 : (0 < #|M|)%nat.
Variable p : {prob R}.
Let card_F2 : #| 'F_2 | = 2%N. by rewrite card_Fp. Qed.
Let W := BSC.c card_F2 p.
Expand Down
43 changes: 27 additions & 16 deletions ecc_classic/linearcode.v
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg poly polydiv fingroup perm.
From mathcomp Require Import finalg zmodp matrix mxalgebra mxpoly vector.
Require Import ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code.
Expand Down Expand Up @@ -117,18 +118,23 @@ Proof. by rewrite /syndrome trmx0 mulmx0 trmx0. Qed.
Lemma additive_syndrome : additive syndrome.
Proof. move=> x y; by rewrite syndromeD syndromeN. Qed.

Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} :=
GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).
HB.instance Definition _ :=
GRing.isAdditive.Build _ _ _ additive_syndrome.
HB.instance Definition _ :=
GRing.isScalable.Build _ _ _ _ _ syndromeZ.

Definition hom_syndrome : 'Hom(matrix_vectType F 1 n, matrix_vectType F 1 m) :=
linfun lin_syndrome.
(*Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} :=
GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).*)

Definition hom_syndrome : 'Hom('rV[F]_n, 'rV[F]_m) :=
linfun syndrome.

Definition kernel : Lcode0.t F n := lker hom_syndrome.

Lemma dim_hom_syndrome_ub : \dim (limg hom_syndrome) <= m.
Proof.
rewrite [in X in _ <= X](_ : m = \dim (fullv : {vspace 'rV[F]_m})); last first.
by rewrite dimvf /Vector.dim /= mul1n.
by rewrite dimvf/= /dim/= mul1n.
by rewrite dimvS // subvf.
Qed.

Expand All @@ -139,7 +145,7 @@ Lemma dim_kernel (Hm : \rank H = m) (mn : m <= n) : \dim kernel = (n - m)%N.
Proof.
move: (limg_ker_dim hom_syndrome fullv).
rewrite (_ : (fullv :&: _)%VS = kernel); last by apply/capv_idPr/subvf.
rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n.
rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n.
move=> H0; rewrite -{}[in RHS]H0.
suff -> : \dim (limg hom_syndrome) = m by rewrite addnK.
set K := castmx (erefl, Hm) (col_base H).
Expand Down Expand Up @@ -190,14 +196,14 @@ Section dual_code.
Variables (F : finFieldType) (m n : nat) (H : 'M[F]_(m, n)).

Definition dual_code : {vspace 'rV[F]_n} :=
(linfun (mulmxr_linear _ H) @: fullv)%VS.
(linfun (mulmxr H) @: fullv)%VS.

Lemma dim_dual_code : (\dim (kernel H) + \dim dual_code = n)%N.
Proof.
move: (limg_ker_dim (linfun (lin_syndrome H)) fullv).
move: (limg_ker_dim (linfun (syndrome H)) fullv).
rewrite -/(kernel H).
rewrite (_ : (fullv :&: _)%VS = kernel H); last by apply/capv_idPr/subvf.
rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n.
rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n.
rewrite (_ : \dim (limg _) = \dim dual_code) // /dual_code.
rewrite /dimv.
Abort.
Expand Down Expand Up @@ -390,28 +396,33 @@ Proof. by apply/rowP => i; rewrite !mxE. Qed.
Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H).
Proof. by move=> x y; rewrite sbound_f'D sbound_f'N. Qed.

Definition sbound_f_linear k (H : k.-1 <= n) :
HB.instance Definition _ k (H : k.-1 <= n) :=
GRing.isAdditive.Build _ _ _ (additive_sbound_f' H).
HB.instance Definition _ k (H : k.-1 <= n) :=
GRing.isScalable.Build _ _ _ _ _ (sbound_f'Z H).

(*Definition sbound_f_linear k (H : k.-1 <= n) :
{linear 'rV[F]_n -> 'rV[F]_k.-1} :=
GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)).
GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)).*)

(* McEliece, theorem 9.8, p.255 *)
Lemma singleton_bound : min_dist <= n - \dim C + 1.
Proof.
set k := \dim C.
have dimCn : k.-1 < n.
have /dimvS := subvf C.
rewrite dimvf /Vector.dim /= mul1n.
rewrite dimvf /dim /= mul1n.
by apply: leq_trans; rewrite prednK // not_trivial_dim.
set f := linfun (sbound_f_linear (ltnW dimCn)).
set f := linfun (sbound_f' (ltnW dimCn)).
have H1 : \dim (f @: C) <= k.-1.
suff : \dim (f @: C) <= \dim (fullv : {vspace 'rV[F]_k.-1}).
by rewrite dimvf /= /Vector.dim /= mul1n.
by rewrite dimvf /= /dim /= mul1n.
by apply/dimvS/subvf.
have H2 : (\dim (f @: C) + \dim (C :&: lker f) = \dim (fullv : {vspace 'rV[F]_k}))%N.
by rewrite dimvf /= /Vector.dim /= mul1n -[RHS](limg_ker_dim f C) addnC.
by rewrite dimvf /= /dim /= mul1n -[RHS](limg_ker_dim f C) addnC.
have H3 : 1 <= \dim (C :&: lker f).
rewrite lt0n; apply/eqP => abs; move: H2.
rewrite abs addn0 dimvf /Vector.dim /= mul1n -/k.
rewrite abs addn0 dimvf /dim /= mul1n -/k.
apply/eqP.
move: H1; rewrite leqNgt; apply: contra => /eqP ->.
by rewrite prednK // not_trivial_dim.
Expand Down
5 changes: 3 additions & 2 deletions ecc_modern/checksum.v
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp.
From mathcomp Require Import matrix vector.
Require Import Reals.
From mathcomp Require Import Rstruct.
Require Import ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode.
Require Import pproba.

Expand Down Expand Up @@ -171,7 +172,7 @@ Qed.
Local Close Scope R_scope.

Let C := kernel H.
Hypothesis HC : 0 < #| [set cw in C] |.
Hypothesis HC : (0 < #| [set cw in C] |)%nat.

Local Open Scope proba_scope.
Variable y : (`U HC).-receivable W.
Expand Down
Loading

0 comments on commit 87c6499

Please sign in to comment.