QuantumLib.FiniteGroups
Require Import List.
Require Import Prelim.
Require Import Summation.
Require Import FinFun.
Require Import ListDec.
Require Import Setoid.
Program Instance list_is_monoid {X} : Monoid (list X) :=
{ Gzero := []
; Gplus := @app X
}.
Lemma big_sum_list_length : ∀ {X} (l : list (list X)) (l' : list X),
G_big_plus l = l' → G_big_plus (map (@length X) l) = length l'.
Lemma length_big_sum_list : ∀ {X} (l : list (list X)),
length (G_big_plus l) = G_big_plus (map (@length X) l).
Lemma In_big_sum_list_In_part : ∀ {X} (l : list (list X)) (x : X),
In x (G_big_plus l) →
∃ l1, In l1 l ∧ In x l1.
Lemma In_part_In_big_sum_list : ∀ {X} (l : list (list X)) (x : X),
(∃ l1, In l1 l ∧ In x l1) →
In x (G_big_plus l).
Inductive eq_mod_perm {X} (l1 l2 : list X) : Prop :=
| eq_list : NoDup l1 → NoDup l2 → incl l1 l2 → incl l2 l1 → eq_mod_perm l1 l2.
Infix "⩦" := eq_mod_perm (at level 70).
Definition disjoint {X} (l1 l2 : list X) : Prop := NoDup (l1 ++ l2).
Lemma In_EMP_compat : ∀ {X} (l1 l2 : list X) (x : X),
l1 ⩦ l2 → (iff (In x l1) (In x l2)).
Add Parametric Morphism {X} : (@In X)
with signature eq ==> eq_mod_perm ==> iff as Pplusf_mor.
Lemma NoDup_app : ∀ {X} (l1 l2 : list X),
NoDup l1 → NoDup l2 →
(∀ x, In x l1 → ¬ (In x l2)) →
NoDup (l1 ++ l2).
Lemma length_lt_new_elem : ∀ {X} (l2 l1 : list X)
(eq_dec : ∀ x y : X, {x = y} + {x ≠ y}),
length l1 < length l2 →
NoDup l2 →
∃ x, In x l2 ∧ ¬ (In x l1).
Lemma length_gt_EMP : ∀ {X} (l1 l2 : list X),
NoDup l1 → NoDup l2 →
incl l1 l2 →
length l1 ≥ length l2 →
l1 ⩦ l2.
Lemma EMP_reduce : ∀ {X} (l1 l21 l22 : list X) (a : X),
(a :: l1) ⩦ (l21 ++ (a::l22)) → l1 ⩦ (l21 ++ l22).
Lemma EMP_eq_length : ∀ {X} (l1 l2 : list X),
l1 ⩦ l2 → length l1 = length l2.
Lemma list_rep_length_eq : ∀ {X} (l1 l2 : list X),
Listing l1 → Listing l2 → length l1 = length l2.
Lemma test : NoDup [1;2;3;4;5]%nat.
Class FiniteGroup G `{Group G} :=
{ G_list_rep : list G
; G_finite_ver : Listing G_list_rep
; G_eq_dec : ∀ x y : G, {x = y} + {x ≠ y}
}.
Infix "·" := Gplus (at level 40) : group_scope.
Definition group_size G `{FiniteGroup G} := length G_list_rep.
Lemma group_size_gt_0 : ∀ G `{FiniteGroup G},
group_size G > 0.
Lemma finitegroup_finite : ∀ G `{FiniteGroup G},
Finite' G.
Lemma Gplus_injective : ∀ G `{Group G} (g : G),
Injective (Gplus g).
Lemma Gplus_surjective : ∀ G `{Group G} (g : G),
Surjective (Gplus g).
Lemma mul_by_g_perm : ∀ G `{FiniteGroup G} (g : G),
Listing (map (Gplus g) G_list_rep).
Definition group_homomorphism (H G : Type) `{FiniteGroup H} `{FiniteGroup G} (f : H → G) : Prop :=
∀ x1 x2, f (x1 · x2) = f x1 · f x2.
Definition inclusion_map (H G : Type) `{FiniteGroup H} `{FiniteGroup G} (f : H → G) : Prop :=
Injective f ∧ group_homomorphism H G f.
Definition sub_group (H G : Type) `{FiniteGroup H} `{FiniteGroup G} : Prop :=
∃ f, inclusion_map H G f.
Lemma homo_id : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
group_homomorphism H G f → f 0 = 0.
Lemma homo_inv : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (h : H),
group_homomorphism H G f → f (- h) = - (f h).
Lemma sub_group_closed_under_inv : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a : G),
inclusion_map H G f →
In a (map f G_list_rep) → In (- a) (map f G_list_rep).
Lemma sub_group_closed_under_mul : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
In a (map f G_list_rep) → In b (map f G_list_rep) →
In (a · b) (map f G_list_rep).
Lemma in_own_coset : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a : G),
inclusion_map H G f →
In a (map (Gplus a) (map f G_list_rep)).
Lemma in_coset_cancel : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
In a (map (Gplus b) (map f G_list_rep)) ↔ In ((- b) · a) (map f G_list_rep).
Lemma cosets_same1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
(∃ x, In x (map (Gplus a) (map f G_list_rep)) ∧ In x (map (Gplus b) (map f G_list_rep))) →
(map (Gplus a) (map f G_list_rep)) ⩦ (map (Gplus b) (map f G_list_rep)).
Lemma cosets_same2 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
(In b (map (Gplus a) (map f G_list_rep))) →
(map (Gplus a) (map f G_list_rep)) ⩦ (map (Gplus b) (map f G_list_rep)).
Lemma cosets_diff : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
¬ (In b (map (Gplus a) (map f G_list_rep))) →
NoDup ((map (Gplus a) (map f G_list_rep)) ++ (map (Gplus b) (map f G_list_rep))).
Definition coset_rep_list_to_cosets H G `{FiniteGroup H} `{FiniteGroup G}
(f : H → G) (l : list G) : list G :=
(G_big_plus (map (fun g ⇒ map (Gplus g) (map f G_list_rep)) l)).
Lemma extend_coset_rep_list : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (l : list G),
inclusion_map H G f →
NoDup (coset_rep_list_to_cosets H G f l) →
length (coset_rep_list_to_cosets H G f l) < group_size G →
∃ g, NoDup (coset_rep_list_to_cosets H G f (g::l)).
Lemma length_cosets : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (l : list G),
inclusion_map H G f →
length (coset_rep_list_to_cosets H G f l) = (group_size H × length l)%nat.
Lemma get_coset_rep_list1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (n : nat),
inclusion_map H G f →
group_size H × n ≤ group_size G →
∃ l, length l = n ∧ NoDup (coset_rep_list_to_cosets H G f l).
Lemma get_coset_rep_list2 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ l, group_size H × length l ≥ group_size G ∧ NoDup (coset_rep_list_to_cosets H G f l).
Lemma get_full_coset_reps1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ (l : list G), (coset_rep_list_to_cosets H G f l) ⩦ G_list_rep.
Theorem Lagranges_Theorem : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ d, (group_size H × d)%nat = group_size G.
Inductive Quaternion :=
| p_1
| n_1
| p_i
| n_i
| p_j
| n_j
| p_k
| n_k.
Definition quatNeg (q : Quaternion) : Quaternion :=
match q with
| p_1 ⇒ n_1
| n_1 ⇒ p_1
| p_i ⇒ n_i
| n_i ⇒ p_i
| p_j ⇒ n_j
| n_j ⇒ p_j
| p_k ⇒ n_k
| n_k ⇒ p_k
end.
Definition quatInv (q : Quaternion) : Quaternion :=
match q with
| p_1 ⇒ p_1
| n_1 ⇒ n_1
| p_i ⇒ n_i
| n_i ⇒ p_i
| p_j ⇒ n_j
| n_j ⇒ p_j
| p_k ⇒ n_k
| n_k ⇒ p_k
end.
Lemma quatNeg_inv : ∀ (q : Quaternion), quatNeg (quatNeg q) = q.
Lemma quatInv_inv : ∀ (q : Quaternion), quatInv (quatInv q) = q.
Definition quatMul (q1 q2 : Quaternion) : Quaternion :=
match (q1, q2) with
| (p_1, _) ⇒ q2
| (_, p_1) ⇒ q1
| (n_1, _) ⇒ quatNeg q2
| (_, n_1) ⇒ quatNeg q1
| (p_i, p_i) ⇒ n_1
| (p_i, n_i) ⇒ p_1
| (p_i, p_j) ⇒ p_k
| (p_i, n_j) ⇒ n_k
| (p_i, p_k) ⇒ n_j
| (p_i, n_k) ⇒ p_j
| (n_i, p_i) ⇒ p_1
| (n_i, n_i) ⇒ n_1
| (n_i, p_j) ⇒ n_k
| (n_i, n_j) ⇒ p_k
| (n_i, p_k) ⇒ p_j
| (n_i, n_k) ⇒ n_j
| (p_j, p_i) ⇒ n_k
| (p_j, n_i) ⇒ p_k
| (p_j, p_j) ⇒ n_1
| (p_j, n_j) ⇒ p_1
| (p_j, p_k) ⇒ p_i
| (p_j, n_k) ⇒ n_i
| (n_j, p_i) ⇒ p_k
| (n_j, n_i) ⇒ n_k
| (n_j, p_j) ⇒ p_1
| (n_j, n_j) ⇒ n_1
| (n_j, p_k) ⇒ n_i
| (n_j, n_k) ⇒ p_i
| (p_k, p_i) ⇒ p_j
| (p_k, n_i) ⇒ n_j
| (p_k, p_j) ⇒ n_i
| (p_k, n_j) ⇒ p_i
| (p_k, p_k) ⇒ n_1
| (p_k, n_k) ⇒ p_1
| (n_k, p_i) ⇒ n_j
| (n_k, n_i) ⇒ p_j
| (n_k, p_j) ⇒ p_i
| (n_k, n_j) ⇒ n_i
| (n_k, p_k) ⇒ p_1
| (n_k, n_k) ⇒ n_1
end.
Program Instance quat_is_monoid : Monoid Quaternion :=
{ Gzero := p_1
; Gplus := quatMul
}.
Solve All Obligations with program_simpl; destruct g; try easy; destruct h; destruct i; easy.
Program Instance quat_is_group : Group Quaternion :=
{ Gopp := quatInv }.
Solve All Obligations with program_simpl; destruct g; try easy.
Lemma quatMul_comm : ∀ (q1 q2 : Quaternion),
q1 · q2 = q2 · q1 ∨ q1 · q2 = quatNeg (q2 · q1).
Definition quat_list : list Quaternion := [p_1; p_i; p_j; p_k; n_1; n_i; n_j; n_k].
Program Instance quat_is_finitegroup : FiniteGroup Quaternion :=
{ G_list_rep := quat_list
}.
Require Import Prelim.
Require Import Summation.
Require Import FinFun.
Require Import ListDec.
Require Import Setoid.
Program Instance list_is_monoid {X} : Monoid (list X) :=
{ Gzero := []
; Gplus := @app X
}.
Lemma big_sum_list_length : ∀ {X} (l : list (list X)) (l' : list X),
G_big_plus l = l' → G_big_plus (map (@length X) l) = length l'.
Lemma length_big_sum_list : ∀ {X} (l : list (list X)),
length (G_big_plus l) = G_big_plus (map (@length X) l).
Lemma In_big_sum_list_In_part : ∀ {X} (l : list (list X)) (x : X),
In x (G_big_plus l) →
∃ l1, In l1 l ∧ In x l1.
Lemma In_part_In_big_sum_list : ∀ {X} (l : list (list X)) (x : X),
(∃ l1, In l1 l ∧ In x l1) →
In x (G_big_plus l).
Inductive eq_mod_perm {X} (l1 l2 : list X) : Prop :=
| eq_list : NoDup l1 → NoDup l2 → incl l1 l2 → incl l2 l1 → eq_mod_perm l1 l2.
Infix "⩦" := eq_mod_perm (at level 70).
Definition disjoint {X} (l1 l2 : list X) : Prop := NoDup (l1 ++ l2).
Lemma In_EMP_compat : ∀ {X} (l1 l2 : list X) (x : X),
l1 ⩦ l2 → (iff (In x l1) (In x l2)).
Add Parametric Morphism {X} : (@In X)
with signature eq ==> eq_mod_perm ==> iff as Pplusf_mor.
Lemma NoDup_app : ∀ {X} (l1 l2 : list X),
NoDup l1 → NoDup l2 →
(∀ x, In x l1 → ¬ (In x l2)) →
NoDup (l1 ++ l2).
Lemma length_lt_new_elem : ∀ {X} (l2 l1 : list X)
(eq_dec : ∀ x y : X, {x = y} + {x ≠ y}),
length l1 < length l2 →
NoDup l2 →
∃ x, In x l2 ∧ ¬ (In x l1).
Lemma length_gt_EMP : ∀ {X} (l1 l2 : list X),
NoDup l1 → NoDup l2 →
incl l1 l2 →
length l1 ≥ length l2 →
l1 ⩦ l2.
Lemma EMP_reduce : ∀ {X} (l1 l21 l22 : list X) (a : X),
(a :: l1) ⩦ (l21 ++ (a::l22)) → l1 ⩦ (l21 ++ l22).
Lemma EMP_eq_length : ∀ {X} (l1 l2 : list X),
l1 ⩦ l2 → length l1 = length l2.
Lemma list_rep_length_eq : ∀ {X} (l1 l2 : list X),
Listing l1 → Listing l2 → length l1 = length l2.
Lemma test : NoDup [1;2;3;4;5]%nat.
Class FiniteGroup G `{Group G} :=
{ G_list_rep : list G
; G_finite_ver : Listing G_list_rep
; G_eq_dec : ∀ x y : G, {x = y} + {x ≠ y}
}.
Infix "·" := Gplus (at level 40) : group_scope.
Definition group_size G `{FiniteGroup G} := length G_list_rep.
Lemma group_size_gt_0 : ∀ G `{FiniteGroup G},
group_size G > 0.
Lemma finitegroup_finite : ∀ G `{FiniteGroup G},
Finite' G.
Lemma Gplus_injective : ∀ G `{Group G} (g : G),
Injective (Gplus g).
Lemma Gplus_surjective : ∀ G `{Group G} (g : G),
Surjective (Gplus g).
Lemma mul_by_g_perm : ∀ G `{FiniteGroup G} (g : G),
Listing (map (Gplus g) G_list_rep).
Definition group_homomorphism (H G : Type) `{FiniteGroup H} `{FiniteGroup G} (f : H → G) : Prop :=
∀ x1 x2, f (x1 · x2) = f x1 · f x2.
Definition inclusion_map (H G : Type) `{FiniteGroup H} `{FiniteGroup G} (f : H → G) : Prop :=
Injective f ∧ group_homomorphism H G f.
Definition sub_group (H G : Type) `{FiniteGroup H} `{FiniteGroup G} : Prop :=
∃ f, inclusion_map H G f.
Lemma homo_id : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
group_homomorphism H G f → f 0 = 0.
Lemma homo_inv : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (h : H),
group_homomorphism H G f → f (- h) = - (f h).
Lemma sub_group_closed_under_inv : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a : G),
inclusion_map H G f →
In a (map f G_list_rep) → In (- a) (map f G_list_rep).
Lemma sub_group_closed_under_mul : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
In a (map f G_list_rep) → In b (map f G_list_rep) →
In (a · b) (map f G_list_rep).
Lemma in_own_coset : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a : G),
inclusion_map H G f →
In a (map (Gplus a) (map f G_list_rep)).
Lemma in_coset_cancel : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
In a (map (Gplus b) (map f G_list_rep)) ↔ In ((- b) · a) (map f G_list_rep).
Lemma cosets_same1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
(∃ x, In x (map (Gplus a) (map f G_list_rep)) ∧ In x (map (Gplus b) (map f G_list_rep))) →
(map (Gplus a) (map f G_list_rep)) ⩦ (map (Gplus b) (map f G_list_rep)).
Lemma cosets_same2 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
(In b (map (Gplus a) (map f G_list_rep))) →
(map (Gplus a) (map f G_list_rep)) ⩦ (map (Gplus b) (map f G_list_rep)).
Lemma cosets_diff : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (a b : G),
inclusion_map H G f →
¬ (In b (map (Gplus a) (map f G_list_rep))) →
NoDup ((map (Gplus a) (map f G_list_rep)) ++ (map (Gplus b) (map f G_list_rep))).
Definition coset_rep_list_to_cosets H G `{FiniteGroup H} `{FiniteGroup G}
(f : H → G) (l : list G) : list G :=
(G_big_plus (map (fun g ⇒ map (Gplus g) (map f G_list_rep)) l)).
Lemma extend_coset_rep_list : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (l : list G),
inclusion_map H G f →
NoDup (coset_rep_list_to_cosets H G f l) →
length (coset_rep_list_to_cosets H G f l) < group_size G →
∃ g, NoDup (coset_rep_list_to_cosets H G f (g::l)).
Lemma length_cosets : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (l : list G),
inclusion_map H G f →
length (coset_rep_list_to_cosets H G f l) = (group_size H × length l)%nat.
Lemma get_coset_rep_list1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G) (n : nat),
inclusion_map H G f →
group_size H × n ≤ group_size G →
∃ l, length l = n ∧ NoDup (coset_rep_list_to_cosets H G f l).
Lemma get_coset_rep_list2 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ l, group_size H × length l ≥ group_size G ∧ NoDup (coset_rep_list_to_cosets H G f l).
Lemma get_full_coset_reps1 : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ (l : list G), (coset_rep_list_to_cosets H G f l) ⩦ G_list_rep.
Theorem Lagranges_Theorem : ∀ H G `{FiniteGroup H} `{FiniteGroup G} (f : H → G),
inclusion_map H G f →
∃ d, (group_size H × d)%nat = group_size G.
Inductive Quaternion :=
| p_1
| n_1
| p_i
| n_i
| p_j
| n_j
| p_k
| n_k.
Definition quatNeg (q : Quaternion) : Quaternion :=
match q with
| p_1 ⇒ n_1
| n_1 ⇒ p_1
| p_i ⇒ n_i
| n_i ⇒ p_i
| p_j ⇒ n_j
| n_j ⇒ p_j
| p_k ⇒ n_k
| n_k ⇒ p_k
end.
Definition quatInv (q : Quaternion) : Quaternion :=
match q with
| p_1 ⇒ p_1
| n_1 ⇒ n_1
| p_i ⇒ n_i
| n_i ⇒ p_i
| p_j ⇒ n_j
| n_j ⇒ p_j
| p_k ⇒ n_k
| n_k ⇒ p_k
end.
Lemma quatNeg_inv : ∀ (q : Quaternion), quatNeg (quatNeg q) = q.
Lemma quatInv_inv : ∀ (q : Quaternion), quatInv (quatInv q) = q.
Definition quatMul (q1 q2 : Quaternion) : Quaternion :=
match (q1, q2) with
| (p_1, _) ⇒ q2
| (_, p_1) ⇒ q1
| (n_1, _) ⇒ quatNeg q2
| (_, n_1) ⇒ quatNeg q1
| (p_i, p_i) ⇒ n_1
| (p_i, n_i) ⇒ p_1
| (p_i, p_j) ⇒ p_k
| (p_i, n_j) ⇒ n_k
| (p_i, p_k) ⇒ n_j
| (p_i, n_k) ⇒ p_j
| (n_i, p_i) ⇒ p_1
| (n_i, n_i) ⇒ n_1
| (n_i, p_j) ⇒ n_k
| (n_i, n_j) ⇒ p_k
| (n_i, p_k) ⇒ p_j
| (n_i, n_k) ⇒ n_j
| (p_j, p_i) ⇒ n_k
| (p_j, n_i) ⇒ p_k
| (p_j, p_j) ⇒ n_1
| (p_j, n_j) ⇒ p_1
| (p_j, p_k) ⇒ p_i
| (p_j, n_k) ⇒ n_i
| (n_j, p_i) ⇒ p_k
| (n_j, n_i) ⇒ n_k
| (n_j, p_j) ⇒ p_1
| (n_j, n_j) ⇒ n_1
| (n_j, p_k) ⇒ n_i
| (n_j, n_k) ⇒ p_i
| (p_k, p_i) ⇒ p_j
| (p_k, n_i) ⇒ n_j
| (p_k, p_j) ⇒ n_i
| (p_k, n_j) ⇒ p_i
| (p_k, p_k) ⇒ n_1
| (p_k, n_k) ⇒ p_1
| (n_k, p_i) ⇒ n_j
| (n_k, n_i) ⇒ p_j
| (n_k, p_j) ⇒ p_i
| (n_k, n_j) ⇒ n_i
| (n_k, p_k) ⇒ p_1
| (n_k, n_k) ⇒ n_1
end.
Program Instance quat_is_monoid : Monoid Quaternion :=
{ Gzero := p_1
; Gplus := quatMul
}.
Solve All Obligations with program_simpl; destruct g; try easy; destruct h; destruct i; easy.
Program Instance quat_is_group : Group Quaternion :=
{ Gopp := quatInv }.
Solve All Obligations with program_simpl; destruct g; try easy.
Lemma quatMul_comm : ∀ (q1 q2 : Quaternion),
q1 · q2 = q2 · q1 ∨ q1 · q2 = quatNeg (q2 · q1).
Definition quat_list : list Quaternion := [p_1; p_i; p_j; p_k; n_1; n_i; n_j; n_k].
Program Instance quat_is_finitegroup : FiniteGroup Quaternion :=
{ G_list_rep := quat_list
}.