From 67117a9c9f27f420d4ce17bcacbe09629c59c90c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 18 May 2024 01:52:59 +0100 Subject: [PATCH] split off and generalize Kronecker Delta in own file Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/KroneckerDelta.v | 148 ++++++++++++++++++++++++ theories/Algebra/Rings/Ring.v | 136 ---------------------- 2 files changed, 148 insertions(+), 136 deletions(-) create mode 100644 theories/Algebra/Rings/KroneckerDelta.v diff --git a/theories/Algebra/Rings/KroneckerDelta.v b/theories/Algebra/Rings/KroneckerDelta.v new file mode 100644 index 00000000000..3c849fd1076 --- /dev/null +++ b/theories/Algebra/Rings/KroneckerDelta.v @@ -0,0 +1,148 @@ +Require Import Basics.Overture Basics.Decidable Spaces.Nat. +Require Import Algebra.Rings.Ring. +Require Import Classes.interfaces.abstract_algebra. + +(** ** Kronecker Delta *) + +Section AssumeDecidable. + (** Throughout this section, we assume that we have a type [A] with decidable equality. This will be our indexing type and can be thought of as [nat] for reading purposes. *) + + Context {A : Type} `{DecidablePaths A}. + + (** The Kronecker delta function is a function of elements of [A] that is 1 when the two numbers are equal and 0 otherwise. It is useful for working with finite sums of ring elements. *) + Definition kronecker_delta {R : Ring} (i j : A) : R + := if dec (i = j) then 1 else 0. + + (** Kronecker delta with the same index is 1. *) + Definition kronecker_delta_refl {R : Ring} (i : A) + : kronecker_delta (R:=R) i i = 1. + Proof. + unfold kronecker_delta. + generalize (dec (i = i)). + by rapply decidable_paths_refl. + Defined. + + (** Kronecker delta with differing indices is 0. *) + Definition kronecker_delta_neq {R : Ring} {i j : A} (p : i <> j) + : kronecker_delta (R:=R) i j = 0. + Proof. + unfold kronecker_delta. + by decidable_false (dec (i = j)) p. + Defined. + + (** Kronecker delta is symmetric in its arguments. *) + Definition kronecker_delta_symm {R : Ring} (i j : A) + : kronecker_delta (R:=R) i j = kronecker_delta j i. + Proof. + unfold kronecker_delta. + destruct (dec (i = j)) as [p|q]. + - by decidable_true (dec (j = i)) p^. + - by decidable_false (dec (j = i)) (symmetric_neq q). + Defined. + + (** An injective endofunction on [A] preserves the Kronecker delta. *) + Definition kronecker_delta_map_inj {R : Ring} (i j : A) (f : A -> A) + `{!IsInjective f} + : kronecker_delta (R:=R) (f i) (f j) = kronecker_delta i j. + Proof. + unfold kronecker_delta. + destruct (dec (i = j)) as [p|p]. + - by decidable_true (dec (f i = f j)) (ap f p). + - destruct (dec (f i = f j)) as [q|q]. + + apply (injective f) in q. + contradiction. + + reflexivity. + Defined. + + (** Kronecker delta commutes with any ring element. *) + Definition kronecker_delta_comm {R : Ring} (i j : A) (r : R) + : r * kronecker_delta i j = kronecker_delta i j * r. + Proof. + unfold kronecker_delta. + destruct (dec (i = j)). + - exact (rng_mult_one_r _ @ (rng_mult_one_l _)^). + - exact (rng_mult_zero_r _ @ (rng_mult_zero_l _)^). + Defined. + +End AssumeDecidable. + +(** The following lemmas are specialised to when the indexing type is [nat]. *) + +(** Kronecker delta where the first index is strictly less than the second is 0. *) +Definition kronecker_delta_lt {R : Ring} {i j : nat} (p : (i < j)%nat) + : kronecker_delta (R:=R) i j = 0. +Proof. + apply kronecker_delta_neq. + intros q; destruct q. + by apply not_lt_n_n in p. +Defined. + +(** Kronecker delta where the first index is strictly greater than the second is 0. *) +Definition kronecker_delta_gt {R : Ring} {i j : nat} (p : (j < i)%nat) + : kronecker_delta (R:=R) i j = 0. +Proof. + apply kronecker_delta_neq. + intros q; destruct q. + by apply not_lt_n_n in p. +Defined. + +(** Kronecker delta can be used to extract a single term from a finite sum. *) +Definition rng_sum_kronecker_delta_l {R : Ring} (n i : nat) (Hi : (i < n)%nat) + (f : forall k, (k < n)%nat -> R) + : rng_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi. +Proof. + induction n as [|n IHn] in i, Hi, f |- *. + 1: destruct (not_leq_Sn_0 _ Hi). + destruct (dec (i = n)) as [p|p]. + - destruct p; simpl. + rewrite kronecker_delta_refl. + rewrite rng_mult_one_l. + rewrite <- rng_plus_zero_r. + f_ap; [f_ap; rapply path_ishprop|]. + nrapply rng_sum_zero. + intros k Hk. + rewrite (kronecker_delta_gt Hk). + apply rng_mult_zero_l. + - simpl; lhs nrapply ap. + + nrapply IHn. + apply diseq_implies_lt in p. + destruct p; [assumption|]. + contradiction (lt_implies_not_geq Hi). + + rewrite (kronecker_delta_neq p). + rewrite rng_mult_zero_l. + rewrite rng_plus_zero_l. + f_ap; apply path_ishprop. +Defined. + +(** Variant of [rng_sum_kronecker_delta_l] where the indexing is swapped. *) +Definition rng_sum_kronecker_delta_l' {R : Ring} (n i : nat) (Hi : (i < n)%nat) + (f : forall k, (k < n)%nat -> R) + : rng_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi. +Proof. + lhs nrapply path_rng_sum. + 2: nrapply rng_sum_kronecker_delta_l. + intros k Hk. + cbn; f_ap; apply kronecker_delta_symm. +Defined. + +(** Variant of [rng_sum_kronecker_delta_l] where the Kronecker delta appears on the right. *) +Definition rng_sum_kronecker_delta_r {R : Ring} (n i : nat) (Hi : (i < n)%nat) + (f : forall k, (k < n)%nat -> R) + : rng_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi. +Proof. + lhs nrapply path_rng_sum. + 2: nrapply rng_sum_kronecker_delta_l. + intros k Hk. + apply kronecker_delta_comm. +Defined. + +(** Variant of [rng_sum_kronecker_delta_r] where the indexing is swapped. *) +Definition rng_sum_kronecker_delta_r' {R : Ring} (n i : nat) (Hi : (i < n)%nat) + (f : forall k, (k < n)%nat -> R) + : rng_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi. +Proof. + lhs nrapply path_rng_sum. + 2: nrapply rng_sum_kronecker_delta_l'. + intros k Hk. + apply kronecker_delta_comm. +Defined. diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index d3043e9487b..06a0002c228 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -561,139 +561,3 @@ Proof. 1: apply rng_mult_zero_l. lhs nrapply rng_dist_r; simpl; f_ap. Defined. - -(** ** Kronecker Delta *) - -(** The Kronecker delta function is a function of two natural numbers that is 1 when the two numbers are equal and 0 otherwise. It is useful for working with finite sums of ring elements. *) -Definition kronecker_delta {R : Ring} (i j : nat) : R - := if dec (i = j) then 1 else 0. - -(** Kronecker delta with the same index is 1. This holds definitionally for a given natural number, but not definitionally for an arbitrary one. *) -Definition kronecker_delta_refl {R : Ring} (i : nat) - : kronecker_delta (R:=R) i i = 1. -Proof. - unfold kronecker_delta. - generalize (dec (i = i)). - by rapply decidable_paths_refl. -Defined. - -(** Kronecker delta with different indices is 0. *) -Definition kronecker_delta_neq {R : Ring} {i j : nat} (p : i <> j) - : kronecker_delta (R:=R) i j = 0. -Proof. - unfold kronecker_delta. - by decidable_false (dec (i = j)) p. -Defined. - -(** Kronecker delta is symmetric in its arguments. *) -Definition kronecker_delta_symm {R : Ring} (i j : nat) - : kronecker_delta (R:=R) i j = kronecker_delta j i. -Proof. - unfold kronecker_delta. - destruct (dec (i = j)) as [p|q]. - - by decidable_true (dec (j = i)) p^. - - by decidable_false (dec (j = i)) (symmetric_neq q). -Defined. - -(** Kronecker delta where the first index is strictly less than the second is 0. *) -Definition kronecker_delta_lt {R : Ring} {i j : nat} (p : (i < j)%nat) - : kronecker_delta (R:=R) i j = 0. -Proof. - apply kronecker_delta_neq. - intros q; destruct q. - by apply not_lt_n_n in p. -Defined. - -(** Kronecker delta where the first index is strictly greater than the second is 0. *) -Definition kronecker_delta_gt {R : Ring} {i j : nat} (p : (j < i)%nat) - : kronecker_delta (R:=R) i j = 0. -Proof. - apply kronecker_delta_neq. - intros q; destruct q. - by apply not_lt_n_n in p. -Defined. - -(** An injective endofunction on nat preserves the Kronecker delta. *) -Definition kronecker_delta_map_inj {R : Ring} (i j : nat) (f : nat -> nat) - `{!IsInjective f} - : kronecker_delta (R:=R) (f i) (f j) = kronecker_delta i j. -Proof. - unfold kronecker_delta. - destruct (dec (i = j)) as [p|p]. - - by decidable_true (dec (f i = f j)) (ap f p). - - destruct (dec (f i = f j)) as [q|q]. - + apply (injective f) in q. - contradiction. - + reflexivity. -Defined. - -(** Kronecker delta commutes with any ring element. *) -Definition kronecker_delta_comm {R : Ring} (i j : nat) (r : R) - : r * kronecker_delta i j = kronecker_delta i j * r. -Proof. - unfold kronecker_delta. - destruct (dec (i = j)). - - exact (rng_mult_one_r _ @ (rng_mult_one_l _)^). - - exact (rng_mult_zero_r _ @ (rng_mult_zero_l _)^). -Defined. - -(** Kronecker delta can be used to extract a single term from a finite sum. *) -Definition rng_sum_kronecker_delta_l {R : Ring} (n i : nat) (Hi : (i < n)%nat) - (f : forall k, (k < n)%nat -> R) - : rng_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi. -Proof. - induction n as [|n IHn] in i, Hi, f |- *. - 1: destruct (not_leq_Sn_0 _ Hi). - destruct (dec (i = n)) as [p|p]. - - destruct p; simpl. - rewrite kronecker_delta_refl. - rewrite rng_mult_one_l. - rewrite <- rng_plus_zero_r. - f_ap; [f_ap; rapply path_ishprop|]. - nrapply rng_sum_zero. - intros k Hk. - rewrite (kronecker_delta_gt Hk). - apply rng_mult_zero_l. - - simpl; lhs nrapply ap. - + nrapply IHn. - apply diseq_implies_lt in p. - destruct p; [assumption|]. - contradiction (lt_implies_not_geq Hi). - + rewrite (kronecker_delta_neq p). - rewrite rng_mult_zero_l. - rewrite rng_plus_zero_l. - f_ap; apply path_ishprop. -Defined. - -(** Variant of [rng_sum_kronecker_delta_l] where the indexing is swapped. *) -Definition rng_sum_kronecker_delta_l' {R : Ring} (n i : nat) (Hi : (i < n)%nat) - (f : forall k, (k < n)%nat -> R) - : rng_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi. -Proof. - lhs nrapply path_rng_sum. - 2: nrapply rng_sum_kronecker_delta_l. - intros k Hk. - cbn; f_ap; apply kronecker_delta_symm. -Defined. - -(** Variant of [rng_sum_kronecker_delta_l] where the Kronecker delta appears on the right. *) -Definition rng_sum_kronecker_delta_r {R : Ring} (n i : nat) (Hi : (i < n)%nat) - (f : forall k, (k < n)%nat -> R) - : rng_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi. -Proof. - lhs nrapply path_rng_sum. - 2: nrapply rng_sum_kronecker_delta_l. - intros k Hk. - apply kronecker_delta_comm. -Defined. - -(** Variant of [rng_sum_kronecker_delta_r] where the indexing is swapped. *) -Definition rng_sum_kronecker_delta_r' {R : Ring} (n i : nat) (Hi : (i < n)%nat) - (f : forall k, (k < n)%nat -> R) - : rng_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi. -Proof. - lhs nrapply path_rng_sum. - 2: nrapply rng_sum_kronecker_delta_l'. - intros k Hk. - apply kronecker_delta_comm. -Defined.