From ef92beece3147f8af0764521e22cb7fc9a3f32a3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 24 Feb 2018 10:17:35 -0500 Subject: coqprime in COQPATH (closes #269) --- coqprime/Coqprime/Lagrange.v | 179 ------------------------------------------- 1 file changed, 179 deletions(-) delete mode 100644 coqprime/Coqprime/Lagrange.v (limited to 'coqprime/Coqprime/Lagrange.v') diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v deleted file mode 100644 index 4765c76c4..000000000 --- a/coqprime/Coqprime/Lagrange.v +++ /dev/null @@ -1,179 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(********************************************************************** - Lagrange.v - - Proof of Lagrange theorem: - the oder of a subgroup divides the order of a group - - Definition: lagrange - **********************************************************************) -Require Import List. -Require Import UList. -Require Import ListAux. -Require Import ZArith Znumtheory. -Require Import NatAux. -Require Import FGroup. - -Open Scope Z_scope. - -Section Lagrange. - -Variable A: Set. - -Variable A_dec: forall a b: A, {a = b} + {~ a = b}. - -Variable op: A -> A -> A. - -Variable G: (FGroup op). - -Variable H:(FGroup op). - -Hypothesis G_in_H: (incl G.(s) H.(s)). - -(************************************** - A group and a subgroup have the same neutral element - **************************************) - -Theorem same_e_for_H_and_G: H.(e) = G.(e). -apply trans_equal with (op H.(e) H.(e)); sauto. -apply trans_equal with (op H.(e) (op G.(e) (H.(i) G.(e)))); sauto. -eq_tac; sauto. -apply trans_equal with (op G.(e) (op G.(e) (H.(i) G.(e)))); sauto. -repeat rewrite H.(assoc); sauto. -eq_tac; sauto. -apply trans_equal with G.(e); sauto. -apply trans_equal with (op G.(e) H.(e)); sauto. -eq_tac; sauto. -Qed. - -(************************************** - The proof works like this. - If G = {e, g1, g2, g3, .., gn} and {e, h1, h2, h3, ..., hm} - we construct the list mkGH - {e, g1, g2, g3, ...., gn - hi*e, hi * g1, hi * g2, ..., hi * gn if hi does not appear before - .... - hk*e, hk * g1, hk * g2, ..., hk * gn if hk does not appear before - } - that contains all the element of H. - We show that this list does not contain double (ulist). - **************************************) - -Fixpoint mkList (base l: (list A)) { struct l} : (list A) := - match l with - nil => nil - | cons a l1 => let r1 := mkList base l1 in - if (In_dec A_dec a r1) then r1 else - (map (op a) base) ++ r1 - end. - -Definition mkGH := mkList G.(s) H.(s). - -Theorem mkGH_length: divide (length G.(s)) (length mkGH). -unfold mkGH; elim H.(s); simpl. -exists 0%nat; auto with arith. -intros a l1 (c, H1); case (In_dec A_dec a (mkList G.(s) l1)); intros H2. -exists c; auto. -exists (1 + c)%nat; rewrite ListAux.length_app; rewrite ListAux.length_map; rewrite H1; ring. -Qed. - -Theorem mkGH_incl: incl H.(s) mkGH. -assert (H1: forall l, incl l H.(s) -> incl l (mkList G.(s) l)). -intros l; elim l; simpl; auto with datatypes. -intros a l1 H1 H2. -case (In_dec A_dec a (mkList (s G) l1)); auto with datatypes. -intros H3; assert (H4: incl l1 (mkList (s G) l1)). -apply H1; auto with datatypes. -intros b H4; apply H2; auto with datatypes. -intros b; simpl; intros [H5 | H5]; subst; auto. -intros _ b; simpl; intros [H3 | H3]; subst; auto. -apply in_or_app; left. -cut (In H.(e) G.(s)). -elim (s G); simpl; auto. -intros c l2 Hl2 [H3 | H3]; subst; sauto. -assert (In b H.(s)); sauto. -apply (H2 b); auto with datatypes. -rewrite same_e_for_H_and_G; sauto. -apply in_or_app; right. -apply H1; auto with datatypes. -apply incl_tran with (2:= H2); auto with datatypes. -unfold mkGH; apply H1; auto with datatypes. -Qed. - -Theorem incl_mkGH: incl mkGH H.(s). -assert (H1: forall l, incl l H.(s) -> incl (mkList G.(s) l) H.(s)). -intros l; elim l; simpl; auto with datatypes. -intros a l1 H1 H2. -case (In_dec A_dec a (mkList (s G) l1)); intros H3; auto with datatypes. -apply H1; apply incl_tran with (2 := H2); auto with datatypes. -apply incl_app. -intros b H4. -case ListAux.in_map_inv with (1:= H4); auto. -intros c (Hc1, Hc2); subst; sauto. -apply internal; auto with datatypes. -apply H1; apply incl_tran with (2 := H2); auto with datatypes. -unfold mkGH; apply H1; auto with datatypes. -Qed. - -Theorem ulist_mkGH: ulist mkGH. -assert (H1: forall l, incl l H.(s) -> ulist (mkList G.(s) l)). -intros l; elim l; simpl; auto with datatypes. -intros a l1 H1 H2. -case (In_dec A_dec a (mkList (s G) l1)); intros H3; auto with datatypes. -apply H1; apply incl_tran with (2 := H2); auto with datatypes. -apply ulist_app; auto. -apply ulist_map; sauto. -intros x y H4 H5 H6; apply g_cancel_l with (g:= H) (a := a); sauto. -apply H2; auto with datatypes. -apply H1; apply incl_tran with (2 := H2); auto with datatypes. -intros b H4 H5. -case ListAux.in_map_inv with (1:= H4); auto. -intros c (Hc, Hc1); subst. -assert (H6: forall l a b, In b G.(s) -> incl l H.(s) -> In a (mkList G.(s) l) -> In (op a b) (mkList G.(s) l)). -intros ll u v; elim ll; simpl; auto with datatypes. -intros w ll1 T0 T1 T2. -case (In_dec A_dec w (mkList (s G) ll1)); intros T3 T4; auto with datatypes. -apply T0; auto; apply incl_tran with (2:= T2); auto with datatypes. -case in_app_or with (1 := T4); intros T5; auto with datatypes. -apply in_or_app; left. -case ListAux.in_map_inv with (1:= T5); auto. -intros z (Hz1, Hz2); subst. -replace (op (op w z) v) with (op w (op z v)); sauto. -apply in_map; sauto. -apply assoc with H; auto with datatypes. -apply in_or_app; right; auto with datatypes. -apply T0; try apply incl_tran with (2 := T2); auto with datatypes. -case H3; replace a with (op (op a c) (G.(i) c)); auto with datatypes. -apply H6; sauto. -apply incl_tran with (2 := H2); auto with datatypes. -apply trans_equal with (op a (op c (G.(i) c))); sauto. -apply sym_equal; apply assoc with H; auto with datatypes. -replace (op c (G.(i) c)) with (G.(e)); sauto. -rewrite <- same_e_for_H_and_G. -assert (In a H.(s)); sauto; apply (H2 a); auto with datatypes. -unfold mkGH; apply H1; auto with datatypes. -Qed. - -(************************************** - Lagrange theorem - **************************************) - -Theorem lagrange: (g_order G | (g_order H)). -unfold g_order. -rewrite Permutation.permutation_length with (l := H.(s)) (m:= mkGH). -case mkGH_length; intros x H1; exists (Z_of_nat x). -rewrite H1; rewrite Zmult_comm; apply inj_mult. -apply ulist_incl2_permutation; auto. -apply ulist_mkGH. -apply mkGH_incl. -apply incl_mkGH. -Qed. - -End Lagrange. -- cgit v1.2.3