Skip to content

Instantly share code, notes, and snippets.

@y-taka-23

y-taka-23/coq_mlattice.v

Created December 22, 2012 17:10
Show Gist options
  • Save y-taka-23/4359976 to your computer and use it in GitHub Desktop.
Save y-taka-23/4359976 to your computer and use it in GitHub Desktop.
Download ZIP
An Example of Modular Lattices (The Lattice of Normal Subgroups of a Group)
Raw
coq_mlattice.v
(******************************************************)
(** //// Modular Lattices //// *)
(******************************************************)
Section ModularLattice.
Require Import Relation_Definitions Setoid Morphisms.
(*////////////////////////////////////////////////////*)
(** Axioms *)
(*////////////////////////////////////////////////////*)
(* Axiom : Partially ordered set *)
Class POSet (S : Type) (eq : S -> S -> Prop)
(le : S -> S -> Prop) := {
POS_equiv :>
Equivalence eq;
POS_le_mor :
forall x x' : S, eq x x' ->
forall y y' : S, eq y y' ->
le x y -> le x' y';
POS_le_refl :
forall x : S,
le x x;
POS_le_trans :
forall x y z : S,
le x y -> le y z -> le x z;
POS_le_antisym :
forall x y : S,
le x y -> le y x -> eq x y
}.
(* Axiom : Lattice *)
Class Lattice (L : Type) (eq : L -> L -> Prop)
(le : L -> L -> Prop)
(sup : L -> L -> L) (inf : L -> L -> L) := {
L_POSset :>
POSet L eq le;
L_sup_mor :
forall x x' : L, eq x x' ->
forall y y' : L, eq y y' ->
eq (sup x y) (sup x' y');
L_inf_mor :
forall x x' : L, eq x x' ->
forall y y' : L, eq y y' ->
eq (inf x y) (inf x' y');
L_sup_l :
forall x y : L,
le x (sup x y);
L_sup_r :
forall x y : L,
le y (sup x y);
L_sup_min :
forall x y z : L,
le x z -> le y z -> le (sup x y) z;
L_inf_l :
forall x y : L,
le (inf x y) x;
L_inf_r :
forall x y : L,
le (inf x y) y;
L_inf_max :
forall x y z : L,
le z x -> le z y -> le z (inf x y)
}.
(* Axiom : Modular Lattice *)
Class ModularLattice (L : Type) (eq : L -> L -> Prop)
(le : L -> L -> Prop)
(sup : L -> L -> L) (inf : L -> L -> L) := {
ML_Lattice :>
Lattice L eq le sup inf;
ML_mod :
forall x y z : L,
le x z -> eq (sup x (inf y z)) (inf (sup x y) z)
}.
(* Axiom : Group *)
Class Group (G : Type) (eq : G -> G -> Prop)
(op : G -> G -> G) (unit : G) (inv : G -> G) := {
G_equiv :>
Equivalence eq;
G_op_mor :
forall x x' : G, eq x x' ->
forall y y' : G, eq y y' ->
eq (op x y) (op x' y');
G_inv_mor :
forall x x' : G,
eq x x' -> eq (inv x) (inv x');
G_op_assoc :
forall x y z : G,
eq (op x (op y z)) (op (op x y) z);
G_unit_l :
forall x : G,
eq (op unit x) x;
G_unit_r :
forall x : G,
eq (op x unit) x;
G_inv_l :
forall x : G,
eq (op (inv x) x) unit;
G_inv_r :
forall x : G,
eq (op x (inv x)) unit
}.
(* Axiom : Subsetoid *)
Class Subsetoid {X : Type} {eq : X -> X -> Prop}
(S : X -> Prop) := {
SS_mor :
forall x x' : X,
eq x x' -> (S x <-> S x')
}.
(* Axiom : Subgroup *)
Class Subgroup {G : Type} {eq : G -> G -> Prop}
{op : G -> G -> G} {unit : G} {inv : G -> G}
(H : G -> Prop) := {
SG_outer_Group :>
Group G eq op unit inv;
SG_Subsetoid :>
@Subsetoid G eq H;
SG_unit_in :
H unit;
SG_op_clo :
forall x y : G,
H x -> H y -> H (op x y);
SG_inv_clo :
forall x : G,
H x -> H (inv x)
}.
(* Axiom : Normal Subgroup *)
Class NormalSubgroup {G : Type} {eq : G -> G -> Prop}
{op : G -> G -> G} {unit : G} {inv : G -> G}
(H : G -> Prop) := {
NSG_Subgroup :>
@Subgroup G eq op unit inv H;
NSG_normal :
forall x y : G,
H x -> H (op (op y x) (inv y))
}.
(* Assumption : G is a group. *)
Variable G : Type.
Variable Geq : G -> G -> Prop.
Variable Gop : G -> G -> G.
Variable Gunit : G.
Variable Ginv : G -> G.
Hypothesis G_Group : Group G Geq Gop Gunit Ginv.
Notation "x |=| y" := (Geq x y)
(at level 70, no associativity).
Notation "x |*| y" := (Gop x y)
(at level 40, left associativity).
Notation "|/| x" := (Ginv x)
(at level 35, right associativity).
Notation "x |/| y" := (Gop x (Ginv y))
(at level 40, left associativity).
(* Reflexivity of Geq *)
Lemma Geq_refl : forall x : G, x |=| x.
Proof.
apply G_Group.
Qed.
(* Symmetricity of Geq *)
Lemma Geq_sym : forall x y : G, x |=| y -> y |=| x.
Proof.
apply G_Group.
Qed.
(* Transitivity of Geq *)
Lemma Geq_trans : forall x y z : G, x |=| y -> y |=| z -> x |=| z.
Proof.
apply G_Group.
Qed.
(* Well-definedness of G as a setoid *)
Add Parametric Relation : G Geq
reflexivity proved by Geq_refl
symmetry proved by Geq_sym
transitivity proved by Geq_trans
as G_Setoid.
(* Well-definedness of Gop *)
Add Parametric Morphism : Gop with signature (Geq ==> Geq ==> Geq)
as Gop_mor.
Proof.
apply G_Group.
Qed.
(* Well-definedness of Ginv *)
Add Parametric Morphism : Ginv with signature (Geq ==> Geq)
as Ginv_mor.
Proof.
apply G_Group.
Qed.
(* Definition : Subsets of G (as characteristic functions) *)
Definition CF : Type := G -> Prop.
(* Definition : *)
(* Normal Subgroups of G (Underlying set of the lattice) *)
Definition NSG : Type :=
{N : CF | @NormalSubgroup G Geq Gop Gunit Ginv N}.
(* Definition : *)
(* Equivalency of normal subgroups (by extensionality) *)
Definition NSGeq (N N' : NSG) : Prop :=
let N := proj1_sig N in
let N' := proj1_sig N' in
forall x : G, N x <-> N' x.
Notation "N [=] N'" := (NSGeq N N')
(at level 70, no associativity).
(* Reflexivity of NSGeq *)
Lemma NSGeq_refl : forall N : NSG, N [=] N.
Proof.
intro N.
destruct N as [N H_N].
unfold NSGeq.
simpl.
reflexivity.
Qed.
(* Symmetricity of NSGeq *)
Lemma NSGeq_sym : forall N N' : NSG, N [=] N' -> N' [=] N.
Proof.
intros N N'.
destruct N as [N H_N].
destruct N' as [N' H_N'].
unfold NSGeq.
simpl.
intros H x.
symmetry.
apply H.
Qed.
(* Transitivity of NSGeq *)
Lemma NSGeq_trans : forall N N' N'' : NSG,
N [=] N' -> N' [=] N'' -> N [=] N''.
Proof.
intros N N' N''.
destruct N as [N H_N].
destruct N' as [N' H_N'].
destruct N'' as [N'' H_N''].
unfold NSGeq.
simpl.
intros H_1 H_2 x.
transitivity (N' x).
(* N x <-> N' x *)
apply H_1.
(* N' x <-> N'' x *)
apply H_2.
Qed.
(* Well-definedness of NSG as a setoid *)
Add Parametric Relation : NSG NSGeq
reflexivity proved by NSGeq_refl
symmetry proved by NSGeq_sym
transitivity proved by NSGeq_trans
as NSG_Setoid.
(* Definition : Ordering on normal subgroups (by inclusion) *)
Definition NSGle (N1 N2 : NSG) : Prop :=
let N1 := proj1_sig N1 in
let N2 := proj1_sig N2 in
forall x : G, N1 x -> N2 x.
Notation "N1 [<=] N2" := (NSGle N1 N2)
(at level 70, no associativity).
(* Well-definedness of NSGle *)
Add Parametric Morphism : NSGle
with signature (NSGeq ==> NSGeq ==> iff)
as NSGle_mor.
Proof.
intros N1 N1' H_1 N2 N2' H_2.
destruct N1 as [N1 H_N1].
destruct N1' as [N1' H_N1'].
destruct N2 as [N2 H_N2].
destruct N2' as [N2' H_N2'].
unfold NSGeq in *.
unfold NSGle.
simpl in *.
split.
(* Direction -> *)
intros H x H_x.
apply H_2.
apply H.
apply H_1.
assumption.
(* Direction -> *)
intros H x H_x.
apply H_2.
apply H.
apply H_1.
assumption.
Qed.
(* Reflexivity of NSGle *)
Lemma NSGle_refl : forall N : NSG, N [<=] N.
Proof.
intro N.
destruct N as [N H_N].
unfold NSGle.
simpl.
trivial.
Qed.
(* Transitivity of NSGle *)
Lemma NSGle_trans : forall N1 N2 N3 : NSG,
N1 [<=] N2 -> N2 [<=] N3 -> N1 [<=] N3.
Proof.
intros N1 N2 N3 H_12 H_23.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
destruct N3 as [N3 H_N3].
unfold NSGle in *.
simpl in *.
intros x H.
apply H_23.
apply H_12.
assumption.
Qed.
(* Anti-symmetricity of NSGle *)
Lemma NSGle_antisym : forall N1 N2 : NSG,
N1 [<=] N2 -> N2 [<=] N1 -> N1 [=] N2.
Proof.
intros N1 N2 H_12 H_21.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
unfold NSGeq in *.
unfold NSGle in *.
simpl in *.
split.
(* Direction -> *)
intros H_x.
apply H_12.
assumption.
(* Direction <- *)
intros H_x.
apply H_21.
assumption.
Qed.
(* NSG is a partially ordered set. *)
Instance NSG_POSet : POSet NSG NSGeq NSGle.
Proof.
apply Build_POSet.
(* Equivalency of NSGseq *)
apply NSG_Setoid.
(* Well-definedness of NSGsle *)
apply NSGle_mor.
(* Reflexivity of NSGsle*)
apply NSGle_refl.
(* Transitivity of NSGsle*)
apply NSGle_trans.
(* Anti-symmetricity of NSGsle*)
apply NSGle_antisym.
Defined.
(* Definition : Product of the subsets of G *)
Definition CFprod (S1 S2 : CF) : CF :=
fun x => exists s1 : G, exists s2 : G,
S1 s1 /\ S2 s2 /\ x |=| s1 |*| s2.
Notation "S1 (.) S2" := (CFprod S1 S2)
(at level 40, left associativity).
(* Well-definedness of CFprod under Geq *)
Lemma CFprod_mor : forall (S1 S2 : CF) (x x' : G),
x |=| x' -> ((S1 (.) S2) x <-> (S1 (.) S2) x').
Proof.
intros S1 S2 x x' H_x.
split.
(* Direction -> *)
intro H.
unfold CFprod in *.
destruct H as [x1 H].
destruct H as [x2 H].
exists x1.
exists x2.
rewrite <- H_x.
assumption.
(* Direction -> *)
intro H.
unfold CFprod in *.
destruct H as [x1 H].
destruct H as [x2 H].
exists x1.
exists x2.
rewrite H_x.
assumption.
Qed.
(* If S1 and S2 are subgroups, Gunit is in S1 (.) S2. *)
Lemma SGprod_unit_in : forall S1 S2 : CF,
@Subgroup G Geq Gop Gunit Ginv S1 ->
@Subgroup G Geq Gop Gunit Ginv S2 ->
(S1 (.) S2) Gunit.
Proof.
intros S1 S2 H_S1 H_S2.
unfold CFprod.
exists Gunit.
exists Gunit.
repeat split.
(* Gunit is in S1. *)
apply H_S1.
(* Gunit is in S2. *)
apply H_S2.
(* Gunit |=| Gunit |*| Gunit *)
rewrite G_unit_l.
reflexivity.
Qed.
(* If N1 and N2 are normal subgroups, *)
(* N1 (.) N2 is closed under Gop. *)
Lemma NSGprod_op_clo : forall (N1 N2 : CF) (x y : G),
@NormalSubgroup G Geq Gop Gunit Ginv N1 ->
@NormalSubgroup G Geq Gop Gunit Ginv N2 ->
(N1 (.) N2) x -> (N1 (.) N2) y ->
(N1 (.) N2) (x |*| y).
Proof.
intros N1 N2 x y H_N1 H_N2 H_x H_y.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
destruct H_y as [y1 H_y].
destruct H_y as [y2 H_y].
exists (x1 |*| x2 |*| y1 |/| x2).
exists (x2 |*| y2).
repeat split.
(* x1 |*| x2 |*| y1 |/| x2 is in N1. *)
assert (x1 |*| x2 |*| y1 |/| x2 |=|
x1 |*| (x2 |*| y1 |/| x2)) as H.
(* Proof of the assertion *)
repeat rewrite G_op_assoc.
reflexivity.
apply (SS_mor (x1 |*| x2 |*| y1 |/| x2)
(x1 |*| (x2 |*| y1 |/| x2))).
(* x1 |*| x2 |*| y1 |/| x2 |=|
x1 |*| (x2 |*| y1 |/| x2)) *)
assumption.
(* (x1 |*| (x2 |*| y1 |/| x2)) is in N1. *)
apply SG_op_clo.
(* x1 is in N1. *)
apply H_x.
(* x2 |*| y1 |/| x2 is in N1. *)
apply NSG_normal.
(* y1 is in N1. *)
apply H_y.
(* x2 |*| y2 is in N2. *)
apply H_N2.
(* x2 is in N2. *)
apply H_x.
(* y2 is in N2. *)
apply H_y.
(* x |*| y |=| x1 |*| x2 |*| y1 |/| x2 |*| (x2 |*| y2) *)
repeat destruct H_x as [_ H_x].
repeat destruct H_y as [_ H_y].
rewrite H_x.
rewrite H_y.
assert (x1 |*| x2 |*| y1 |/| x2 |*| (x2 |*| y2) |=|
x1 |*| x2 |*| y1 |*| (|/| x2 |*| x2 |*| y2)) as H.
(* Proof of the assertion *)
repeat rewrite G_op_assoc.
reflexivity.
rewrite G_inv_l in H.
rewrite G_unit_l in H.
rewrite H.
repeat rewrite G_op_assoc.
reflexivity.
Qed.
(* The right inverses uniquly exist. *)
Lemma Ginv_unique_r : forall x y : G,
x |*| y |=| Gunit -> y |=| |/| x.
Proof.
intros x y H_xy.
assert (y |=| |/| x |*| (x |*| y)) as H.
(* Proof of the assertion *)
rewrite G_op_assoc.
rewrite G_inv_l.
rewrite G_unit_l.
reflexivity.
rewrite H_xy in H.
rewrite G_unit_r in H.
assumption.
Qed.
(* The inverse of the product is *)
(* the opposite product of the inverses. *)
Lemma Ginv_Gop_opp : forall x y : G,
|/| (x |*| y) |=| |/| y |/| x.
Proof.
intros x y.
symmetry.
apply Ginv_unique_r.
assert (x |*| y |*| (|/| y |/| x) |=|
x |*| (y |*| |/| y) |/| x) as H.
(* Proof of the assertion *)
repeat rewrite G_op_assoc.
reflexivity.
rewrite H.
rewrite G_inv_r.
rewrite G_unit_r.
rewrite G_inv_r.
reflexivity.
Qed.
(* If N1 and N2 are normal subgroups, *)
(* N1 (.) N2 is closed under Ginv. *)
Lemma NSGprod_inv_clo : forall (N1 N2 : CF) (x : G),
@NormalSubgroup G Geq Gop Gunit Ginv N1 ->
@NormalSubgroup G Geq Gop Gunit Ginv N2 ->
(N1 (.) N2) x -> (N1 (.) N2) (|/| x).
Proof.
intros N1 N2 x H_N1 H_N2 H_x.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
exists (|/| x1).
exists (x1 |/| x2 |/| x1).
repeat split.
(* |/| x1 is in N1. *)
apply H_N1.
apply H_x.
(* x1 |/| x2 |/| x1 is in N2. *)
apply NSG_normal.
apply H_N2.
apply H_x.
(* |/| x |=| |/| x1 |*| (x1 |/| x2 |/| x1) *)
repeat destruct H_x as [_ H_x].
rewrite H_x.
rewrite Ginv_Gop_opp.
repeat rewrite G_op_assoc.
rewrite G_inv_l.
rewrite G_unit_l.
reflexivity.
Qed.
(* If N1 and N2 are normal subgroups, *)
(* N1 (.) N2 is a normal subgroup. *)
Lemma NSGprod_normal : forall (N1 N2 : CF) (x y : G),
@NormalSubgroup G Geq Gop Gunit Ginv N1 ->
@NormalSubgroup G Geq Gop Gunit Ginv N2 ->
(N1 (.) N2) x ->
(N1 (.) N2) (y |*| x |/| y).
Proof.
intros N1 N2 x y H_N1 H_N2 H_x.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
exists (y |*| x1 |/| y).
exists (y |*| x2 |/| y).
repeat split.
(* y |*| x1 |/| y is in N1. *)
apply NSG_normal.
apply H_x.
(* y |*| x2 |/| y is in N2. *)
apply NSG_normal.
apply H_x.
(* y |*| x |/| y |=| y |*| x1 |/| y |*| (y |*| x2 |/| y) *)
repeat destruct H_x as [_ H_x].
rewrite H_x.
assert (x1 |*| x2 |=| x1 |*| (|/| y |*| y) |*| x2) as H.
(* Proof of the assertion *)
rewrite G_inv_l.
rewrite G_unit_r.
reflexivity.
rewrite H.
repeat rewrite G_op_assoc.
reflexivity.
Qed.
(* Definition : sup on NSG (by product of the normal subgroups) *)
Definition NSGsup (N1 N2 : NSG) : NSG.
Proof.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
exists (N1 (.) N2).
apply Build_NormalSubgroup.
(* N1 (.) N2 is a subgroup. *)
apply Build_Subgroup.
(* G is a group. *)
apply G_Group.
(* N1 (.) N2 is a subsetoid of G. *)
apply Build_Subsetoid.
(* Well-definedness of CFprod *)
apply CFprod_mor.
(* Gunit is in N1 (.) N2. *)
apply SGprod_unit_in.
(* N1 is a subgroup. *)
apply H_N1.
(* N2 is a subgroup. *)
apply H_N2.
(* N1 (.) N2 is closed under Gop. *)
intros x y.
apply NSGprod_op_clo.
(* N1 is normal. *)
assumption.
(* N2 is normal. *)
assumption.
(* N1 (.) N2 is closed under Ginv. *)
intro x.
apply NSGprod_inv_clo.
(* N1 is normal. *)
assumption.
(* N2 is normal. *)
assumption.
(* Normality of N1 (.) N2 *)
intros x y.
apply NSGprod_normal.
(* N1 is normal. *)
assumption.
(* N2 is normal. *)
assumption.
Defined.
Notation "N1 [\/] N2" := (NSGsup N1 N2)
(at level 50, left associativity).
(* Definition : Intersection of the subsets of G *)
Definition CFint (S1 S2 : CF) : CF := fun x => S1 x /\ S2 x.
Notation "S1 (/\) S2" := (CFint S1 S2)
(at level 45, left associativity).
(* If S1 and S2 are subsetoids, CFint is well-defined under Geq. *)
Lemma CFint_mor : forall (S1 S2 : CF) (x x' : G),
@Subsetoid G Geq S1 -> @Subsetoid G Geq S2 ->
x |=| x' -> ((S1 (/\) S2) x <-> (S1 (/\) S2) x').
Proof.
intros S1 S2 x x' H_S1 H_S2 H_x.
destruct H_S1 as [H_S1].
destruct H_S2 as [H_S2].
split.
(* Direction -> *)
intro H.
unfold CFint in *.
split.
(* x' is in S1. *)
specialize H_S1 with x x'.
apply H_S1.
(* x |=| x' *)
assumption.
(* x is in S1. *)
apply H.
(* x' os om S2. *)
specialize H_S2 with x x'.
apply H_S2.
(* x |=| x' *)
assumption.
(* x is in S2. *)
apply H.
(* Direction <- *)
intro H.
unfold CFint in *.
split.
(* x' is in S1. *)
specialize H_S1 with x x'.
apply H_S1.
(* x |=| x' *)
assumption.
(* x is in S1. *)
apply H.
(* x' os om S2. *)
specialize H_S2 with x x'.
apply H_S2.
(* x |=| x' *)
assumption.
(* x is in S2. *)
apply H.
Qed.
(* If S1 and S2 are subgroups, Gunit is in S1 (/\) S2. *)
Lemma SGint_unit_in : forall (S1 S2 : CF),
@Subgroup G Geq Gop Gunit Ginv S1 ->
@Subgroup G Geq Gop Gunit Ginv S2 ->
(S1 (/\) S2) Gunit.
Proof.
intros S1 S2 H_S1 H_S2.
unfold CFint.
split.
(* Gunit is in S1. *)
apply H_S1.
(* Gunit is in S2. *)
apply H_S2.
Qed.
(* If S1 and S2 are subgroups, S1 (/\) S1 is closed under Gop. *)
Lemma SGint_op_clo : forall (S1 S2 : CF) (x y : G),
@Subgroup G Geq Gop Gunit Ginv S1 ->
@Subgroup G Geq Gop Gunit Ginv S2 ->
(S1 (/\) S2) x -> (S1 (/\) S2) y ->
(S1 (/\) S2) (x |*| y).
Proof.
intros S1 S2 x y H_S1 H_S2 H_x H_y.
unfold CFint in *.
split.
(* x |*| y is in S1. *)
apply H_S1.
(* x is in S1. *)
apply H_x.
(* y is in S1. *)
apply H_y.
(* x |*| y is in S2. *)
apply H_S2.
(* x is in S1. *)
apply H_x.
(* y is in S1. *)
apply H_y.
Qed.
(* If S1 and S2 are subgroups, S1 (/\) S2 is closed under Ginv. *)
Lemma SGint_inv_clo : forall (S1 S2 : CF) (x : G),
@Subgroup G Geq Gop Gunit Ginv S1 ->
@Subgroup G Geq Gop Gunit Ginv S2 ->
(S1 (/\) S2) x -> (S1 (/\) S2) (|/| x).
Proof.
intros S1 S2 x H_S1 H_S2 H_x.
unfold CFint in *.
split.
(* |/| x is in S1. *)
apply H_S1.
apply H_x.
(* |/| x is in S2. *)
apply H_S2.
apply H_x.
Qed.
(* If N1 and N2 are normal subgroups, *)
(* S1 (/\) S2 is a normal subgroup. *)
Lemma NSGint_normal : forall (N1 N2 : CF) (x y : G),
@NormalSubgroup G Geq Gop Gunit Ginv N1 ->
@NormalSubgroup G Geq Gop Gunit Ginv N2 ->
(N1 (/\) N2) x ->
(N1 (/\) N2) (y |*| x |/| y).
Proof.
intros N1 N2 x y H_N1 H_N2 H_x.
unfold CFint in *.
split.
(* y |*| x |/| y is in N1. *)
apply NSG_normal.
apply H_x.
(* y |*| x |/| y is in N2. *)
apply NSG_normal.
apply H_x.
Qed.
(* Definition : *)
(* inf on NSG (by intersection of the normal subgroups) *)
Definition NSGinf (N1 N2 : NSG) : NSG.
Proof.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
exists (N1 (/\) N2).
apply Build_NormalSubgroup.
(* N1 (/\) N2 is a subgroup. *)
apply Build_Subgroup.
(* G is a group. *)
apply G_Group.
(* N1 (/\) N2 is a subsetoid. *)
apply Build_Subsetoid.
(* Well-definedness of CFint *)
intros x x'.
apply CFint_mor.
(* N1 is a subsetoid. *)
apply H_N1.
(* N2 is a subsetoid. *)
apply H_N2.
(* Gunit is in N1 (/\) N2. *)
apply SGint_unit_in.
(* N1 is a subgroup. *)
apply H_N1.
(* N2 is a subgroup. *)
apply H_N2.
(* N1 (/\) N2 is closed under Gop. *)
intros x y.
apply SGint_op_clo.
(* N1 is a subgroup. *)
apply H_N1.
(* N2 is a subgroup. *)
apply H_N2.
(* N1 (/\) N2 is closed under Ginv. *)
intro x.
apply SGint_inv_clo.
(* N1 is a subgroup. *)
apply H_N1.
(* N2 is a subgroup. *)
apply H_N2.
(* Normality of N1 (/\) N2 *)
intros x y.
apply NSGint_normal.
(* N1 is normal. *)
assumption.
(* N2 is normal. *)
assumption.
Defined.
Notation "N1 [/\] N2" := (NSGinf N1 N2)
(at level 40, left associativity).
(* Well-definedness of NSGsup *)
Add Parametric Morphism : NSGsup
with signature (NSGeq ==> NSGeq ==> NSGeq)
as NSGsup_mor.
Proof.
intros N1 N1' H_1 N2 N2' H_2.
destruct N1 as [N1 H_N1].
destruct N1' as [N1' H_N1'].
destruct N2 as [N2 H_N2].
destruct N2' as [N2' H_N2'].
unfold NSGsup.
unfold NSGeq.
simpl.
intro x.
split.
(* Direction -> *)
intro H_x.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
exists x1.
exists x2.
repeat split.
(* x1 is in N1' *)
apply H_1.
apply H_x.
(* x2 is in N2' *)
apply H_2.
apply H_x.
(* x |=| x1 |*| x2 *)
apply H_x.
(* Direction <- *)
intro H_x.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
exists x1.
exists x2.
repeat split.
(* x1 is in N1 *)
apply H_1.
apply H_x.
(* x2 is in N2 *)
apply H_2.
apply H_x.
(* x |=| x1 |*| x2 *)
apply H_x.
Qed.
(* Well-definedness of NSGinf *)
Add Parametric Morphism : NSGinf
with signature (NSGeq ==> NSGeq ==> NSGeq)
as NSGinf_mor.
Proof.
intros N1 N1' H_1 N2 N2' H_2.
destruct N1 as [N1 H_N1].
destruct N1' as [N1' H_N1'].
destruct N2 as [N2 H_N2].
destruct N2' as [N2' H_N2'].
unfold NSGinf.
unfold NSGeq.
simpl.
intro x.
split.
(* Direction -> *)
intro H_x.
unfold CFint in *.
split.
(* x is in N1'. *)
apply H_1.
apply H_x.
(* x is in N2'. *)
apply H_2.
apply H_x.
(* Direction <- *)
intro H_x.
unfold CFint in *.
split.
(* x is in N1. *)
apply H_1.
apply H_x.
(* x is in N2. *)
apply H_2.
apply H_x.
Qed.
(* Property as the sup function (1) *)
Lemma NSGsup_l : forall N1 N2 : NSG, N1 [<=] N1 [\/] N2.
Proof.
intros N1 N2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFprod.
exists x.
exists Gunit.
repeat split.
(* x is in N1. *)
assumption.
(* Gunit is in N2. *)
apply H_N2.
(* x |=| x |*| Gunit *)
rewrite G_unit_r.
reflexivity.
Qed.
(* Property as the sup function (2) *)
Lemma NSGsup_r : forall N1 N2 : NSG, N2 [<=] N1 [\/] N2.
Proof.
intros N1 N2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFprod.
exists Gunit.
exists x.
repeat split.
(* Gunit is in N1. *)
apply H_N1.
(* x is in N2. *)
assumption.
(* x |=| Gunit |*| x *)
rewrite G_unit_l.
reflexivity.
Qed.
(* Property as the sup function (3) *)
Lemma NSGsup_min : forall N1 N2 N3 : NSG,
N1 [<=] N3 -> N2 [<=] N3 -> N1 [\/] N2 [<=] N3.
Proof.
intros N1 N2 N3 H_1 H_2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
destruct N3 as [N3 H_N3].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFprod in *.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
apply (SS_mor x (x1 |*| x2)).
(* x |=| x1 |*| x2 *)
apply H_x.
(* x1 |*| x2 is in N3. *)
apply SG_op_clo.
(* x1 is in N3. *)
apply H_1.
apply H_x.
(* x2 is in N3. *)
apply H_2.
apply H_x.
Qed.
(* Property as the inf function (1) *)
Lemma NSGinf_l : forall N1 N2 : NSG, N1 [/\] N2 [<=] N1.
Proof.
intros N1 N2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFint in H_x.
apply H_x.
Qed.
(* Property as the inf function (2) *)
Lemma NSGinf_r : forall N1 N2 : NSG, N1 [/\] N2 [<=] N2.
Proof.
intros N1 N2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFint in H_x.
apply H_x.
Qed.
(* Property as the inf function (3) *)
Lemma NSGinf_max : forall N1 N2 N3 : NSG,
N3 [<=] N1 -> N3 [<=] N2 -> N3 [<=] N1 [/\] N2.
Proof.
intros N1 N2 N3 H_1 H_2.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
destruct N3 as [N3 H_N3].
unfold NSGsup.
unfold NSGle.
simpl.
intros x H_x.
unfold CFint.
split.
(* x is in N1. *)
apply H_1.
assumption.
(* x is in N2. *)
apply H_2.
assumption.
Qed.
(* NSG is a lattice. *)
Instance NSG_Lattice : Lattice NSG NSGeq NSGle NSGsup NSGinf.
Proof.
apply Build_Lattice.
(* NSG is a POSet. *)
apply NSG_POSet.
(* Well-definedness of NSGsup *)
apply NSGsup_mor.
(* Well-definedness of NSGinf *)
apply NSGinf_mor.
(* Sup property (1) *)
apply NSGsup_l.
(* Sup property (2) *)
apply NSGsup_r.
(* Sup property (3) *)
apply NSGsup_min.
(* Int property (1) *)
apply NSGinf_l.
(* Inf property (2) *)
apply NSGinf_r.
(* Inf property (3) *)
apply NSGinf_max.
Defined.
(* Modularity of NSG *)
Lemma NSG_mod : forall N1 N2 N3 : NSG,
N1 [<=] N3 ->
N1 [\/] (N2 [/\] N3) [=] (N1 [\/] N2) [/\] N3.
Proof.
intros N1 N2 N3 H_le.
unfold NSGeq.
intro x.
destruct N1 as [N1 H_N1].
destruct N2 as [N2 H_N2].
destruct N3 as [N3 H_N3].
unfold NSGsup.
unfold NSGinf.
unfold NSGle in H_le.
simpl in *.
split.
(* Direction -> *)
intro H_x.
unfold CFprod in H_x.
destruct H_x as [x1 H_x].
destruct H_x as [x23 H_x].
unfold CFint.
split.
(* x is in N1 (.) N2. *)
unfold CFprod.
exists x1.
exists x23.
repeat split.
(* x1 is in N1. *)
apply H_x.
(* x23 is in N2. *)
apply H_x.
(* x |=| x1 |*| x23 *)
apply H_x.
(* x is in N3. *)
apply (SS_mor x (x1 |*| x23)).
(* x |=| x1 |*| x23 *)
apply H_x.
(* x1 |*| x23 is in N3. *)
apply SG_op_clo.
(* x1 is in N3. *)
apply H_le.
apply H_x.
(* x23 is in N3. *)
apply H_x.
(* Direction <- *)
intro H_x.
destruct H_x as [H_x H_x3].
unfold CFprod in H_x.
destruct H_x as [x1 H_x].
destruct H_x as [x2 H_x].
unfold CFprod.
exists x1.
exists x2.
repeat split.
(* x1 is in N1. *)
apply H_x.
(* x2 is in N2. *)
apply H_x.
(* x2 is in N3. *)
assert (x2 |=| |/| x1 |*| x) as H.
(* Proof of the assertion *)
repeat destruct H_x as [_ H_x].
rewrite H_x.
rewrite G_op_assoc.
rewrite G_inv_l.
rewrite G_unit_l.
reflexivity.
apply (SS_mor x2 (|/| x1 |*| x)).
(* x2 |=| |/| x1 |*| x *)
assumption.
(* |/| x1 |*| x is in N3. *)
apply SG_op_clo.
(* |/| x1 is in N3. *)
apply SG_inv_clo.
apply H_le.
apply H_x.
(* x is in N3. *)
assumption.
(* x |=| x1 |*| x2 *)
apply H_x.
Qed.
(* NSG is a modular lattice. *)
Instance NSG_ModularLattice : ModularLattice NSG NSGeq NSGle
NSGsup NSGinf.
Proof.
apply Build_ModularLattice.
(* NSG is a lattice. *)
apply NSG_Lattice.
(* Modurality of NSG *)
apply NSG_mod.
Defined.
End ModularLattice.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment