Using Coq to prove Lagrange's Theorem

Using Coq
1

Hi, I am a student currently trying to prove Lagrange’s theorem using Coq, and I have run into some issues that I cannot find many resources or avenues to fix. I was hoping that someone on here could take a look at my definitions for group/subgroup/coset/finite group and provide advice on how to prove some useful theorems surrounding these things, as well as how to formulate a definition of a partition and a finite coset, as I am thinking that I will also need those to eventually prove this theorem. Here are some of the things I have already defined:

Class Group (G : Type) (op : G → G → G) (e : G) (inv : G → G) : Prop :=
{
group_associativity : forall a b c : G, op (op a b) c = op a (op b c);
group_identity_r : forall a : G, op a e = a;
group_identity_l : forall a : G, op e a = a;
group_inverse_r : forall a : G, op a (inv a) = e;
group_inverse_l : forall a : G, op (inv a) a = e;
group_inverse_identity : inv e = e;
}.

Class subgroup (H : Type) (e’ : H) := makeSubgroup{
subgroup_carrier : H → G;
subgroup_op : H → H → H;
subgroup_inv : H → H;
subgroup_identity_is_identity : subgroup_carrier e’ = e;
subgroup_closure : forall h1 h2 : H, subgroup_carrier (subgroup_op h1 h2) = op (subgroup_carrier h1) (subgroup_carrier h2);
subgroup_identity_r : forall h : H, subgroup_carrier (subgroup_op h e’) = subgroup_carrier h;
subgroup_identity_l : forall h : H, subgroup_carrier (subgroup_op e’ h) = subgroup_carrier h;
subgroup_inverse : forall h : H, subgroup_carrier(subgroup_op h (subgroup_inv h)) = e /\ subgroup_carrier(subgroup_op (subgroup_inv h) h) = e;
}.

Definition left_coset (a : G) (h : H) : Type := {x : G | exists h : H, op a ([h]) = x}.
Definition right_coset (h : H) (a : G) : Type := {x : G | exists h : H, op ([h]) a = x}.

Class FiniteGroup (G : Type) (op : G → G → G) (e : G) (inv : G → G) (card : nat) : Prop :=
{
group_assoc : forall a b c : G, op (op a b) c = op a (op b c);
group_i_r : forall a : G, op a e = a;
group_i_l : forall a : G, op e a = a;
group_inv_r : forall a : G, op a (inv a) = e;
group_inv_l : forall a : G, op (inv a) a = e;
group_inv_i : inv e = e;
group_cardinality : card > 0;
group_finite : exists l : list G, NoDup l /\ length l = card /\ forall g, In g l;
}.

Definition ListInjective (A B: Type) (f: A → B) (l: list A) :=
(forall x y: A, In x l → In y l → f x = f y → x = y).

Definition ListSurjective (A B: Type) (f: A → B) (l: list B) (l’: list A) :=
(forall x: B, In x l → exists y, In y l’ /\ f y = x).

Definition ListIsomorphism (A B: Type) (f: A → B) (l: list A) (l’: list B) :=
ListInjective A B f l /\ ListSurjective A B f l’ l.

Lemma listinjective_bounds_length (A B: Type):
forall (l1: list A) (l2: list B) (f: A → B),
ListInjective A B f l1 →
(forall c, In c l1 → In (f c) l2) →
length l1 <= length l2.
Proof.
Admitted.

Lemma listsurjective_bounds_length (A B: Type):
forall (l1: list A) (l2: list B) (f: A → B),
ListSurjective A B f l2 l1 →
length l2 <= length l1.
Proof.
Admitted.

Lemma listisomorphism_bounds_length (A B: Type):
forall (l1: list A) (l2: list B) (f: A → B),
ListIsomorphism A B f l1 l2 →
length l1 = length l2.
Proof.
Admitted.

Any tips on how to use them, or prove these Lemmas would be greatly appreciated!

2

Do not confuse lists with finite sets. For instance, listinjective_bounds_length is incorrect and here is a counter example: l1 = [1;1] l2 = [1] and f = fun n => x.

More generally, the cardinal (=number of differents elements) of a list is not its length. It is the length of the shortest list which has the same elements, or via the PHP, the length of any list with the same elements that do not contain duplicates.

The cardinal does not necessarily exist (constructivelly). For instance, if there is a cardinal for [x;y], then one can decide whether x = y (card = 1) or x <> y (card <> 1). More generally, it is necessary and sufficient that equality is decidable for the cardinal (of a list) to exist.

I suggest you study the PHP (Pigeon Hole Principle) within Coq before trying to work with the notion of cardinal of a list. For instance try to show that if l and m are two lists, “l incl m” and “length l > length m” then l must contain a duplicate.

1 Like