diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/IGroup.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/IGroup.v | 253 |
1 files changed, 253 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/IGroup.v b/coqprime-8.4/Coqprime/IGroup.v new file mode 100644 index 000000000..04219be5a --- /dev/null +++ b/coqprime-8.4/Coqprime/IGroup.v @@ -0,0 +1,253 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(********************************************************************** + Igroup + + Build the group of the inversible elements for the operation + + Definition: ZpGroup + **********************************************************************) +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. + +Open Scope Z_scope. + +Section IG. + +Variable A: Set. +Variable op: A -> A -> A. +Variable support: list A. +Variable e: A. + +Hypothesis A_dec: forall a b: A, {a = b} + {a <> b}. +Hypothesis support_ulist: ulist support. +Hypothesis e_in_support: In e support. +Hypothesis op_internal: forall a b, In a support -> In b support -> In (op a b) support. +Hypothesis op_assoc: forall a b c, In a support -> In b support -> In c support -> op a (op b c) = op (op a b) c. +Hypothesis e_is_zero_l: forall a, In a support -> op e a = a. +Hypothesis e_is_zero_r: forall a, In a support -> op a e = a. + +(************************************** + is_inv_aux tests if there is an inverse of a for op in l + **************************************) + +Fixpoint is_inv_aux (l: list A) (a: A) {struct l}: bool := + match l with nil => false | cons b l1 => + if (A_dec (op a b) e) then if (A_dec (op b a) e) then true else is_inv_aux l1 a else is_inv_aux l1 a + end. + +Theorem is_inv_aux_false: forall b l, (forall a, (In a l) -> op b a <> e \/ op a b <> e) -> is_inv_aux l b = false. +intros b l; elim l; simpl; auto. +intros a l1 Rec H; case (A_dec (op a b) e); case (A_dec (op b a) e); auto. +intros H1 H2; case (H a); auto; intros H3; case H3; auto. +Qed. + +(************************************** + is_inv tests if there is an inverse in support + **************************************) +Definition is_inv := is_inv_aux support. + +(************************************** + isupport_aux returns the sublist of inversible element of support + **************************************) + +Fixpoint isupport_aux (l: list A) : list A := + match l with nil => nil | cons a l1 => if is_inv a then a::isupport_aux l1 else isupport_aux l1 end. + +(************************************** + Some properties of isupport_aux + **************************************) + +Theorem isupport_aux_is_inv_true: forall l a, In a (isupport_aux l) -> is_inv a = true. +intros l a; elim l; simpl; auto. +intros b l1 H; case_eq (is_inv b); intros H1; simpl; auto. +intros [H2 | H2]; subst; auto. +Qed. + +Theorem isupport_aux_is_in: forall l a, is_inv a = true -> In a l -> In a (isupport_aux l). +intros l a; elim l; simpl; auto. +intros b l1 Rec H [H1 | H1]; subst. +rewrite H; auto with datatypes. +case (is_inv b); auto with datatypes. +Qed. + + +Theorem isupport_aux_not_in: + forall b l, (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> ~ In b (isupport_aux l). +intros b l; elim l; simpl; simpl; auto. +intros a l1 H; case_eq (is_inv a); intros H1; simpl; auto. +intros H2 [H3 | H3]; subst. +contradict H1. +unfold is_inv; rewrite is_inv_aux_false; auto. +case H; auto; apply isupport_aux_is_in; auto. +Qed. + +Theorem isupport_aux_incl: forall l, incl (isupport_aux l) l. +intros l; elim l; simpl; auto with datatypes. +intros a l1 H1; case (is_inv a); auto with datatypes. +Qed. + +Theorem isupport_aux_ulist: forall l, ulist l -> ulist (isupport_aux l). +intros l; elim l; simpl; auto with datatypes. +intros a l1 H1 H2; case_eq (is_inv a); intros H3; auto with datatypes. +apply ulist_cons; auto with datatypes. +intros H4; apply (ulist_app_inv _ (a::nil) l1 a); auto with datatypes. +apply (isupport_aux_incl l1 a); auto. +apply H1; apply ulist_app_inv_r with (a:: nil); auto. +apply H1; apply ulist_app_inv_r with (a:: nil); auto. +Qed. + +(************************************** + isupport is the sublist of inversible element of support + **************************************) + +Definition isupport := isupport_aux support. + +(************************************** + Some properties of isupport + **************************************) + +Theorem isupport_is_inv_true: forall a, In a isupport -> is_inv a = true. +unfold isupport; intros a H; apply isupport_aux_is_inv_true with (1 := H). +Qed. + +Theorem isupport_is_in: forall a, is_inv a = true -> In a support -> In a isupport. +intros a H H1; unfold isupport; apply isupport_aux_is_in; auto. +Qed. + +Theorem isupport_incl: incl isupport support. +unfold isupport; apply isupport_aux_incl. +Qed. + +Theorem isupport_ulist: ulist isupport. +unfold isupport; apply isupport_aux_ulist. +apply support_ulist. +Qed. + +Theorem isupport_length: (length isupport <= length support)%nat. +apply ulist_incl_length. +apply isupport_ulist. +apply isupport_incl. +Qed. + +Theorem isupport_length_strict: + forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> + (length isupport < length support)%nat. +intros b H H1; apply ulist_incl_length_strict. +apply isupport_ulist. +apply isupport_incl. +intros H2; case (isupport_aux_not_in b support); auto. +Qed. + +Fixpoint inv_aux (l: list A) (a: A) {struct l}: A := + match l with nil => e | cons b l1 => + if A_dec (op a b) e then if (A_dec (op b a) e) then b else inv_aux l1 a else inv_aux l1 a + end. + +Theorem inv_aux_prop_r: forall l a, is_inv_aux l a = true -> op a (inv_aux l a) = e. +intros l a; elim l; simpl. +intros; discriminate. +intros b l1 H1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros H3 H4; subst; auto. +Qed. + +Theorem inv_aux_prop_l: forall l a, is_inv_aux l a = true -> op (inv_aux l a) a = e. +intros l a; elim l; simpl. +intros; discriminate. +intros b l1 H1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros H3 H4; subst; auto. +Qed. + +Theorem inv_aux_inv: forall l a b, op a b = e -> op b a = e -> (In a l) -> is_inv_aux l b = true. +intros l a b; elim l; simpl. +intros _ _ H; case H. +intros c l1 Rec H H0 H1; case H1; clear H1; intros H1; subst; rewrite H. +case (A_dec (op b a) e); case (A_dec e e); auto. +intros H1 H2; contradict H2; rewrite H0; auto. +case (A_dec (op b c) e); case (A_dec (op c b) e); auto. +Qed. + +Theorem inv_aux_in: forall l a, In (inv_aux l a) l \/ inv_aux l a = e. +intros l a; elim l; simpl; auto. +intros b l1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros _ _ [H1 | H1]; auto. +Qed. + +(************************************** + The inverse function + **************************************) + +Definition inv := inv_aux support. + +(************************************** + Some properties of inv + **************************************) + +Theorem inv_prop_r: forall a, In a isupport -> op a (inv a) = e. +intros a H; unfold inv; apply inv_aux_prop_r with (l := support). +change (is_inv a = true). +apply isupport_is_inv_true; auto. +Qed. + +Theorem inv_prop_l: forall a, In a isupport -> op (inv a) a = e. +intros a H; unfold inv; apply inv_aux_prop_l with (l := support). +change (is_inv a = true). +apply isupport_is_inv_true; auto. +Qed. + +Theorem is_inv_true: forall a b, op b a = e -> op a b = e -> (In a support) -> is_inv b = true. +intros a b H H1 H2; unfold is_inv; apply inv_aux_inv with a; auto. +Qed. + +Theorem is_inv_false: forall b, (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> is_inv b = false. +intros b H; unfold is_inv; apply is_inv_aux_false; auto. +Qed. + +Theorem inv_internal: forall a, In a isupport -> In (inv a) isupport. +intros a H; apply isupport_is_in. +apply is_inv_true with a; auto. +apply inv_prop_l; auto. +apply inv_prop_r; auto. +apply (isupport_incl a); auto. +case (inv_aux_in support a); unfold inv; auto. +intros H1; rewrite H1; apply e_in_support; auto with zarith. +Qed. + +(************************************** + We are now ready to build our group + **************************************) + +Definition IGroup : (FGroup op). +generalize (fun x=> (isupport_incl x)); intros Hx. +apply mkGroup with (s := isupport) (e := e) (i := inv); auto. +apply isupport_ulist. +intros a b H H1. +assert (Haii: In (inv a) isupport); try apply inv_internal; auto. +assert (Hbii: In (inv b) isupport); try apply inv_internal; auto. +apply isupport_is_in; auto. +apply is_inv_true with (op (inv b) (inv a)); auto. +rewrite op_assoc; auto. +rewrite <- (op_assoc a); auto. +rewrite inv_prop_r; auto. +rewrite e_is_zero_r; auto. +apply inv_prop_r; auto. +rewrite <- (op_assoc (inv b)); auto. +rewrite (op_assoc (inv a)); auto. +rewrite inv_prop_l; auto. +rewrite e_is_zero_l; auto. +apply inv_prop_l; auto. +apply isupport_is_in; auto. +apply is_inv_true with e; auto. +intros a H; apply inv_internal; auto. +intros; apply inv_prop_l; auto. +intros; apply inv_prop_r; auto. +Defined. + +End IG. |