(** * Algebra: Laws of composition; associativity; commutativity Copyright INRIA (2010) Apics Team (Jose Grimm). *) Require Export algebran. Require Export algebra2. Require Export set1. Set Implicit Arguments. (* $Id: algebra3.v,v 1.37 2010/08/02 13:31:39 grimm Exp $ *) Module Mn_notation. Section Gconstruction. Variables (E:Set) (p: EEE)(z:Set) . Definition create := denote Underlying_not E (denote Plus_not (Operations.bincreate E p) (denote Zero_not z stop)). Lemma underlying_create: Ul create = E. Proof. ir. uf Ul. uf create. drw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. uf dplus. uf create. uf Ul. drw. app Operations.binary_recovers. Qed. Lemma zero_create: zero create = z. Proof. uf zero. uf create. drw. Qed. Definition struct_property:= (inc z E) & (Operations.is_law2I p E). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rww zero_create. rww underlying_create. destruct H. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. destruct H as [_ H]. red in H. red. split. red. intros. rww plus_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_plus. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. nin (is_bin_plus_create H0). am. am. app plus_create_when. Qed. End Gconstruction. Hint Rewrite underlying_create plus_create plus_create_when zero_create: mw. Lemma create_properties: forall E p z, Operations.is_law2E p E -> struct_property E p z -> (dplus (create E p z) = p). Proof. ir. ee. mw. Qed. Definition like (a:Set):= a = create (Ul a) (dplus a) (zero a). Lemma create_like: forall a, like(create (Ul a) (dplus a) (zero a)). Proof. ir. uf like. set (x:=(create (Ul a) (dplus a) (zero a))). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. sy; am. ir. rewrite H in H1,H2. mw. rw H; rw H0; rw H1. tv. Qed. Lemma like_create:forall x p z, Operations.is_law2E p x -> struct_property x p z -> like (create x p z). Proof. ir. pose (create_properties H H0). ee. red. mw. Qed. End Mn_notation. Export Mn_notation. Module Gnotation. Section Gconstruction. (* Group *) Variables (E:Set) (p: EEE)(o: EE)(z:Set) . Definition create := (denote Neg_not (Operations.uncreate E o) (Mn_notation.create E p z)). Lemma underlying_create: Ul create = E. Proof. ir. uf Ul. uf create. unfold Mn_notation.create. drw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. uf dplus. uf Ul. uf create. unfold Mn_notation.create. drw. app Operations.binary_recovers. Qed. Lemma zero_create: zero create = z. Proof. uf zero. uf create. unfold Mn_notation.create. drw. Qed. Lemma neg_create_when: forall a, inc a E -> neg create a = o a. Proof. ir. uf neg. uf create. uf Ul. unfold Mn_notation.create. drw. app Operations.unary_recovers. Qed. Definition struct_property:= (inc z E) & (Operations.is_law1I o E) & (Operations.is_law2I p E). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rw underlying_create; rww zero_create. destruct H. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. destruct H as [_ [_ H]]. red in H. red. split. red. intros. rww plus_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_plus. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) E. Proof. intros. destruct H as [_ [H _]]. red in H. red. split. red. intros. rww neg_create_when. app H. pose (H1:=underlying_create). app is_un_domain_neg. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_plus_create H0). destruct i. am. am. app plus_create_when. Qed. Lemma neg_create : Operations.is_law1E o E -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_neg_create H0). destruct i. am. am. intros. app neg_create_when. Qed. End Gconstruction. Hint Rewrite underlying_create neg_create plus_create zero_create: mw. Hint Rewrite neg_create_when plus_create_when: mw. Lemma create_properties: forall x p o z, Operations.is_law1E o x -> Operations.is_law2E p x -> struct_property x p o z -> ( (dplus (create x p o z) = p) & (neg (create x p o z) = o) ). Proof. ir. ee. mw. mw. Qed. Definition like (a:Set):= a = create (Ul a) (dplus a) (neg a) (zero a). Lemma create_like: forall a, like(create (Ul a) (dplus a) (neg a) (zero a)). Proof. ir. uf like. set (x:=(create (Ul a) (dplus a) (neg a) (zero a))). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H1. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. sy; am. ir. rewrite H in H2,H3. mw. rw H; rw H0; rw H1; rw H2. tv. Qed. Lemma like_create:forall x p o z, Operations.is_law1E o x -> Operations.is_law2E p x -> struct_property x p o z -> like (create x p o z). Proof. ir. pose (create_properties H H0 H1). ee. red. rw H2; rw H3. mw. Qed. End Gnotation. Export Gnotation. (* ************************************************** *) Module Rnotation. (* Ring construction *) Section Dconstruction. Variables (E:Set) (p:EEE)(o: EE) (z:Set)(u:Set)(m:EEE). Definition create := (denote Mult_not (Operations.bincreate E m) (denote One_not u (Gnotation.create E p o z))). Lemma underlying_create: Ul create = E. Proof. ir. transitivity (Ul (Gnotation.create E p o z)). uf Ul; uf create. drwe. tv. mw. Qed. Lemma zero_create: zero create = z. Proof. ir. transitivity (zero (Gnotation.create E p o z)). uf zero; uf create. drw. mw. Qed. Lemma neg_create_when: forall a, inc a E -> neg create a = o a. Proof. ir. transitivity (neg (Gnotation.create E p o z) a). uf create; uf neg; uf Ul. drwe. tv. mw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. transitivity (dplus (Gnotation.create E p o z) a b). uf create; uf dplus; uf Ul. drwe. tv. mw. Qed. Lemma mult_create_when: forall a b, inc a E -> inc b E -> dmult create a b = (m a b). Proof. ir. pose (underlying_create). ufi create e. uf dmult; uf create. rw e. drwe. app Operations.binary_recovers. Qed. Lemma one_create: one create = u. Proof. uf one. uf create. drw. Qed. Definition struct_property:= (inc u E) & (Operations.is_law2I m E) & (Gnotation.struct_property E p o z). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rw zero_create. rw underlying_create. destruct H. ee. destruct H1. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. destruct H as [_ [_ H]]. destruct H as [_ [_ H]]. red in H. red. split. red. intros. rww plus_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_plus. Qed. Lemma is_bin_mult_create : struct_property -> Operations.is_law2 (dmult create) E. Proof. ir. destruct H as [_ [H _]]. red in H. red. split. red. intros. rww mult_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_mult. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) E. Proof. intros. destruct H as [_ [_ H]]. destruct H as [_ [H _]]. red in H. red. split. red. intros. rww neg_create_when. app H. pose (H1:=underlying_create). app is_un_domain_neg. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_plus_create H0). destruct i. am. am. app plus_create_when. Qed. Lemma mult_create: Operations.is_law2E m E -> struct_property -> dmult create = m. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_mult_create H0). destruct i. am. am. app mult_create_when. Qed. Lemma neg_create: Operations.is_law1E o E -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_neg_create H0). destruct i. am. am. intros. app neg_create_when. Qed. End Dconstruction. Hint Rewrite underlying_create neg_create plus_create zero_create: mw. Hint Rewrite one_create neg_create_when plus_create_when: mw. Hint Rewrite mult_create mult_create_when: mw. Lemma create_properties: forall x p o z u m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> struct_property x p o z u m -> ((dplus (create x p o z u m) = p) & (dmult (create x p o z u m) = m) & (neg (create x p o z u m) = o)). Proof. ir. ee; mw. Qed. Definition like (a:Set):= a = create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a). Lemma create_like: forall a, like(create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a)). Proof. ir. uf like. set (x:= create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a)). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (one x = one a). uf x; mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H2. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. sy; am. ir. rewrite H in H3,H4. mw. assert (dmult x = dmult a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_mult. app is_bin_domain_mult. sy; am. ir. rewrite H in H4,H5. mw. rw H; rw H0; rw H1; rw H2; rw H3; rw H4. tv. Qed. Lemma like_create: forall x p o z u m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> struct_property x p o z u m -> like (create x p o z u m). Proof. ir. pose (create_properties H H0 H1 H2). ee. red. rw H3; rw H4; rw H5. mw. Qed. End Rnotation. Export Rnotation. Module Fnotation. (* Sfield notations *) Section Fconstruction. Variables (E:Set) (p:EEE)(o: EE) (z:Set)(u:Set) (m:EEE)(i:EE). Definition create := (denote Inv_not (Operations.uncreate E i) (Rnotation.create E p o z u m)). Lemma underlying_create: Ul create = E. Proof. ir. transitivity (Ul (Rnotation.create E p o z u m)). uf Ul. uf create. drwe. tv. mw. Qed. Lemma neg_create_when: forall a, inc a E -> neg create a = o a. Proof. ir. transitivity (neg (Rnotation.create E p o z u m) a). uf create; uf neg; uf Ul. drwe. tv. mw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. transitivity (dplus (Rnotation.create E p o z u m) a b). uf create; uf dplus; uf Ul. drwe. tv. mw. Qed. Lemma zero_create: zero create = z. Proof. ir. transitivity (zero (Rnotation.create E p o z u m)). uf zero. uf create. drwe. tv. mw. Qed. Lemma mult_create_when: forall a b, inc a E -> inc b E -> dmult create a b = (m a b). Proof. ir. transitivity (dmult (Rnotation.create E p o z u m) a b). uf create; uf dmult; uf Ul. drwe. tv. mw. Qed. Lemma one_create: one create = u. Proof. ir. transitivity (one (Rnotation.create E p o z u m)). uf one. uf create. drwe. tv. mw. Qed. Lemma inv_create_when: forall a, inc a E -> inv create a = i a. Proof. ir. pose (underlying_create). ufi create e. uf inv; uf create. rw e. drwe. app Operations.unary_recovers. Qed. Definition struct_property:= (Operations.is_law1I i E) & (Rnotation.struct_property E p o z u m). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rw underlying_create. rw zero_create. destruct H. destruct H0. ee. destruct H2. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. destruct H as [_ [_ [_ H]]]. destruct H as [_ [_ H]]. red in H. red. split. red. intros. rww plus_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_plus. Qed. Lemma is_bin_mult_create : struct_property -> Operations.is_law2 (dmult create) E. Proof. ir. destruct H as [_ [_ [H _]]]. red in H. red. split. red. intros. rww mult_create_when. app H. pose (H1:=underlying_create). app is_bin_domain_mult. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) E. Proof. intros. destruct H as [_ [_ [_ H]]]. destruct H as [_ [H _]]. red in H. red. split. red. intros. rww neg_create_when. app H. pose (H1:=underlying_create). app is_un_domain_neg. Qed. Lemma is_un_inv_create : struct_property -> Operations.is_law1 (inv create) E. Proof. intros. destruct H. red in H. red. split. red. intros. rww inv_create_when. app H. pose (H1:=underlying_create). app is_un_domain_inv. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_plus_create H0). destruct i0. am. am. app plus_create_when. Qed. Lemma mult_create : Operations.is_law2E m E -> struct_property -> dmult create = m. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_mult_create H0). destruct i0. am. am. app mult_create_when. Qed. Lemma neg_create : Operations.is_law1E o E -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_neg_create H0). destruct i0. am. am. intros. app neg_create_when. Qed. Lemma inv_create : Operations.is_law1E i E -> struct_property -> inv create = i. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_inv_create H0). destruct i0. am. am. intros. app inv_create_when. Qed. End Fconstruction. Hint Rewrite underlying_create neg_create plus_create zero_create: mw. Hint Rewrite one_create neg_create_when plus_create_when: mw. Hint Rewrite mult_create mult_create_when: mw. Hint Rewrite inv_create inv_create_when: mw. Lemma create_properties: forall (x:Set) (p:EEE)(o: EE)(z:Set)(u:Set) (m:EEE)(i:EE), Operations.is_law1E i x -> Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> struct_property x p o z u m i -> ((dplus (create x p o z u m i) = p) & (dmult (create x p o z u m i) = m) & (neg (create x p o z u m i) = o) & (inv (create x p o z u m i) = i)). Proof. ir. ee;mw. Qed. Definition like (a:Set):= a = create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a). Lemma create_like: forall a, like(create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a)). Proof. ir. uf like. set (x:=create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a)). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (one x = one a). uf x; mw. assert (inv x = inv a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_inv. app is_un_domain_inv. sy; am. ir. rwi H H2. mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H3. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. symmetry; am. ir. rewrite H in H4,H5. mw. assert (dmult x = dmult a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_mult. app is_bin_domain_mult. symmetry; am. ir. rewrite H in H5,H6. mw. rw H; rw H0; rw H1; rw H2; rw H3; rw H4; rw H5. tv. Qed. Lemma like_create: forall x p o z u m i, Operations.is_law1E i x -> Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> struct_property x p o z u m i -> like (create x p o z u m i). Proof. ir. pose (create_properties H H0 H1 H2 H3). ee. red. rw H4; rw H5; rw H6; rw H7. mw. Qed. End Fnotation. Export Fnotation. Module LMnotation. Section Construction. Variables (E:Set)(A:Set)(p:EEE)(o:EE)(z:Set)(m:EEE). Definition create := denote Laux_not A (denote Laction_not (Operations.actcreate (Ul A) E m) (Gnotation.create E p o z)). Lemma underlying_create: Ul create = E. Proof. ir. transitivity (Ul (Gnotation.create E p o z)). uf Ul; uf create. drwe. tv. mw. Qed. Lemma zero_create: zero create = z. Proof. ir. transitivity (zero (Gnotation.create E p o z)). uf zero; uf create. drw. mw. Qed. Lemma neg_create_when: forall a, inc a E -> neg create a = o a. Proof. ir. transitivity (neg (Gnotation.create E p o z) a). uf create; uf neg; uf Ul. drwe. tv. mw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. transitivity (dplus (Gnotation.create E p o z) a b). uf create; uf dplus; uf Ul. drwe. tv. mw. Qed. Lemma auxiliary_create: lauxiliary create = A. Proof. ir. uf lauxiliary. uf create. drw. Qed. Lemma lmult_create_when: forall a b, inc a (Ul A) -> inc b E -> lmult create a b = (m a b). Proof. ir. uf lmult. rw underlying_create. rw auxiliary_create. uf create. drw. app Operations.action_recovers. Qed. Definition struct_property:= (inc z E) & (Operations.is_law1I o E) & (Operations.is_law2I p E) & (Operations.is_lawaI m (Ul A) E). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rw zero_create. rw underlying_create. destruct H. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. red in H. ee. red. split. red. intros. rww plus_create_when. app H1. pose (underlying_create). app is_bin_domain_plus. Qed. Lemma is_act_mult_create : struct_property -> Operations.is_lawa (lmult create) (Ul A) E. Proof. ir. red in H. ee. red. split. red. intros. rww lmult_create_when. app H2. pose (underlying_create). app is_act_domain_lmult. app auxiliary_create. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) E. Proof. ir. red in H. ee. red. split. red. intros. rww neg_create_when. app H0. pose (underlying_create). app is_un_domain_neg. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_plus_create H0). destruct i. am. am. app plus_create_when. Qed. Lemma lmult_create : Operations.is_lawaE m (Ul A) E -> struct_property -> lmult create = m. Proof. ir. apply Operations.action_extensionality with (Ul A) E. pose (is_act_mult_create H0). destruct i. am. am. app lmult_create_when. Qed. Lemma neg_create: Operations.is_law1E o E -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_neg_create H0). destruct i. am. am. intros. app neg_create_when. Qed. End Construction. Hint Rewrite underlying_create auxiliary_create neg_create plus_create zero_create: mw. Hint Rewrite neg_create_when plus_create_when: mw. Hint Rewrite lmult_create lmult_create_when: mw. Lemma create_properties: forall (x:Set) (y:Set)(p:EEE)(o: EE)(z:Set)(m:EEE), Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> struct_property x y p o z m -> ((dplus (create x y p o z m) = p) & (lmult (create x y p o z m) = m) & (neg (create x y p o z m) = o)). Proof. ir. ee; mw. Qed. Definition like (a:Set):= a = create (Ul a) (lauxiliary a) (dplus a) (neg a) (zero a) (lmult a). Lemma create_like: forall a, like(create (Ul a) (lauxiliary a) (dplus a) (neg a) (zero a) (lmult a)). Proof. ir. uf like. set (x:= create (Ul a) (lauxiliary a) (dplus a) (neg a) (zero a) (lmult a)). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H1. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. symmetry; am. ir. rewrite H in H2,H3. mw. assert (lauxiliary x = lauxiliary a). uf x; mw. assert (lmult x = lmult a). unfold x. set (y:= lauxiliary x). apply Operations.action_extensionality with (Ul y) (Ul x). rw H. app is_act_domain_lmult. app is_act_domain_lmult. sy; am. wrr H3. ir. rewrite H in H5. unfold y in H4. rewrite H3 in H4. mw. rw H; rw H0; rw H1; rw H2; rw H3; rw H4. tv. Qed. Lemma like_create: forall x y p o z m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> struct_property x y p o z m -> like (create x y p o z m). Proof. ir. pose (create_properties H H0 H1 H2). ee. red. rw H3; rw H4; rw H5. mw. Qed. End LMnotation. Export LMnotation. Module RMnotation. Section Construction. Variables (E:Set)(A:Set)(p:EEE)(o:EE)(z:Set)(m:EEE). Definition create := denote Raux_not A (denote Raction_not (Operations.actcreate (Ul A) E m) (Gnotation.create E p o z)). Lemma underlying_create: Ul create = E. Proof. ir. transitivity (Ul (Gnotation.create E p o z)). uf Ul; uf create. drwe. tv. mw. Qed. Lemma zero_create: zero create = z. Proof. ir. transitivity (zero (Gnotation.create E p o z)). uf zero; uf create. drw. mw. Qed. Lemma neg_create_when: forall a, inc a E -> neg create a = o a. Proof. ir. transitivity (neg (Gnotation.create E p o z) a). uf create; uf neg; uf Ul. drwe. tv. mw. Qed. Lemma plus_create_when: forall a b, inc a E -> inc b E -> dplus create a b = (p a b). Proof. ir. transitivity (dplus (Gnotation.create E p o z) a b). uf create; uf dplus; uf Ul. drwe. tv. mw. Qed. Lemma auxiliary_create: rauxiliary create = A. Proof. ir. uf rauxiliary. uf create. drw. Qed. Lemma rmult_create_when: forall a b, inc a (Ul A) -> inc b E -> rmult create a b = (m a b). Proof. ir. uf rmult. rw underlying_create. rw auxiliary_create. uf create. drw. app Operations.action_recovers. Qed. Definition struct_property:= (inc z E) & (Operations.is_law1I o E) & (Operations.is_law2I p E) & (Operations.is_lawaI m (Ul A) E). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rw zero_create. rw underlying_create. destruct H. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) E. Proof. ir. red in H. ee. red. split. red. intros. rww plus_create_when. app H1. pose (underlying_create). app is_bin_domain_plus. Qed. Lemma is_act_mult_create : struct_property -> Operations.is_lawa (rmult create) (Ul A) E. Proof. ir. red in H. ee. red. split. red. intros. rww rmult_create_when. app H2. pose (underlying_create). app is_act_domain_rmult. app auxiliary_create. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) E. Proof. ir. red in H. ee. red. split. red. intros. rww neg_create_when. app H0. pose (underlying_create). app is_un_domain_neg. Qed. Lemma plus_create : Operations.is_law2E p E -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with E. pose (is_bin_plus_create H0). destruct i. am. am. app plus_create_when. Qed. Lemma rmult_create : Operations.is_lawaE m (Ul A) E -> struct_property -> rmult create = m. Proof. ir. apply Operations.action_extensionality with (Ul A) E. pose (is_act_mult_create H0). destruct i. am. am. app rmult_create_when. Qed. Lemma neg_create: Operations.is_law1E o E -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with E. pose (is_un_neg_create H0). destruct i. am. am. intros. app neg_create_when. Qed. End Construction. Hint Rewrite underlying_create auxiliary_create neg_create plus_create zero_create: mw. Hint Rewrite neg_create_when plus_create_when: mw. Hint Rewrite rmult_create rmult_create_when: mw. Lemma create_properties: forall (x:Set) (y:Set)(p:EEE)(o: EE)(z:Set)(m:EEE), Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> struct_property x y p o z m -> ((dplus (create x y p o z m) = p) & (rmult (create x y p o z m) = m) & (neg (create x y p o z m) = o)). Proof. ir. ee; mw. Qed. Definition like (a:Set):= a = create (Ul a) (rauxiliary a) (dplus a) (neg a) (zero a) (rmult a). Lemma create_like: forall a, like(create (Ul a) (rauxiliary a) (dplus a) (neg a) (zero a) (rmult a)). Proof. ir. uf like. set (x:= create (Ul a) (rauxiliary a) (dplus a) (neg a) (zero a) (rmult a)). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H1. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. symmetry; am. ir. rewrite H in H2,H3. mw. assert (rauxiliary x = rauxiliary a). uf x; mw. assert (rmult x = rmult a). unfold x. set (y:= rauxiliary x). apply Operations.action_extensionality with (Ul y) (Ul x). rw H. app is_act_domain_rmult. app is_act_domain_rmult. sy; am. wrr H3. ir. rewrite H in H5. unfold y in H4. rewrite H3 in H4. mw. rw H; rw H0; rw H1; rw H2; rw H3; rw H4. tv. Qed. Lemma like_create: forall x y p o z m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> struct_property x y p o z m -> like (create x y p o z m). Proof. ir. pose (create_properties H H0 H1 H2). ee. red. rw H3; rw H4; rw H5. mw. Qed. End RMnotation. Export RMnotation. Module LRMnotation. Section Construction. Variables (x:Set)(yl yr:Set)(p:EEE)(o:EE)(z:Set)(ml mr:EEE). Definition create := denote Laux_not yl (denote Raux_not yr (denote Laction_not (Operations.actcreate (Ul yl) x ml) (denote Raction_not (Operations.actcreate (Ul yr) x mr) (Gnotation.create x p o z)))). Lemma lauxiliary_create: lauxiliary create = yl. Proof. ir. uf lauxiliary. uf create. drw. Qed. Lemma rauxiliary_create: rauxiliary create = yr. Proof. ir. uf rauxiliary. uf create. drw. Qed. Lemma underlying_create: Ul create = x. Proof. ir. transitivity (Ul (Gnotation.create x p o z)). uf Ul; uf create. drwe. tv. mw. Qed. Lemma zero_create: zero create = z. Proof. ir. transitivity (zero (Gnotation.create x p o z)). uf zero; uf create. drw. mw. Qed. Lemma neg_create_when: forall a, inc a x -> neg create a = o a. Proof. ir. transitivity (neg (Gnotation.create x p o z) a). uf create; uf neg; uf Ul. drwe. tv. mw. Qed. Lemma plus_create_when: forall a b, inc a x -> inc b x -> dplus create a b = (p a b). Proof. ir. transitivity (dplus (Gnotation.create x p o z) a b). uf create; uf dplus; uf Ul. drwe. tv. mw. Qed. Lemma lmult_create_when: forall a b, inc a (Ul yl) -> inc b x -> lmult create a b = (ml a b). Proof. ir. uf lmult. rw underlying_create. rw lauxiliary_create. uf create. drw. app Operations.action_recovers. Qed. Lemma rmult_create_when: forall a b, inc a (Ul yr) -> inc b x -> rmult create a b = (mr a b). Proof. ir. uf rmult. rw underlying_create. rw rauxiliary_create. uf create. drw. app Operations.action_recovers. Qed. Definition struct_property:= (inc z x) & (Operations.is_law1I o x) & (Operations.is_law2I p x) & (Operations.is_lawaI ml (Ul yl) x) & (Operations.is_lawaI mr (Ul yr) x). Lemma inc_create_zero_U: struct_property -> inc (zero create) (Ul create). Proof. ir. rewrite zero_create. rewrite underlying_create. destruct H. am. Qed. Lemma is_bin_plus_create : struct_property -> Operations.is_law2 (dplus create) x. Proof. ir. red in H. ee. red. split. red. intros. rww plus_create_when. app H1. pose (underlying_create). app is_bin_domain_plus. Qed. Lemma is_act_lmult_create : struct_property -> Operations.is_lawa (lmult create) (Ul yl) x. Proof. ir. red in H. ee. red. split. red. intros. rww lmult_create_when. app H2. pose (underlying_create). app is_act_domain_lmult. app lauxiliary_create. Qed. Lemma is_act_rmult_create : struct_property -> Operations.is_lawa (rmult create) (Ul yr) x. Proof. ir. red in H. ee. red. split. red. intros. rww rmult_create_when. app H3. pose (underlying_create). app is_act_domain_rmult. app rauxiliary_create. Qed. Lemma is_un_neg_create : struct_property -> Operations.is_law1 (neg create) x. Proof. ir. red in H. ee. red. split. red. intros. rww neg_create_when. app H0. pose (underlying_create). app is_un_domain_neg. Qed. Lemma plus_create : Operations.is_law2E p x -> struct_property -> dplus create = p. Proof. ir. apply Operations.binary_extensionality with x. pose (is_bin_plus_create H0). destruct i. am. am. app plus_create_when. Qed. Lemma lmult_create : Operations.is_lawaE ml (Ul yl) x -> struct_property -> lmult create = ml. Proof. ir. apply Operations.action_extensionality with (Ul yl) x. pose (is_act_lmult_create H0). destruct i. am. am. app lmult_create_when. Qed. Lemma rmult_create : Operations.is_lawaE mr (Ul yr) x -> struct_property -> rmult create = mr. Proof. ir. apply Operations.action_extensionality with (Ul yr) x. pose (is_act_rmult_create H0). destruct i. am. am. app rmult_create_when. Qed. Lemma neg_create: Operations.is_law1E o x -> struct_property -> neg create = o. Proof. intros. apply Operations.unary_extensionality with x. pose (is_un_neg_create H0). destruct i. am. am. intros. app neg_create_when. Qed. End Construction. Hint Rewrite underlying_create lauxiliary_create rauxiliary_create neg_create plus_create zero_create: mw. Hint Rewrite one_create neg_create_when plus_create_when: mw. Hint Rewrite lmult_create lmult_create_when: mw. Hint Rewrite rmult_create rmult_create_when: mw. Lemma create_properties: forall (x:Set) (yl yr:Set)(p:EEE)(o: EE)(z:Set)(ml mr:EEE), Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE ml (Ul yl) x -> Operations.is_lawaE mr (Ul yr) x -> struct_property x yl yr p o z ml mr -> ((dplus (create x yl yr p o z ml mr) = p) & (lmult (create x yl yr p o z ml mr) = ml) & (rmult (create x yl yr p o z ml mr) = mr) & (neg (create x yl yr p o z ml mr) = o)). Proof. ir. ee; mw. Qed. Definition like (a:Set):= a = create (Ul a) (lauxiliary a) (rauxiliary a) (dplus a) (neg a) (zero a) (lmult a) (rmult a). Lemma create_like: forall a, like(create (Ul a) (lauxiliary a) (rauxiliary a) (dplus a) (neg a) (zero a) (lmult a) (rmult a)). Proof. ir. uf like. set (x:= create (Ul a) (lauxiliary a) (rauxiliary a) (dplus a) (neg a) (zero a) (lmult a) (rmult a)). assert (Ul x = Ul a). uf x; mw. assert (zero x = zero a). uf x; mw. assert (neg x = neg a). uf x. apply Operations.unary_extensionality with (Ul x). rw H. app is_un_domain_neg. app is_un_domain_neg. sy; am. ir. rwi H H1. mw. assert (dplus x = dplus a). unfold x. apply Operations.binary_extensionality with (Ul x). rw H. app is_bin_domain_plus. app is_bin_domain_plus. symmetry; am. ir. rewrite H in H2,H3. mw. assert (lauxiliary x = lauxiliary a). uf x; mw. assert (rauxiliary x = rauxiliary a). uf x; mw. assert (lmult x = lmult a). unfold x. set (y:= lauxiliary x). apply Operations.action_extensionality with (Ul y) (Ul x). rw H. app is_act_domain_lmult. app is_act_domain_lmult. sy; am. wrr H3. ir. rewrite H in H6. unfold y in H5. rewrite H3 in H5. mw. assert (rmult x = rmult a). unfold x. set (y:= rauxiliary x). apply Operations.action_extensionality with (Ul y) (Ul x). rw H. app is_act_domain_rmult. app is_act_domain_rmult. sy; am. wrr H4. ir. rewrite H in H7. unfold y in H6. rewrite H4 in H6. mw. rw H; rw H0; rw H1; rw H2; rw H3; rw H4; rw H5; rw H6. tv. Qed. Lemma like_create: forall x yl yr p o z ml mr, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE ml (Ul yl) x -> Operations.is_lawaE mr (Ul yr) x -> struct_property x yl yr p o z ml mr -> like (create x yl yr p o z ml mr). Proof. ir. pose (create_properties H H0 H1 H2 H3). ee. red. rw H4; rw H5; rw H6; rw H7. mw. Qed. End LRMnotation. Export LRMnotation. (* ******************************************************************* *) Module Adefinitions. Section Construction. Variables (x:Set) (p: EEE)(o: EE)(z:Set)(u:Set)(m:EEE)(i:EE). Definition plus_commutativity := forall (a b:Set), inc a x -> inc b x -> p a b = p b a. Definition plus_associativity := forall (a b c:Set), inc a x -> inc b x -> inc c x-> p (p a b) c = p a (p b c). Definition mult_commutativity := forall (a b:Set), inc a x -> inc b x -> m a b = m b a. Definition mult_associativity := forall (a b c:Set), inc a x -> inc b x -> inc c x-> m (m a b) c = m a (m b c). Definition plus_unit_left := forall (a:Set), inc a x -> p z a =a. Definition plus_unit_right := forall (a:Set), inc a x -> p a z =a. Definition mult_unit_left := forall (a:Set), inc a x -> m u a =a. Definition mult_unit_right := forall (a:Set), inc a x -> m a u =a. Definition plus_inverse_left := forall (a:Set), inc a x -> p (o a) a= z. Definition plus_inverse_right := forall (a:Set), inc a x -> p a (o a) = z. Definition mult_inverse_left := forall (a:Set), inc a x -> a <> z -> m (i a) a= u. Definition mult_inverse_right := forall (a:Set), inc a x -> a <> z -> m a (i a) = u. Definition left_distributive := forall(a b c:Set), inc a x -> inc b x -> inc c x -> m a (p b c) = p (m a b) (m a c). Definition right_distributive := forall(a b c:Set), inc a x -> inc b x -> inc c x -> m (p b c) a = p (m b a) (m c a). Definition plus_internal:= Operations.is_law2I p x. Definition neg_internal:= Operations.is_law1I o x. Definition mult_internal:= Operations.is_law2I m x. Definition inv_internal:= Operations.is_law1I i x. Definition mproperty := (inc z x) & plus_internal & plus_associativity & plus_unit_right & plus_unit_left. Definition gproperty := mproperty & neg_internal & plus_inverse_right & plus_inverse_left. Definition cgproperty := gproperty & plus_commutativity. Definition rproperty := cgproperty & mult_internal & (inc u x) & mult_associativity & mult_unit_right & mult_unit_left & left_distributive & right_distributive. Definition fproperty := rproperty & mult_inverse_left & mult_inverse_right & inv_internal &(exists a, inc a x & a <> z). Definition crproperty := rproperty & mult_commutativity. Definition cfproperty := fproperty & mult_commutativity. End Construction. Section Mconstruction. Variables (x:Set) (y:Set) (p: EEE)(o: EE)(z:Set)(m:EEE). Definition action_left_distributive := forall(a b c:Set), inc a (Ul y) -> inc b x -> inc c x -> m a (p b c) = p (m a b) (m a c). Definition action_right_distributive := forall(a b c:Set), inc a x -> inc b (Ul y) -> inc c (Ul y) -> m (dplus y b c) a = p (m b a) (m c a). Definition laction_associative := forall(a b c:Set), inc a (Ul y) -> inc b (Ul y) -> inc c x -> m a (m b c) = m (dmult y a b) c. Definition raction_associative := forall(a b c:Set), inc a (Ul y) -> inc b (Ul y) -> inc c x -> m a (m b c) = m (dmult y b a) c. Definition action_unary:= forall a:Set, inc a x -> m (one y) a = a. Definition action_internal:= Operations.is_lawaI m (Ul y) x. End Mconstruction. Definition lmproperty (x:Set) (y:Set) (p: EEE)(o: EE)(z:Set)(m:EEE):= cgproperty x p o z & action_left_distributive x y p m & action_right_distributive x y p m& laction_associative x y m & action_internal x y m & action_unary x y m. Definition rmproperty (x:Set) (y:Set) (p: EEE)(o: EE)(z:Set)(m:EEE):= cgproperty x p o z & action_left_distributive x y p m & action_right_distributive x y p m& raction_associative x y m & action_internal x y m & action_unary x y m. Definition lrmproperty (x:Set) (yl yr:Set) (p: EEE)(o: EE)(z:Set)(ml mr:EEE):= cgproperty x p o z & action_left_distributive x yl p ml & action_right_distributive x yl p ml & action_left_distributive x yr p mr & action_right_distributive x yr p mr& laction_associative x yl ml & raction_associative x yr mr & action_internal x yl ml & action_unary x yl ml & action_internal x yr mr & action_unary x yr mr. Definition monoid_axioms a := mproperty (Ul a) (dplus a) (zero a). Definition strong_monoid_axioms a := (Mn_notation.like a) & (monoid_axioms a). Definition group_axioms a := gproperty (Ul a) (dplus a) (neg a) (zero a). Definition strong_group_axioms a := (Gnotation.like a) & (group_axioms a). Definition cgroup_axioms a := cgproperty (Ul a) (dplus a) (neg a) (zero a). Definition strong_cgroup_axioms a := (Gnotation.like a) &(cgroup_axioms a). Definition ring_axioms a := rproperty (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a). Definition strong_ring_axioms a := (Rnotation.like a) & (ring_axioms a). Definition cring_axioms a := crproperty (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a). Definition strong_cring_axioms a := (Rnotation.like a) &(cring_axioms a). Definition sfield_axioms a := fproperty (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a). Definition strong_sfield_axioms a := (Fnotation.like a) & (sfield_axioms a). Definition field_axioms a := cfproperty (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a). Definition strong_field_axioms a := (Fnotation.like a) & (field_axioms a). Definition lmodule_axioms a := (ring_axioms (lauxiliary a)) & (lmproperty (Ul a) (lauxiliary a) (dplus a) (neg a) (zero a) (lmult a)). Definition strong_lmodule_axioms a := (LMnotation.like a) & (Rnotation.like (lauxiliary a)) & (lmodule_axioms a). Definition rmodule_axioms a := (ring_axioms (rauxiliary a)) & (rmproperty (Ul a) (rauxiliary a) (dplus a) (neg a) (zero a) (rmult a)). Definition strong_rmodule_axioms a := (RMnotation.like a) & (Rnotation.like (rauxiliary a)) & (rmodule_axioms a). Definition lrmodule_axioms a := (ring_axioms (lauxiliary a)) & (ring_axioms (rauxiliary a)) & (lrmproperty (Ul a) (lauxiliary a) (rauxiliary a) (dplus a) (neg a) (zero a) (lmult a) (rmult a)). Definition strong_lrmodule_axioms a := (LRMnotation.like a) & (Rnotation.like (lauxiliary a)) & (Rnotation.like (rauxiliary a)) & (lrmodule_axioms a). Lemma monoid_implies_mstruct:forall x p z, mproperty x p z -> (Mn_notation.struct_property x p z). Proof. ir. red in H. ee. red. split; am. Qed. Lemma group_implies_gstruct:forall x p o z, gproperty x p o z -> (Gnotation.struct_property x p o z). Proof. ir. red in H. ee. cp (monoid_implies_mstruct H). red in H3; ee. red. intuition. Qed. Lemma ring_implies_gstruct:forall x p o z u m, rproperty x p o z u m-> (Gnotation.struct_property x p o z). Proof. ir. destruct H. destruct H. app group_implies_gstruct. Qed. Lemma ring_implies_rstruct: forall x p o z u m, rproperty x p o z u m -> Rnotation.struct_property x p o z u m. Proof. ir. red. split. red in H. ee; am. split. red in H. ee. am. app (ring_implies_gstruct H). Qed. Lemma sfield_implies_rstruct: forall x p o z u m i, fproperty x p o z u m i-> Rnotation.struct_property x p o z u m. Proof. ir. destruct H. app ring_implies_rstruct. Qed. Lemma sfield_implies_fstruct: forall x p o z u m i, fproperty x p o z u m i-> Fnotation.struct_property x p o z u m i. Proof. ir. destruct H. split. destruct H0 as [_ [_ [H0 _]]]. am. app ring_implies_rstruct. Qed. Lemma lmodule_implies_mstruct: forall x y p o z m, lmproperty x y p o z m -> LMnotation.struct_property x y p o z m. Proof. ir. assert (Gnotation.struct_property x p o z). destruct H. destruct H. app group_implies_gstruct. red in H0. ee. red in H. ee. red. intuition. Qed. Lemma rmodule_implies_mstruct: forall x y p o z m, rmproperty x y p o z m -> RMnotation.struct_property x y p o z m. Proof. ir. assert (Gnotation.struct_property x p o z). destruct H. destruct H. app group_implies_gstruct. red in H0. ee. red in H. ee. red. intuition. Qed. Lemma lrmodule_implies_mstruct: forall x yl yr p o z ml mr, lrmproperty x yl yr p o z ml mr -> LRMnotation.struct_property x yl yr p o z ml mr. Proof. ir. assert (Gnotation.struct_property x p o z). destruct H. destruct H. app group_implies_gstruct. red in H0. ee. red in H. ee. red. intuition. Qed. Lemma lrmodule_implies_lmstruct: forall x yl yr p o z ml mr, lrmproperty x yl yr p o z ml mr -> LMnotation.struct_property x yl p o z ml. Proof. ir. cp (lrmodule_implies_mstruct H). red in H0. ee. red. intuition. Qed. Lemma lrmodule_implies_rmstruct: forall x yl yr p o z ml mr, lrmproperty x yl yr p o z ml mr -> RMnotation.struct_property x yr p o z mr. Proof. ir. cp (lrmodule_implies_mstruct H). red in H0. ee. red. intuition. Qed. Lemma mcreate_axioms: forall x p z, Operations.is_law2E p x -> mproperty x p z -> strong_monoid_axioms (Mn_notation.create x p z). Proof. ir. assert (Mn_notation.struct_property x p z). app monoid_implies_mstruct. split. app Mn_notation.like_create. red. mw. Qed. Lemma monoid_is_monoid: forall a, monoid_axioms a -> strong_monoid_axioms (Mn_notation.create (Ul a) (dplus a) (zero a)). Proof. intros. apply mcreate_axioms. app is_bin_domain_plus. am. Qed. Lemma gcreate_axioms: forall x p o z, Operations.is_law2E p x -> Operations.is_law1E o x -> gproperty x p o z -> strong_group_axioms (Gnotation.create x p o z). Proof. ir. cp (group_implies_gstruct H1). split. app Gnotation.like_create. red. mw. Qed. Lemma group_is_group: forall a, group_axioms a -> strong_group_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. intros. apply gcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. am. Qed. Lemma group_is_monoid: forall a, group_axioms a -> monoid_axioms a. Proof. ir. red in H. red in H. destruct H. am. Qed. Lemma strong_group_is_monoid: forall a, group_axioms a -> strong_monoid_axioms (Mn_notation.create (Ul a) (dplus a) (zero a)). Proof. ir. destruct H. pose (b:=Mn_notation.create (Ul a) (dplus a) (zero a)). app mcreate_axioms. app is_bin_domain_plus. Qed. Lemma cgcreate_axioms: forall x p o z, Operations.is_law2E p x -> Operations.is_law1E o x -> gproperty x p o z -> plus_commutativity x p -> strong_cgroup_axioms (Gnotation.create x p o z). Proof. ir. pose (a:=Gnotation.create x p o z). assert (strong_group_axioms a). uf a. app gcreate_axioms. red in H3. ee. fold a. split. am. split. mw. assert (Gnotation.struct_property x p o z). app group_implies_gstruct. unfold a. mw. Qed. Lemma plus_gcreate : forall a, group_axioms a-> dplus (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)) = dplus a. Proof. ir. red in H. ee. mw. app is_bin_domain_plus. app group_implies_gstruct. Qed. Lemma neg_gcreate : forall a, group_axioms a-> neg (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)) = neg a. Proof. ir. red in H. ee. mw. app is_un_domain_neg. app group_implies_gstruct. Qed. Lemma cgroup_is_group: forall a, cgroup_axioms a -> group_axioms a. Proof. intros. destruct H. red. am. Qed. Lemma strong_cgroup_is_group: forall a, strong_cgroup_axioms a -> strong_group_axioms a. Proof. intros. destruct H. pose (cgroup_is_group H0). split; am. Qed. Lemma cgroup_is_cgroup: forall a, cgroup_axioms a -> strong_cgroup_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. intros. destruct H. app cgcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. Qed. Lemma rcreate_axioms: forall x p o z u m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> rproperty x p o z u m-> strong_ring_axioms (Rnotation.create x p o z u m). Proof. ir. cp(ring_implies_rstruct H2). red. split. app Rnotation.like_create. red. mw. Qed. Lemma ring_is_ring: forall a, ring_axioms a -> strong_ring_axioms (Rnotation.create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a)). Proof. ir. ap rcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_bin_domain_mult. am. Qed. Lemma ring_is_cgroup: forall a, ring_axioms a -> cgroup_axioms a. Proof. ir. red in H. red in H. destruct H. am. Qed. Lemma strong_ring_is_cgroup: forall a, ring_axioms a -> strong_cgroup_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. ir. destruct H. destruct H. pose (b:=Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). app cgcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. Qed. Lemma plus_rcreate : forall a, ring_axioms a-> dplus (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)) = dplus a. Proof. ir. mw. app is_bin_domain_plus. red in H. app ring_implies_rstruct. Qed. Lemma neg_rcreate : forall a, ring_axioms a-> neg (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)) = neg a. Proof. ir. mw. app is_un_domain_neg. red in H. app ring_implies_rstruct. Qed. Lemma mult_rcreate : forall a, ring_axioms a-> dmult (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)) = dmult a. Proof. ir. mw. app is_bin_domain_mult. red in H. app ring_implies_rstruct. Qed. Lemma cring_is_ring: forall a, cring_axioms a -> ring_axioms a. Proof. intros. destruct H. am. Qed. Lemma strong_cring_is_ring: forall a, strong_cring_axioms a -> strong_ring_axioms a. Proof. intros. destruct H. pose (cring_is_ring H0). split;am. Qed. Lemma cring_is_cring: forall a, cring_axioms a -> strong_cring_axioms (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). Proof. intros. destruct H. set (b:=Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). assert (strong_ring_axioms b). unfold b. app ring_is_ring. red. destruct H1. split. am. split. am. assert (Ul b = Ul a). unfold b. mw. assert (dmult b = dmult a). unfold b. app mult_rcreate. rw H3; rww H4. Qed. Lemma fcreate_axioms: forall x p o z u m i, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_law2E m x -> Operations.is_law1E i x -> fproperty x p o z u m i-> strong_sfield_axioms (Fnotation.create x p o z u m i). Proof. ir. cp (sfield_implies_fstruct H3). red. split. app Fnotation.like_create. red. mw. Qed. Lemma sfield_is_sfield: forall a, sfield_axioms a -> strong_sfield_axioms (Fnotation.create (Ul a) (dplus a) (neg a) (zero a) (one a) (dmult a) (inv a)). Proof. ir. ap fcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_bin_domain_mult. app is_un_domain_inv. am. Qed. Lemma field_is_sfield: forall a, field_axioms a -> sfield_axioms a. Proof. intros. destruct H. am. Qed. Lemma mult_fcreate : forall a, sfield_axioms a-> dmult (Fnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a) (dmult a)(inv a)) = dmult a. Proof. ir. mw. app is_bin_domain_mult. red in H. app sfield_implies_fstruct. Qed. Lemma field_is_field: forall a, field_axioms a -> strong_field_axioms (Fnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a) (dmult a)(inv a)). Proof. intros. destruct H. set (b:=Fnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a) (dmult a)(inv a)). assert (strong_sfield_axioms b). unfold b. app sfield_is_sfield. red. destruct H1. split. am. split. am. assert (Ul b = Ul a). unfold b. mw. assert (dmult b = dmult a). unfold b. app mult_fcreate. rw H3; rww H4. Qed. Lemma sfield_is_ring: forall a, sfield_axioms a -> ring_axioms a. Proof. ir. red in H. red in H. destruct H. am. Qed. Lemma strong_sfield_is_ring: forall a, sfield_axioms a -> strong_ring_axioms (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). Proof. ir. destruct H. pose (b:=Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). app rcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_bin_domain_mult. Qed. Lemma field_is_cring: forall a, field_axioms a -> cring_axioms a. Proof. ir. red in H. red in H. destruct H. destruct H. split;am. Qed. Lemma strong_field_is_cring: forall a, field_axioms a -> strong_cring_axioms (Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). Proof. ir. cp (field_is_cring H). cp(cring_is_ring H0). destruct H. pose (b:=Rnotation.create (Ul a) (dplus a) (neg a) (zero a)(one a)(dmult a)). assert (strong_ring_axioms b). unfold b. app strong_sfield_is_ring. red in H3. ee. red in H4. ee. fold b. split. am. split. am. assert (Ul b = Ul a). unfold b. mw. assert (dmult b = dmult a). unfold b. app mult_rcreate. rw H5; rww H6. Qed. Lemma lmcreate_axioms: forall x y p o z m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> lmproperty x y p o z m -> strong_ring_axioms y -> strong_lmodule_axioms (LMnotation.create x y p o z m). Proof. ir. assert (ring_axioms y). red in H3; ee;am. cp (lmodule_implies_mstruct H2). red. split. mw. app LMnotation.like_create. split. mw. red in H3; ee; am. red. split. mw. mw. Qed. Lemma rmcreate_axioms: forall x y p o z m, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE m (Ul y) x -> rmproperty x y p o z m -> strong_ring_axioms y -> strong_rmodule_axioms (RMnotation.create x y p o z m). Proof. ir. assert (ring_axioms y). red in H3; ee;am. cp (rmodule_implies_mstruct H2). red. split. app RMnotation.like_create. split. mw. red in H3;ee;am. red. split. mw. mw. Qed. Lemma lrmcreate_axioms: forall x yr yl p o z ml mr, Operations.is_law2E p x -> Operations.is_law1E o x -> Operations.is_lawaE ml (Ul yl) x -> Operations.is_lawaE mr (Ul yr) x -> lrmproperty x yl yr p o z ml mr -> strong_ring_axioms yl -> strong_ring_axioms yr -> strong_lrmodule_axioms (LRMnotation.create x yl yr p o z ml mr). Proof. ir. assert (ring_axioms yr). red in H5; ee;am. assert (ring_axioms yl). red in H4; ee;am. cp (lrmodule_implies_mstruct H3). red. split. app LRMnotation.like_create. split. mw. red in H4; ee;am. split. mw. red in H5; ee;am. red. split. mw. mw. split; am. Qed. Lemma lmodule_is_lmodule: forall a, lmodule_axioms a -> strong_ring_axioms (lauxiliary a) -> strong_lmodule_axioms (LMnotation.create (Ul a) (lauxiliary a) (dplus a) (neg a) (zero a) (lmult a)). Proof. ir. red in H. ee. ap lmcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_act_domain_lmult. am. am. Qed. Lemma rmodule_is_rmodule: forall a, rmodule_axioms a -> strong_ring_axioms (rauxiliary a) -> strong_rmodule_axioms (RMnotation.create (Ul a) (rauxiliary a) (dplus a) (neg a) (zero a) (rmult a)). Proof. ir. red in H. ee. ap rmcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_act_domain_rmult. am. am. Qed. Lemma lrmodule_is_lrmodule: forall a, lrmodule_axioms a -> strong_ring_axioms (lauxiliary a) -> strong_ring_axioms (rauxiliary a) -> strong_lrmodule_axioms (LRMnotation.create (Ul a) (lauxiliary a) (rauxiliary a) (dplus a) (neg a) (zero a) (lmult a) (rmult a)). Proof. ir. red in H. ee. ap lrmcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. app is_act_domain_lmult. app is_act_domain_rmult. am. am. am. Qed. Lemma lmodule_is_cgroup: forall a, lmodule_axioms a -> cgroup_axioms a. Proof. ir. destruct H as [_ [H _]]. am. Qed. Lemma rmodule_is_cgroup: forall a, rmodule_axioms a -> cgroup_axioms a. Proof. ir. destruct H as [_ [H _]]. am. Qed. Lemma lrmodule_is_cgroup: forall a, lrmodule_axioms a -> cgroup_axioms a. Proof. ir. destruct H as [_ [_ [H _]]]. am. Qed. Lemma strong_lmodule_is_cgroup: forall a, lmodule_axioms a -> strong_cgroup_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. ir. destruct H as [_ [H _]]. destruct H. pose (b:=Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). app cgcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. Qed. Lemma strong_rmodule_is_cgroup: forall a, rmodule_axioms a -> strong_cgroup_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. ir. destruct H as [_ [H _]]. destruct H. pose (b:=Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). app cgcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. Qed. Lemma strong_lrmodule_is_cgroup: forall a, lrmodule_axioms a -> strong_cgroup_axioms (Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). Proof. ir. destruct H as [_ [_ [H _]]]. destruct H. pose (b:=Gnotation.create (Ul a) (dplus a) (neg a) (zero a)). app cgcreate_axioms. app is_bin_domain_plus. app is_un_domain_neg. Qed. Lemma lmodule_aux_is_ring: forall a, lmodule_axioms a -> ring_axioms (lauxiliary a). Proof. ir. red in H; ee. am. Qed. Lemma rmodule_aux_is_ring: forall a, rmodule_axioms a -> ring_axioms (rauxiliary a). Proof. ir. red in H; ee. am. Qed. Lemma llrmodule_aux_is_ring: forall a, lrmodule_axioms a -> ring_axioms (lauxiliary a). Proof. ir. red in H; ee. am. Qed. Lemma rlrmodule_aux_is_ring: forall a, lrmodule_axioms a -> ring_axioms (rauxiliary a). Proof. ir. red in H; ee. am. Qed. Lemma lrmodule_is_lmodule: forall a, lrmodule_axioms a -> lmodule_axioms a. Proof. ir. red in H. ee. red; split. am. red in H1. ee. red. intuition. Qed. Lemma lrmodule_is_rmodule: forall a, lrmodule_axioms a -> rmodule_axioms a. Proof. ir. red in H. ee. red; split. am. red in H1. ee. red. intuition. Qed. End Adefinitions. Export Adefinitions. Module Transformation. Definition Taxioms (A B: Set) (f : EE) := forall x, inc x A -> inc (f x) B. Definition Tinjective A B f := (Taxioms A B f & forall x y , inc x A -> inc y A -> f x = f y -> x = y). Definition Tsurjective A B f := (Taxioms A B f & forall x, inc x B -> exists y, (inc y A) & (f y = x)). Definition Tbijective A B f := (Tinjective A B f & Tsurjective A B f). Lemma compose_Taxioms : forall A B C f g, Taxioms B C f -> Taxioms A B g -> Taxioms A C (fun x => f (g x)). Proof. uf Taxioms. ir. auto. Qed. Lemma identity_Taxioms : forall A, Taxioms A A (fun x : Set => x). Proof. uf Taxioms. tv. Qed. Definition Tinverse (A : Set) (f : EE) (y : Set) := choose (fun x => (inc x A & f x = y)). Lemma surjective_inverse_Taxioms : forall A B f, Tsurjective A B f -> Taxioms B A (Tinverse A f). Proof. uf Tsurjective. uf Taxioms. uf Tinverse. ir. set (q:= (choose (fun x0 : Set => inc x0 A & f x0 = x))). assert (inc q A & f q = x). uf q. app choose_pr. nin H. app H1. nin H1; am. Qed. Lemma Tsurjective_inverse_right : forall A B f y , Tsurjective A B f -> inc y B -> f (Tinverse A f y) = y. Proof. uf Tinverse. uf Tsurjective. ir. ee. set (q:= choose (fun x => inc x A & f x = y)). assert (inc q A & f q = y). uf q. app choose_pr. app H1. nin H2; am. Qed. Definition are_Tinverse (A B : Set) (f g : EE) := Taxioms A B f & Taxioms B A g & (forall x, inc x A -> g (f x) = x) & (forall y, inc y B -> f (g y) = y). Lemma Tbijective_inverse : forall A B f, Tbijective A B f -> are_Tinverse A B f (Tinverse A f). Proof. uf Tbijective; uf are_Tinverse. ir. nin H. nin H. cp (surjective_inverse_Taxioms H0). ee. am. am. ir. ir. cp (Tsurjective_inverse_right H0 (H _ H3)). app H1. app H2. app H. ir. app (Tsurjective_inverse_right H0 H3). Qed. Lemma Tinverse_bijective : forall A B f g, are_Tinverse A B f g -> Tbijective A B f. Proof. uf Tbijective. uf are_Tinverse. ir. ee. red. ee. am. ir. wrr H1. wr H5. sy; app H1. red. ee. am. ir. exists (g x). split. app H0. app H2. Qed. Lemma Tsub_bijective : forall A B f C, Tinjective A B f -> sub C A -> Tbijective C (fun_image C f) f. Proof. ir. assert (Taxioms C (fun_image C f) f). red. app inc_fun_image. red. ee. red. split. am. red in H; ee. ir. app H2. app H0. app H0. red. ee. am. ir. rwi fun_image_rw H2. am. Qed. Lemma Tidentity_bijective : forall A, Tbijective A A (fun y => y). Proof. ir. cp (identity_Taxioms (A:=A)). red. split; split; try am. auto. ir. exists x. auto. Qed. Lemma Tsubidentity_injective : forall A B, sub A B -> Tinjective A B (fun z => z). Proof. ir. split. red. ir. app H. tv. Qed. Lemma Tcompose_injective : forall A B C f g, Tinjective A B f -> Tinjective B C g -> Tinjective A C (fun y=> g (f y)). Proof. ir. nin H. nin H0. split. ap (compose_Taxioms H0 H). ir. app H1. app H2. app H. app H. Qed. Lemma Tcompose_surjective : forall A B C f g, Tsurjective A B f -> Tsurjective B C g -> Tsurjective A C (fun y=> g (f y)). Proof. ir. nin H; nin H0. split. ap (compose_Taxioms H0 H). ir. nin (H2 x). ee. nin (H1 x0); ee. exists x1; ee; try am. rww H7. am. am. Qed. Lemma Tcompose_bijective : forall A B C f g, Tbijective A B f -> Tbijective B C g -> Tbijective A C (fun y => g (f y)). Proof. uf Tbijective. ir. ee. apply Tcompose_injective with B; am. apply Tcompose_surjective with B; am. Qed. (* M stands for Map *) Definition Maxioms (a b f : Set) := fgraph f & domain f = a & sub (range f) b. Lemma function_Maxioms: forall f, is_function f -> Maxioms (source f) (target f) (graph f). Proof. ir. uf Maxioms. red in H. eee. Qed. Lemma function_Maxioms2: forall a b f, Maxioms a b f -> is_function (corresp a b f). Proof. ir. red in H. ee. app is_function_pr. sy; am. Qed. Lemma Mcompose_axioms : forall a b c f g, Maxioms b c f -> Maxioms a b g -> Maxioms a c (fcompose f g). Proof. uf Maxioms. ir. assert (fcomposable f g). unfold fcomposable. ee. am. am. rww H3. cp (fcompose_fgraph f g). ee. am. rww fcomposable_domain. red. ir. awi H7. nin H7. cp (pr2_V H2 H7). awi H8. cp (inc_pr1_domain H7). rwi fcomposable_domain H9. rwi pr1_pair H9. bwi H8. rw H8. app H6. app inc_V_range. rw H5. app H4. app inc_V_range. am. am. am. nin H2; am. Qed. Lemma identity_Maxioms : forall a, Maxioms a a (identity_g a). Proof. ir. unfold Maxioms. ee. ap identity_fgraph. rww identity_domain. uf identity_g. red. ir. rwi L_range_rw H. nin H. ee. wrr H0. Qed. Definition Msurjective A B f := Maxioms A B f & (forall x, inc x B -> exists y, (inc y A) & (V y f = x)). Definition Minjective A B f := Maxioms A B f & (forall x y , inc x A -> inc y A -> (V x f= V y f)-> x = y). Definition Mbijective (A B f : Set) := Minjective A B f & Msurjective A B f. Lemma trans_map_axioms : forall x y f, Taxioms x y f = Maxioms x y (L x f). Proof. ir. ap iff_eq; ir. red. ee. gprops. bw. rw L_range. red. ir. awi H0. nin H0. ee. wr H1. app H. red. ir. red in H; ee. app H2. rw L_range. aw. exists x0. ee. am. tv. Qed. Lemma trans_map_injective : forall x y f, Tinjective x y f = Minjective x y (L x f). Proof. ir. uf Minjective. uf Tinjective. rw trans_map_axioms. ap iff_eq; ir. ee. am. ir. bwi H3. app H0. am. am. ee. am. ir. app H0. bw. Qed. Lemma trans_map_surjective : forall x y f, Tsurjective x y f = Msurjective x y (L x f). Proof. uf Tsurjective; uf Msurjective. ir. rw trans_map_axioms. ap iff_eq; ir. ee. am. ir. nin (H0 _ H1). exists x1. nin H2. bw. intuition. ee. am. ir. nin (H0 _ H1). nin H2. bwi H3. exists x1. intuition. am. Qed. Lemma trans_map_bijective : forall x y f, Tbijective x y f = Mbijective x y (L x f). Proof. uf Tbijective. uf Mbijective. ir. rww trans_map_injective. rww trans_map_surjective. Qed. Lemma map_bijective1 : forall x y f, Mbijective x y f -> bijective (corresp x y f). Proof. ir. nin H. split. red. nin H. ir. split. app function_Maxioms2. uf W. aw. nin H0. app surjective_pr6. app function_Maxioms2. uf W. aw. Qed. Lemma map_bijective2 : forall f, bijective f -> Mbijective (source f) (target f) (graph f). Proof. ir. nin H. split. nin H. split. app function_Maxioms. app H1. red. split. nin H0. app function_Maxioms. ir. nin (surjective_pr2 H0 H1). exists x0. eee. Qed. Definition Acreate (x y a: Set ) := denote Source_not x ( denote Target_not y ( denote Arrow_not a ( stop))). Lemma source_Acreate : forall x y a, sourceC (Acreate x y a) = x. Proof. ir. uf sourceC; uf Acreate. drw. Qed. Lemma target_Acreate : forall x y a, targetC (Acreate x y a) = y. Proof. ir. uf targetC; uf Acreate; drw. Qed. Lemma arrow_Acreate : forall x y a, arrowC (Acreate x y a) = a. Proof. ir; uf arrowC; uf Acreate; drw. Qed. Definition Alike a := a = Acreate (sourceC a) (targetC a) (arrowC a). Lemma create_Alike : forall s t a, Alike (Acreate s t a). Proof. ir. uf Alike. rw source_Acreate. rw target_Acreate. rw arrow_Acreate. tv. Qed. Section Construction. Variables (x y : Set) (f : EE). Definition Ucreate := Acreate x y (L (Ul x) f). Lemma source_Ucreate : sourceC Ucreate = x. Proof. uf Ucreate. rw source_Acreate. tv. Qed. Lemma target_Ucreate : targetC Ucreate = y. Proof. uf Ucreate. rww target_Acreate. Qed. Lemma ev_Ucreate : forall a , inc a (Ul x) -> ev Ucreate a = f a. Proof. ir. uf ev. uf Ucreate. rw arrow_Acreate. bw. Qed. Lemma arrow_Ucreate : arrowC Ucreate = L (Ul (sourceC Ucreate)) (ev Ucreate). Proof. uf Ucreate. rw arrow_Acreate. rw source_Acreate. uf ev. app L_exten1. ir. rw arrow_Acreate. bw. Qed. End Construction. Lemma Ucreate_extens : forall x x' y y' f g, x = x' -> y = y' -> (forall a, inc a (Ul x) -> f a = g a) -> Ucreate x y f = Ucreate x' y' g. Proof. ir. wr H; wr H0. uf Ucreate. ap uneq. app L_exten1. Qed. Definition Urealizes x y f a := sourceC a = x & targetC a = y & (forall z, inc z (Ul x) -> ev a z = f z). Definition Ulike a := Ucreate (sourceC a) (targetC a) (ev a) = a. Lemma Ucreate_like : forall x y f, Ulike (Ucreate x y f). Proof. ir. uf Ulike. ap Ucreate_extens. ap source_Ucreate. ap target_Ucreate. ir. ap ev_Ucreate. rwi source_Ucreate H. am. Qed. Lemma Ulike_Alike : forall u, Ulike u -> Alike u. Proof. ir. red in H. red. ufi Ucreate H. set (f:=L (Ul (sourceC u)) (ev u)) in H. assert (arrowC u = f). wr H. rw arrow_Acreate. tv. rw H0. sy; am. Qed. Lemma Ucreate_realizes : forall x y f, Urealizes x y f (Ucreate x y f). Proof. ir. pose source_Ucreate. pose target_Ucreate. pose ev_Ucreate. unfold Urealizes. intuition. Qed. Lemma Urealizes_like_eq : forall x y f a, Ulike a -> Urealizes x y f a -> Ucreate x y f = a. Proof. ir. ufi Ulike H. wr H. ap Ucreate_extens; ufi Urealizes H0; ee. sy; am. ee; sy;am. ir; sy; ap H2; am. Qed. Definition Uproperty x y f := Taxioms (Ul x) (Ul y) f. Definition Uaxioms (a : Set) := Uproperty (sourceC a) (targetC a) (ev a). Definition is_morphism (a : Set) := (Uaxioms a & Ulike a). Lemma Uaxioms_from_strong : forall a, is_morphism a -> Uaxioms a. Proof. ir. unfold is_morphism in H. ee;am. Qed. Lemma Ucreate_strong_axioms : forall x y f, Uproperty x y f -> is_morphism (Ucreate x y f). Proof. ir. red. split. red. rw source_Ucreate. rw target_Ucreate. uf Uproperty. uf Taxioms. ir. rw ev_Ucreate. red in H. red in H. app H. am. ap Ucreate_like. Qed. Lemma Ucreate_axioms : forall x y f, Uproperty x y f -> Uaxioms (Ucreate x y f). Proof. ir. ap Uaxioms_from_strong. app Ucreate_strong_axioms. Qed. Lemma Uextens : forall a b, is_morphism a -> is_morphism b -> sourceC a = sourceC b -> targetC a = targetC b -> (forall x, inc x (Ul (sourceC a)) -> ev a x = ev b x) -> a = b. Proof. ir. red in H; red in H0; ee. red in H4. wr H4. sy. ap Urealizes_like_eq. am. red. ee. am. am. ir. app H3. rww H1. Qed. Definition Uidentity x := Ucreate x x (fun y : Set => y). Definition Ucompose a b := Ucreate (sourceC b) (targetC a) (fun y => ev a (ev b y)). Lemma identity_is_morphism : forall x, is_morphism (Uidentity x). Proof. ir. uf Uidentity. ap Ucreate_strong_axioms. uf Uproperty. ap identity_Taxioms. Qed. Lemma left_Uidentity : forall a, is_morphism a -> Ucompose (Uidentity (targetC a)) a = a. Proof. ir. uf Ucompose. ap Urealizes_like_eq. nin H; am. uf Uidentity. red. ee. tv. rww target_Ucreate. ir. rww ev_Ucreate. nin H. app H. Qed. Lemma right_Uidentity : forall a, is_morphism a -> Ucompose a (Uidentity (sourceC a)) = a. Proof. ir. uf Ucompose. ap Urealizes_like_eq. nin H; am. red. uf Uidentity. rww source_Ucreate. ee. tv. tv. ir. rww ev_Ucreate. Qed. Lemma source_Uidentity : forall x, sourceC (Uidentity x) = x. Proof. ir. unfold Uidentity; rewrite source_Ucreate. tv. Qed. Lemma target_Uidentity : forall x, targetC (Uidentity x) = x. Proof. ir. unfold Uidentity; rww target_Ucreate. Qed. Lemma ev_Uidentity : forall x y, inc y (Ul x) -> ev (Uidentity x) y = y. Proof. ir. uf Uidentity. rw ev_Ucreate. tv. am. Qed. Lemma source_Ucompose : forall a b, sourceC (Ucompose a b) = sourceC b. Proof. ir. uf Ucompose; rww source_Ucreate. Qed. Lemma target_Ucompose : forall a b, targetC (Ucompose a b) = targetC a. Proof. ir. uf Ucompose; rww target_Ucreate. Qed. Lemma ev_Ucompose : forall a b y, inc y (Ul (sourceC b)) -> ev (Ucompose a b) y = ev a (ev b y). Proof. ir. uf Ucompose; rww ev_Ucreate. Qed. Lemma source_Uidentity1: forall x, sourceU (Uidentity x) = (Ul x). Proof. ir. uf sourceU. rw source_Uidentity. tv. Qed. Lemma source_Ucompose1: forall f g, (sourceU (Ucompose g f)) = Ul (sourceC f). Proof. ir. uf sourceU. rw source_Ucompose. tv. Qed. Lemma target_Ucompose1: forall f g, (targetU (Ucompose g f)) = Ul (targetC g). Proof. ir. uf targetU. rw target_Ucompose. tv. Qed. Definition Ucomposable (a b : Set) := (Uaxioms a & Uaxioms b & sourceC a = targetC b). Lemma compose_is_morphism : forall a b, Ucomposable a b -> is_morphism (Ucompose a b). Proof. ir. red. ee. red. rw source_Ucompose. rw target_Ucompose. red. red. ir. rw ev_Ucompose. red in H. ee. app H. rw H2. app H1. am. uf Ucompose. ap Ucreate_like. Qed. Lemma Ucompose_axioms : forall a b, Ucomposable a b -> Uaxioms (Ucompose a b). Proof. ir. set (K := compose_is_morphism H). nin K; am. Qed. Lemma Uassociativity : forall a b c , Ucomposable a b -> Ucomposable b c -> Ucompose (Ucompose a b) c = Ucompose a (Ucompose b c). Proof. ir. cp (compose_is_morphism H). cp (compose_is_morphism H0). red in H; red in H0; ee. ap Uextens. ap compose_is_morphism. red. ee. nin H1; am. am. rww source_Ucompose. ap compose_is_morphism. red. ee. am. nin H2;am. rww target_Ucompose. repeat rw source_Ucompose. tv. repeat rw target_Ucompose. tv. rw source_Ucompose. ir. repeat rw ev_Ucompose. tv. am. rw source_Ucompose. am. rw H4. app H3. am. Qed. Definition Uinjective (u : Set) := Uaxioms u & Tinjective (Ul (sourceC u)) (Ul (targetC u)) (ev u). Definition Usurjective (u : Set) := Uaxioms u & Tsurjective (Ul (sourceC u)) (Ul (targetC u)) (ev u). Definition Ubijective (u : Set) := (Uinjective u & Usurjective u). Lemma Uinjective_compose_with : forall u v w , is_morphism u -> is_morphism v -> Uinjective w -> Ucomposable w u -> Ucomposable w v -> Ucompose w u = Ucompose w v -> u = v. Proof. ir. red in H2. red in H3. ee. assert (sourceC (Ucompose w u) = sourceC (Ucompose w v)). rww H4. rwi source_Ucompose H9. rwi source_Ucompose H9. app Uextens. transitivity (sourceC w). sy; am. am. ir. nin H1. nin H11. app H12. rw H8. app H7. rw H6. app H5. wrr H9. transitivity (ev (Ucompose w u) x). rww ev_Ucompose. rw H4. rww ev_Ucompose. wrr H9. Qed. Definition Uinverse (u : Set) := Ucreate (targetC u) (sourceC u) (Tinverse (Ul (sourceC u)) (ev u)). Lemma surjective_inverse_Uaxioms : forall u, Usurjective u -> is_morphism (Uinverse u). Proof. ir. red. uf Uinverse. ee. ap Ucreate_axioms. red. ap surjective_inverse_Taxioms. red in H. ee. am. uf Tinverse. ap Ucreate_like. Qed. Lemma Usurjective_composable_left : forall u, Usurjective u -> Ucomposable (Uinverse u) u. Proof. ir. red. ee. ap Uaxioms_from_strong. ap surjective_inverse_Uaxioms. am. red in H; ee; am. uf Uinverse. rww source_Ucreate. Qed. Lemma Usurjective_composable_right : forall u, Usurjective u -> Ucomposable u (Uinverse u). Proof. ir. red. ee. red in H; ee; am. ap Uaxioms_from_strong. ap surjective_inverse_Uaxioms. am. uf Uinverse. rww target_Ucreate. Qed. Lemma Usurjective_inverse_right : forall u, Usurjective u -> Ucompose u (Uinverse u) = Uidentity (targetC u). Proof. ir. assert (Uaxioms u). red in H. ee; am. ap Uextens. ap compose_is_morphism. app Usurjective_composable_right. ap identity_is_morphism. rw source_Ucompose. uf Uinverse. rw source_Ucreate. rww source_Uidentity. rw target_Ucompose. rww target_Uidentity. ir. rwi source_Ucompose H1. rww ev_Ucompose. uf Uinverse. ufi Uinverse H1. rwi source_Ucreate H1. rww ev_Ucreate. rww ev_Uidentity. red in H. ee. ap (Tsurjective_inverse_right H2 H1). Qed. Lemma Ubijective_transformation_bijective : forall u, Ubijective u -> Tbijective (Ul (sourceC u)) (Ul (targetC u)) (ev u). Proof. ir. red in H. ufi Uinjective H; ufi Usurjective H. red. ufi Uaxioms H. ufi Uproperty H. intuition. Qed. Lemma Utransformation_bijective_bijective : forall u, Uaxioms u -> Tbijective (Ul (sourceC u)) (Ul (targetC u)) (ev u) -> Ubijective u. Proof. ir. red in H0. red. uf Uinjective; uf Usurjective. intuition. Qed. Definition are_Uinverse u v := Ucomposable u v & Ucomposable v u & Ucompose u v = Uidentity (sourceC v) & Ucompose v u = Uidentity (sourceC u). Lemma Uinverse_symm : forall u v, are_Uinverse u v -> are_Uinverse v u. Proof. uf are_Uinverse. ir. ee; am. Qed. Lemma Uinverse_unique : forall u v w, is_morphism v -> is_morphism w -> are_Uinverse u v -> are_Uinverse u w -> v = w. Proof. ir. transitivity (Ucompose v (Uidentity (sourceC v))). sy. app right_Uidentity. red in H1; red in H2. ee. assert (sourceC v = targetC u). red in H6; ee; am. assert (sourceC v = sourceC w). rw H9. sy. red in H3; ee; am. rw H10. wr H4. wr Uassociativity. rw H8. red in H2. ee. rw H12. app left_Uidentity. am. am. Qed. Definition has_Uinverse (u:Set) := ex (fun v => are_Uinverse u v). Lemma are_Uinverse_Tinverse : forall u v, are_Uinverse u v -> are_Tinverse (Ul (sourceC u)) (Ul (targetC u)) (ev u) (ev v). Proof. uf are_Uinverse. uf are_Tinverse. ir. ufi Ucomposable H. ee. red in H. am. wr H4. rw H6. red in H5. am. ir. transitivity (ev (Ucompose v u) x). sy; app ev_Ucompose. rw H2. app ev_Uidentity. ir. wri H4 H7. transitivity (ev (Ucompose u v) y). rww ev_Ucompose. rw H1. rww ev_Uidentity. Qed. Lemma Uinverse_bijective : forall u v, are_Uinverse u v -> Ubijective u. Proof. ir. ap Utransformation_bijective_bijective. red in H; ee. red in H; ee. am. apply Tinverse_bijective with (ev v). app are_Uinverse_Tinverse. Qed. Lemma Ubijective_inverse : forall u, Ubijective u -> are_Uinverse u (Uinverse u). Proof. ir. red in H. ee. cp (Usurjective_composable_left H0). cp (Usurjective_composable_right H0). cp (Usurjective_inverse_right H0). red. ee. am. am. rw H3. red in H1; ee. rw H5. app refl_equal. apply Uinjective_compose_with with u. app compose_is_morphism. app identity_is_morphism. am. red. rw target_Ucompose. ee. red in H; ee. am. app Ucompose_axioms. red in H2. ee. am. red. split. red in H; ee; am. split. nin (identity_is_morphism (sourceC u)). am. rww target_Uidentity. wrr Uassociativity. rw H3. ap Uextens. ap compose_is_morphism. red. ee. nin (identity_is_morphism (targetC u)). am. red in H; ee; am. rww source_Uidentity. ap compose_is_morphism. red. ee. red in H; ee; am. nin (identity_is_morphism (sourceC u)). am. rww target_Uidentity. rw source_Ucompose. rww source_Ucompose. rw source_Uidentity. tv. rw target_Ucompose. rw target_Ucompose. rw target_Uidentity. tv. rw source_Ucompose. ir. repeat rewrite ev_Ucompose. repeat rewrite ev_Uidentity. tv. am. red in H. ee. red in H. ee. app H. rw source_Uidentity. am. am. Qed. Lemma Ubijective_has_inverse : forall u, Ubijective u -> has_Uinverse u. Proof. ir. red. exists (Uinverse u). app Ubijective_inverse. Qed. Lemma Ubijective_eq_has_inverse : forall u, Ubijective u = has_Uinverse u. Proof. ir. ap iff_eq; ir. ap Ubijective_has_inverse. am. nin H. apply Uinverse_bijective with x. am. Qed. Lemma Ubijective_eq_inverse : forall u, Ubijective u = are_Uinverse u (Uinverse u). Proof. ir. ap iff_eq; ir. app Ubijective_inverse. apply Uinverse_bijective with (Uinverse u); am. Qed. Lemma Uhas_inverse_eq_inverse : forall u, has_Uinverse u = are_Uinverse u (Uinverse u). Proof. ir. wr Ubijective_eq_inverse. rww Ubijective_eq_has_inverse. Qed. Lemma map_axioms_from_mor:forall m, is_morphism m -> Maxioms (sourceU m) (targetU m) (arrowC m). Proof. uf sourceU; uf targetU. ir. red in H. ee. red in H0. assert (arrowC (Ucreate (sourceC m) (targetC m) (ev m)) = arrowC m). rww H0. rwi arrow_Ucreate H1. rwi H0 H1. wr H1. wr trans_map_axioms. red in H. red in H. am. Qed. Lemma function_axioms_from_mor:forall m, is_morphism m -> fgraph (arrowC m). Proof. ir. nin (map_axioms_from_mor H). am. Qed. Lemma mor_domain:forall m, is_morphism m -> domain (arrowC m) = sourceU m. Proof. ir. nin (map_axioms_from_mor H). nin H1; am. Qed. Lemma mor_target:forall m, is_morphism m ->sub (range (arrowC m)) (targetU m). Proof. ir. nin(map_axioms_from_mor H). nin H1. am. Qed. Lemma mor_inc_target:forall m x, is_morphism m ->inc x (sourceU m) -> inc (ev m x) (targetU m). Proof. ir. app mor_target. assert (inc x (domain (arrowC m))). rww mor_domain. rw frange_inc_rw. exists x. split. am. uf ev. tv. app function_axioms_from_mor. Qed. Lemma mor_inc_ev: forall f x, Uaxioms f -> inc x (sourceU f) -> inc (ev f x) (targetU f). Proof. ir. red in H. red in H. red in H. app H. Qed. Definition mor_image (x m: Set) := fun_image x (fun u=> ev m u). Definition mor_inv_image (x m:Set):= inverse_image x (arrowC m). Definition mor_range (m:Set) := range (L (sourceU m)(ev m)). Lemma mor_image_inc_rw: forall x m y, inc y (mor_image x m)= exists z, (inc z x & ev m z=y). Proof. ir. uf mor_image. ap iff_eq. ir. awi H. am. ir. aw. Qed. Lemma mor_range_inc_rw: forall f y, inc y (mor_range f) = (exists x, inc x (sourceU f) & ev f x = y). Proof. ir. uf mor_range. rw frange_inc_rw. bw. app iff_eq. ir. nin H. ee. exists x. bwi H0. split. am. sy;am. am. ir. nin H. exists x. bw. ee. am. sy. am. ee; am. gprops. Qed. Lemma range_is_image: forall f, mor_range f= mor_image (sourceU f) f. Proof. ir. set_extens. rwi mor_range_inc_rw H. rw mor_image_inc_rw. am. rw mor_range_inc_rw. rwi mor_image_inc_rw H. am. Qed. Lemma mor_inv_image_pr : forall a m x, is_morphism m-> inc x (mor_inv_image a m) -> (inc x (sourceU m) & inc (ev m x) a). Proof. ir. split. ufi mor_inv_image H0. red in H. ee. red in H1. wri H1 H0. rwi arrow_Ucreate H0. rwi H1 H0. pose (f := (L (sourceU m) (ev m))). assert (inc x (domain f)). app (inverse_image_sub H0). unfold f in H2. rwi L_domain H2. am. uf ev. ufi mor_inv_image H. app inverse_image_pr. Qed. Lemma mor_inv_image_pr_s : forall a m x, inc x (mor_inv_image a m) -> inc (ev m x) a. Proof. ir. uf ev. ufi mor_inv_image H. app inverse_image_pr. Qed. Lemma mor_inv_image_inc : forall a m x, is_morphism m -> inc x (sourceU m) -> inc (ev m x) a -> inc x (mor_inv_image a m). Proof. ir. uf mor_inv_image. app inverse_image_inc. rww mor_domain. Qed. Lemma inverse_image_sub : forall a m, is_morphism m-> sub (mor_inv_image a m) (sourceU m). Proof. ir. uf mor_inv_image. wrr mor_domain. app inverse_image_sub. Qed. Lemma increasing_image: forall m x z, sub x z -> sub (mor_image x m) (mor_image z m). Proof. ir. red. ir. rwi mor_image_inc_rw H0. nin H0. ee. rw mor_image_inc_rw. exists x1. ee. app H. am. Qed. Lemma increasing_invimage: forall m x z, is_morphism m-> sub x z -> sub (mor_inv_image x m) (mor_inv_image z m). Proof. ir. red. ir. pose (mor_inv_image_pr H H1). ee. app mor_inv_image_inc. app H0. Qed. Lemma sub_mor_inv: forall m z, sub (mor_image (mor_inv_image z m) m) z. Proof. ir. red. ir. rwi mor_image_inc_rw H. nin H. ee. wrr H0. app mor_inv_image_pr_s. Qed. Lemma sub_inv_image: forall m z w, is_morphism m-> sub z (sourceU m) -> sub (mor_image z m) w -> sub z (mor_inv_image w m). Proof. ir. red. ir. app mor_inv_image_inc. app H0. app H1. rw mor_image_inc_rw. exists x. split. am. tv. Qed. Lemma sub_inv_image2: forall m z w, is_morphism m-> sub z (sourceU m) -> sub z (mor_inv_image w m)-> sub (mor_image z m) w. Proof. ir. red. ir. rwi mor_image_inc_rw H2. nin H2. ee. red in H1. wr H3. app mor_inv_image_pr_s. app H1. Qed. Definition mor_restr (m z:Set):= Ucreate z (targetC m) (ev m). Lemma source_mor_restr: forall f z, sourceC (mor_restr f z) = z. Proof. ir. uf mor_restr. app source_Ucreate. Qed. Lemma target_mor_restr: forall f z, targetC (mor_restr f z) = targetC f. Proof. ir. uf mor_restr. app target_Ucreate. Qed. Lemma ev_mor_restr:forall a f z, inc a (Ul z) -> ev (mor_restr f z) a = ev f a. Proof. ir. uf mor_restr. app ev_Ucreate. Qed. Lemma surjective_pr8: forall f a, Usurjective f -> inc a (targetU f) -> (ev f (Tinverse (sourceU f) (ev f) a) =a &inc (Tinverse (sourceU f) (ev f) a ) (sourceU f)). Proof. ir. induction H. induction H1. pose (H2 _ H0). assert(Hy:= choose_pr e). induction Hy. split. am. am. Qed. Definition mor_to_arrow (f:Set) (hyp: Uaxioms f) (x:sourceU f) := chooseT (fun a: (targetU f) => Ro a = ev f (Ro x)) (inc_nonempty(hyp (Ro x)(R_inc x))). Lemma mor_to_arrow_pr: forall f (x:sourceU f) (hyp:Uaxioms f), Ro(mor_to_arrow hyp x) = ev f (Ro x). Proof. ir. uf mor_to_arrow. app chooseT_pr. apply (hyp (Ro x) (R_inc x)). Qed. End Transformation. Export Transformation. Module Blist. Import List. (** Nonempty lists and functions with totally ordered finite domain *) Lemma interval_Bnat_co_pr: forall n, inc n Bnat -> (induced_order Bnat_order (interval_Bnat card_zero n)) = interval_Bnatco (succ n). Proof. ir. uf interval_Bnatco. wrr interval_co_cc. set (x:= (interval_Bnat card_zero n)). uf Bnat_order. uf graph_on. uf induced_order. set_extens. nin (intersection2_both H0). Ztac. Ztac. app intersection2_inc. Ztac. awi H1. ee. aw. ee. am. app (sub_interval_Bnat H5). app (sub_interval_Bnat H6). Qed. Lemma the_least_interval1: forall n, inc n Bnat -> the_least_element (interval_Bnatco (succ n)) = card_zero. Proof. ir. wrr interval_Bnat_co_pr. uf interval_Bnat. app the_least_interval. nin (Bnat_order_worder). am. rw Bnat_order_le. red. ee. fprops. am. app zero_smallest. fprops. Qed. Lemma the_greatest_interval1: forall n, inc n Bnat -> the_greatest_element (interval_Bnatco (succ n)) = n. Proof. ir. wrr interval_Bnat_co_pr. uf interval_Bnat. app the_greatest_interval. nin (Bnat_order_worder). am. rw Bnat_order_le. red. ee. fprops. am. app zero_smallest. fprops. Qed. Lemma the_greatest_interval2: forall n, inc n Bnat -> n <> card_zero -> the_greatest_element (interval_Bnatco n) = predc n. Proof. ir. rwi inc_Bnat H. nin (predc_pr H H0). wri inc_Bnat H1. rw H2. rw the_greatest_interval1. wrr H2. am. Qed. Lemma the_least_interval2: forall n, inc n Bnat -> n <> card_zero -> the_least_element (interval_Bnatco n) = card_zero. Proof. ir. rwi inc_Bnat H. nin (predc_pr H H0). wri inc_Bnat H1. rw H2. app the_least_interval1. Qed. Lemma nonempty_interval: forall n, inc n Bnat -> n <> card_zero -> nonempty (interval_co_0a n). Proof. ir. exists card_zero. rw interval_co_0a_pr2. split. app zero_smallest. fprops. intuition. am. Qed. Lemma nonempty_compl_singleton: forall x E, cardinal_le card_two (cardinal E) -> nonempty (complement E (singleton x)). Proof. ir. nin (card_le_two_prop H). nin H0. ee. nin (equal_or_not x0 x). exists x1. srw. ee. am. wr H3. red. ir. elim H2. rww (singleton_eq H4). exists x0. srw. ee. am. red. ir. elim H3. rww (singleton_eq H4). Qed. Lemma the_least_singleton: forall r x, total_order r -> substrate r = singleton x -> the_least_element r = x. Proof. ir. assert (inc x (substrate r)). rw H0. fprops. nin H. app the_least_element_pr2. red. ee. am. ir. rwi H0 H3. rw (singleton_eq H3). wrr order_reflexivity. Qed. Definition restriction_compl_singl f x:= restriction2 f (complement (source f) (singleton x)) (complement (target f) (singleton (W x f))). Lemma restriction_compl_singl1: forall f x, is_function f -> inc x (source f) -> (forall y, inc y (source f) -> W x f = W y f -> x = y) -> restriction2_axioms f (complement (source f) (singleton x)) (complement (target f) (singleton (W x f))). Proof. ir. red. ee. am. app sub_complement. app sub_complement. red. ir. awi H2. nin H2. ee. srwi H2. ee. srw. ee. wr H3. fprops. red. ir. rwi (singleton_eq H5) H3. elim H4. symmetry in H3. rw (H1 _ H2 H3). fprops. am. app sub_complement. Qed. Lemma restriction_compl_singl2: forall f x, inc x (source f) -> injective f -> injective (restriction_compl_singl f x). Proof. ir. nin H0. uf restriction_compl_singl. assert (forall y, inc y (source f) -> W x f = W y f -> x = y). ir. app H1. cp (restriction_compl_singl1 H0 H H2). red. ee. app restriction2_function. intros x0 y Ha Hb. ufi restriction2 Ha. ufi restriction2 Hb. awi Ha. awi Hb. rww restriction2_W. rww restriction2_W. app H1. srwi Ha. ee. am. srwi Hb. ee. am. Qed. Lemma restriction_compl_singl3: forall f x, inc x (source f) -> bijective f -> bijective (restriction_compl_singl f x). Proof. ir. nin H0. set (g:=restriction_compl_singl f x). assert (injective g). uf g. app restriction_compl_singl2. split. am. app surjective_pr6. nin H2; am. ir. ufi g H3. ufi restriction_compl_singl H3. ufi restriction2 H3. awi H3. srwi H3. ee. nin (surjective_pr2 H1 H3). ee. assert (inc x0 (complement (source f) (singleton x))). srw. ee. am. red. ir. rwi (singleton_eq H7) H6. rwi H6 H4. elim H4. fprops. exists x0. ee. uf g. uf restriction_compl_singl. uf restriction2. aw. uf g. uf restriction_compl_singl. rww restriction2_W. nin H0. assert (forall y, inc y (source f) -> W x f = W y f -> x = y). ir. app H8. ap (restriction_compl_singl1 H0 H H9). Qed. Lemma todf_order_isomorphism3: forall f r r' x, order_isomorphism f r r' -> inc x (source f) -> order_isomorphism (restriction_compl_singl f x) (induced_order r (complement (source f) (singleton x))) (induced_order r' (complement (target f) (singleton (W x f)))). Proof. ir. set (sf := complement (source f) (singleton x)). set (tf:= complement (target f) (singleton (W x f))). set (g:=restriction_compl_singl f x). assert (Hw:is_function g). app bij_is_function. uf g. app restriction_compl_singl3. red in H; ee; am. assert (forall a, inc a sf -> W a f = W a g). ir. uf g. uf restriction_compl_singl. rww restriction2_W. nin H. ee. nin H3. nin H3. assert (forall y, inc y (source f) -> W x f = W y f -> x = y). ir. app H8. ap (restriction_compl_singl1 H3 H0 H9). red. red in H. ee. assert (sub sf (substrate r)). uf sf. rw H4. app sub_complement. fprops. assert (sub tf (substrate r')). uf tf. rw H5. app sub_complement. fprops. uf g. app restriction_compl_singl3. uf g. uf restriction_compl_singl. uf restriction2. aw. rw H4. uf sf. app sub_complement. aw. uf g. uf restriction_compl_singl. uf restriction2. aw. rw H5. uf tf. app sub_complement. assert (Ht: tf = target g). uf g. uf restriction_compl_singl. uf restriction2. aw. ir. assert (inc (W x0 g) tf). rw Ht. fprops. assert (inc (W y g) tf). rw Ht. fprops. ufi g H7. ufi restriction_compl_singl H7. ufi restriction2 H7. awi H7. ufi g H8. ufi restriction_compl_singl H8. ufi restriction2 H8. awi H8. aw. rww H6. wrr H1. wrr H1. srwi H7; ee; am. srwi H8; ee; am. Qed. Definition tofd_function f r := total_order r & is_function f & is_finite_set (substrate r) & source f = substrate r. Definition tofd_graph f r := total_order r & fgraph f & is_finite_set (substrate r) & domain f = substrate r. Definition iid_graph f := fgraph f & exists n, domain f = interval_co_0a (nat_to_B n). Definition tofd_to_iid_aux r := inverse_fun ( choose (fun g => order_isomorphism g r (interval_Bnatco (cardinal (substrate r))))). Definition tofd_to_iid r f := compose f (tofd_to_iid_aux r). Definition tofd_to_iid_graph r f := compose_graph f (graph (tofd_to_iid_aux r)). Lemma tofd_to_iid_pr1: forall r, total_order r -> is_finite_set (substrate r) -> order_isomorphism (tofd_to_iid_aux r) (interval_Bnatco (cardinal (substrate r))) r. Proof. ir. uf tofd_to_iid_aux. app inverse_order_isomorphism. app choose_pr. nin (finite_ordered_interval1 H H0). am. Qed. Lemma tofd_to_iid_pr2: forall r f, tofd_function f r -> composable f (tofd_to_iid_aux r). Proof. ir. red in H. ee. cp (tofd_to_iid_pr1 H H1). red in H3. red. ee. am. app bij_is_function. wrr H7. Qed. Lemma tofd_to_iid_pr3: forall r f, tofd_function f r -> is_function (tofd_to_iid r f). Proof. ir. uf tofd_to_iid. app compose_function. app tofd_to_iid_pr2. Qed. Lemma tofd_to_iid_pr4: forall r f, tofd_function f r -> target (tofd_to_iid r f) = target f. Proof. ir. uf tofd_to_iid. aw. Qed. Lemma tofd_to_iid_pr5: forall r f, tofd_function f r -> source (tofd_to_iid r f) = interval_co_0a (cardinal (source f)). Proof. ir. red in H. ee. cp (tofd_to_iid_pr1 H H1). rw H2. uf tofd_to_iid. red in H3. ee. rwi interval_Bnatco_substrate H6. rw H6. aw. rw inc_Bnat. exact H1. Qed. Lemma tofd_to_iid_pr6: forall r f, tofd_function f r -> iid_function (tofd_to_iid r f). Proof. ir. red. ee. app tofd_to_iid_pr3. rww tofd_to_iid_pr5. exists (cardinal_nat (cardinal (source f))). rww nat_to_B_pr. red in H. ee. rw inc_Bnat. rw H2. exact H1. Qed. Lemma tofd_graph_pr1: forall f r, is_function f -> (tofd_function f r) = (tofd_graph (graph f) r). Proof. ir. uf tofd_function. uf tofd_graph. pose (function_fgraph H). rw (f_domain_graph H). ap iff_eq; intuition. Qed. Lemma tofd_graph_pr2: forall f, is_function f -> iid_function f = iid_graph (graph f). Proof. ir. uf iid_function. uf iid_graph. rw (f_domain_graph H). pose (function_fgraph H). ap iff_eq; intuition. Qed. Lemma tofd_graph_pr3: forall r f, tofd_graph f r -> tofd_to_iid_graph r f = graph (tofd_to_iid r (corresp (domain f) (range f) f)). Proof. ir. red in H. ee. set (g:= corresp (domain f) (range f) f). assert (is_function g). uf g. app is_function_pr. fprops. uf tofd_to_iid_graph. uf tofd_to_iid. nin (tofd_to_iid_pr1 H H1). set (h:= tofd_to_iid_aux r) in *. ee. clear H9. cp (bij_is_function H6). uf compose. aw. red in H0; ee. rw graph_exten; fprops. assert (graph g = f). uf g. aw. rww H11. Qed. Lemma tofd_to_iid_pr7: forall r f, tofd_function f r -> (source f = emptyset) = (source (tofd_to_iid r f) = interval_co_0a card_zero). Proof. ir. rww tofd_to_iid_pr5. ap iff_eq. ir. rw H0. rww cardinal_zero. ir. assert (inc (cardinal (source f)) Bnat). rww inc_Bnat. red in H. ee. rww H3. app cardinal_nonemptyset. cp (f_equal cardinal H0). do 2 rwii cardinal_interval_co_0a1 H2. fprops. Qed. Definition tonefs_order r := total_order r & is_finite_set (substrate r) & nonempty (substrate r). Lemma tonefs_order_isomorphism1: forall f r r', order_isomorphism f r r' -> tonefs_order r = tonefs_order r'. Proof. ir. assert (Ha:total_order r = total_order r'). red in H. ee. uf total_order. ap iff_eq; ir; ee. am. ir. rwi H3 H7. rwi H3 H8. nin H1. nin (surjective_pr2 H9 H7). nin (surjective_pr2 H9 H8). ee. wr H13. wr H12. uf gge. wrr H4. wrr H4. rwi H2 H6. nin (H6 _ _ H10 H11); [left | right]; am. am. ir. rwi H2 H7; rwi H2 H8. uf gge. rww H4. rww H4. rwi H3 H6. cp (bij_is_function H1). nin (H6 _ _ (inc_W_target H9 H7)(inc_W_target H9 H8)); [left | right]; am. assert (Hb:is_finite_set (substrate r) = is_finite_set (substrate r')). red in H. ee. rw H2. rw H3. uf is_finite_set. assert (cardinal (source f) = cardinal (target f)). aw. exists f. intuition. rww H5. uf tonefs_order. assert (nonempty (substrate r) = nonempty (substrate r')). red in H. ee. rw H2. rw H3. nin H1. ap iff_eq;ir; nin H6. nin H1. exists (W y f). fprops. nin (surjective_pr2 H5 H6). ee. exists x. am. rw Ha. rw Hb. rww H0. Qed. Lemma tonefs_least_element_pr: forall r, tonefs_order r -> least_element r (the_least_element r). Proof. ir. red in H. ee. app the_least_element_pr. nin H; am. app worder_least. app finite_set_torder_worder. Qed. Lemma tonefs_greatest_element_pr: forall r, tonefs_order r -> greatest_element r (the_greatest_element r). Proof. ir. red in H. ee. app the_greatest_element_pr. nin H; am. app finite_set_torder_greatest. Qed. Lemma todf_order_isomorphism1: forall f r r', tonefs_order r -> order_isomorphism f r r' -> W (the_least_element r) f = (the_least_element r'). Proof. ir. cp (tonefs_least_element_pr H). set (x :=the_least_element r) in *. rwi (tonefs_order_isomorphism1 H0) H. cp (tonefs_least_element_pr H). nin H0. red in H1. ee. nin H5. nin H5. rwi H6 H1. assert (least_element r' (W x f)). red. ee. rw H7. fprops. ir. rwi H7 H11. nin (surjective_pr2 H9 H11). ee. wr H13. wrr H8. app H4. rww H6. ap (unique_least H3 H11 H2). Qed. Lemma todf_order_isomorphism2: forall f r r', tonefs_order r -> order_isomorphism f r r' -> W (the_greatest_element r) f = (the_greatest_element r'). Proof. ir. cp (tonefs_greatest_element_pr H). set (x :=the_greatest_element r) in *. rwi (tonefs_order_isomorphism1 H0) H. cp (tonefs_greatest_element_pr H). nin H0. red in H1. ee. nin H5. nin H5. rwi H6 H1. assert (greatest_element r' (W x f)). red. ee. rw H7. fprops. ir. rwi H7 H11. nin (surjective_pr2 H9 H11). ee. wr H13. wrr H8. app H4. rww H6. ap (unique_greatest H3 H11 H2). Qed. Lemma the_least_tofd: forall r f, tofd_function f r -> nonempty (substrate r) -> W card_zero (tofd_to_iid r f) = W (the_least_element r) f. Proof. ir. uf tofd_to_iid. cp (tofd_to_iid_pr5 H). cp (tofd_to_iid_pr2 H). assert (source (tofd_to_iid_aux r) = source (tofd_to_iid r f)). uf tofd_to_iid. aw. set (n:= cardinal (source f)). assert (inc n Bnat). rw inc_Bnat. red in H. ee. uf n. rww H6. assert (n = cardinal (substrate r)). red in H. ee. wrr H7. cp (cardinal_nonemptyset1 H0). assert (inc card_zero (source (tofd_to_iid_aux r))). red in H. ee. rw H3. rw H1. rw interval_co_0a_pr2. split. fprops. fold n. rw H5. intuition. am. rww compose_W. cut (W card_zero (tofd_to_iid_aux r) = (the_least_element r)). ir. rww H8. assert (tonefs_order (interval_Bnatco (cardinal (substrate r)))). red. wr H5. rw interval_Bnatco_substrate. ee. ap (worder_total (interval_Bnatco_worder H4)). red. rw cardinal_interval_co_0a1. wrr inc_Bnat. am. app nonempty_interval. rww H5. am. red in H. ee. cp (tofd_to_iid_pr1 H H10). wr (todf_order_isomorphism1 H8 H12). rww the_least_interval2. wrr H5. Qed. Lemma the_greatest_tofd: forall r f p, tofd_function f r -> inc p Bnat -> source (tofd_to_iid r f) = interval_co_0a (succ p) -> W p (tofd_to_iid r f) = W (the_greatest_element r) f. Proof. ir. uf tofd_to_iid. cp (tofd_to_iid_pr5 H). cp (tofd_to_iid_pr2 H). assert (source (tofd_to_iid_aux r) = source (tofd_to_iid r f)). uf tofd_to_iid. aw. set (n:= cardinal (source f)). assert (inc n Bnat). rw inc_Bnat. red in H. ee. uf n. rww H7. assert (n = succ p). rwi H2 H1. cp (f_equal cardinal H1). rwi cardinal_interval_co_0a1 H6. rwi cardinal_interval_co_0a1 H6. am. fprops. am. assert (n = cardinal (substrate r)). red in H. ee. wrr H9. assert (card_zero <> n). rw H6. cp (succ_positive p). nin H8; ee; am. assert (nonempty (substrate r)). nin (emptyset_dichot (substrate r)). elim H8. rw H7. rww H9. rww cardinal_zero. am. assert (inc p (source (tofd_to_iid_aux r))). rw H4. rw H1. rw interval_co_0a_pr3. fprops. am. rww compose_W. cut (W p (tofd_to_iid_aux r) = (the_greatest_element r)). ir. rww H11. assert (tonefs_order (interval_Bnatco (cardinal (substrate r)))). red. wr H7. rw interval_Bnatco_substrate. ee. ap (worder_total (interval_Bnatco_worder H5)). red. rw cardinal_interval_co_0a1. wrr inc_Bnat. am. app nonempty_interval. intuition. am. red in H. ee. cp (tofd_to_iid_pr1 H H13). wr (todf_order_isomorphism2 H11 H15). rww the_greatest_interval2. wrr H7. rw H6. aw. rww predc_pr1. fprops. wrr H7. wr H7. intuition. Qed. Lemma tofd_restriction: forall f r ns, tofd_function f r -> sub ns (substrate r) -> tofd_function (restriction f ns) (induced_order r ns). Proof. ir. red in H. ee. nin H. red. ee. red. ee. fprops. aw. ir. uf gge. aw. ufi gge H4. app H4. app H0. app H0. app restriction_function. rww H3. aw. app (sub_finite_set H0 H2). uf restriction. aw. Qed. Lemma tofd_restriction2: forall f r, let least := the_least_element r in let ns := (complement (substrate r) (singleton least)) in tofd_function f r -> nonempty (substrate r) -> (sub ns (substrate r) & inc least (substrate r) & succ (cardinal ns) = cardinal (substrate r)). Proof. ir. assert (tonefs_order r). red. red in H. ee; am. cp (tonefs_least_element_pr H1). fold least in H2. red in H2. nin H2. ee. uf ns. app sub_complement. am. assert (substrate r = tack_on ns least). set_extens. uf ns. nin (equal_or_not x least). rw H5. fprops. assert (inc x (complement (substrate r) (singleton least))). srw. ee. am. red. ir. elim H5. rw (singleton_eq H6). tv. fprops. nin (tack_on_or H4). ufi ns H5. srwi H5. ee. am. rww H5. rw H4. uf ns. rww cardinal_succ_pr1. Qed. Lemma tofd_restriction3: forall f r, let least := the_least_element r in let ns := (complement (substrate r) (singleton least)) in let f':= restriction f ns in let r':= induced_order r ns in tofd_function f r -> nonempty (substrate r) -> nonempty ns -> (tofd_function f' r' & the_greatest_element r = the_greatest_element r' & W (the_greatest_element r) f = W (the_greatest_element r') f'). Proof. ir. assert (tonefs_order r). red. red in H. ee; am. cp (tonefs_least_element_pr H2). fold least in H3. red in H3. nin H3. assert (sub ns (substrate r)). uf ns. app sub_complement. cp (tofd_restriction H H5). fold f' in H6. fold r' in H6. assert (tonefs_order r'). red. red in H6. ee. am. am. uf r'. aw. nin H2. nin H2; am. cp (tonefs_greatest_element_pr H7). cp (tonefs_greatest_element_pr H2). assert (order r). red in H. ee. red in H. ee. am. assert (inc (the_greatest_element r) ns). uf ns. srw. split. red in H9. ee. am. red. ir. cp (singleton_eq H11). ufi least H12. cp (tonefs_least_element_pr H2). rwi H12 H9. nin (least_not_greatest H10 H13 H9). ufi ns H1. rwi H14 H1. nin H1. srwi H1. nin H1. rwi (singleton_eq H1) H15. elim H15. rwi H14 H3. rw (singleton_eq H3). fprops. cp (greatest_induced H10 H5 H11 H9). rw H12. ee. am. tv. fold r'. rwi H12 H11. fold r' in H11. uf f'. red in H. ee. wri H15 H5. rww restriction_W. Qed. Lemma tofd_restriction4: forall f r b, let least := the_least_element r in let ns := (complement (substrate r) (singleton least)) in let r':= induced_order r ns in tofd_function f r -> nonempty (substrate r) -> inc b (source (tofd_to_iid_aux r')) -> W (succ b) (tofd_to_iid_aux r) = W b (tofd_to_iid_aux r'). Proof. ir. cp (tofd_restriction2 H H0). fold least in H2. fold ns in H2. ee. set (f':=restriction f ns). assert (tofd_function f' r'). uf r'. uf f'. app tofd_restriction. red in H. ee. cp (tofd_to_iid_pr1 H H7). red in H5. ee. cp (tofd_to_iid_pr1 H5 H11). set (u:= cardinal ns) in *. wri H4 H9. assert (ns = substrate r'). uf r'. aw. nin H; am. wri H14 H13. fold u in H13. assert (inc u Bnat). uf u. rw inc_Bnat. rw H14. am. set (h:= BL (fun a => W (succ a) (tofd_to_iid_aux r)) (interval_co_0a u) ns). assert (transf_axioms (fun a => W (succ a) (tofd_to_iid_aux r)) (interval_co_0a u) ns). red. ir. uf ns. assert (inc (succ c) (interval_co_0a (succ u))). rww interval_co_0a_pr3. cp (sub_interval_co_0a_Bnat H16). rwi interval_co_0a_pr2 H16. srw. fprops. fprops. am. srw. ee. red in H9. ee. rw H21. app inc_W_target. app bij_is_function. wrr H20. rww interval_Bnatco_substrate. fprops. red. ir. cp (singleton_eq H18). assert (inc card_zero (interval_co_0a (succ u))). rww interval_co_0a_pr3. fprops. assert (tonefs_order r). red. ee. am. am. am. wri (tonefs_order_isomorphism1 H9) H21. ufi least H19. wri (todf_order_isomorphism1 H21 H9) H19. assert (the_least_element (interval_Bnatco (succ u)) = card_zero). app the_least_interval2. fprops. cp (succ_positive u). nin H22. intuition. rwi H22 H19. red in H9. ee. rwi interval_Bnatco_substrate H25. rwi H25 H17. rwi H25 H20. nin H24. nin H24. cp (H29 _ _ H17 H20 H19). cp (succ_positive c). nin H31. rwi H30 H32. app H32. fprops. assert (injective h). uf h. app bl_injective. ir. nin H9. ee. rwi interval_Bnatco_substrate H22. cp (sub_interval_co_0a_Bnat H17). cp (sub_interval_co_0a_Bnat H18). nin H21. nin H21. assert (succ u0 = succ v). ap H28. wr H22. rww interval_co_0a_pr3. rwi interval_co_0a_pr2 H17. srw. fprops. fprops. am. wr H22. rww interval_co_0a_pr3. rwi interval_co_0a_pr2 H18. srw. fprops. fprops. am. am. ap succ_injective. fprops. fprops. am. fprops. assert (order_isomorphism h (interval_Bnatco u) r'). red. assert (substrate (interval_Bnatco u) = source h). rw interval_Bnatco_substrate. uf h. aw. am. split. nin (interval_Bnatco_worder H15). am. split. nin H5. am. assert (substrate r' = target h). uf r'. uf h. aw. nin H;am. assert (bijective h). ap bijective_if_same_finite_c_inj. wr H18. rw interval_Bnatco_substrate. rww cardinal_interval_co_0a1. uf h. aw. am. wr H18. rw interval_Bnatco_substrate. red. rww cardinal_interval_co_0a1. wrr inc_Bnat. am. am. ee. am. am. am. uf h. aw. ir. aw. red in H9. ee. cp (sub_interval_co_0a_Bnat H21). cp (sub_interval_co_0a_Bnat H22). rwi interval_co_0a_pr2 H21. rwi interval_co_0a_pr2 H22. assert (inc (succ x) (source (tofd_to_iid_aux r))). wr H25. rw interval_Bnatco_substrate. rww interval_co_0a_pr3. srw. fprops. fprops. fprops. assert (inc (succ y) (source (tofd_to_iid_aux r))). wr H25. rw interval_Bnatco_substrate. rww interval_co_0a_pr3. srw. fprops. fprops. fprops. cp (H27 _ _ H30 H31). assert (gle (interval_Bnatco u) x y = cardinal_le x y). rw interval_Bnatco_related. ap iff_eq. ir. ee; am. ir. ee; am. am. rw H33. assert (gle (interval_Bnatco (succ u)) (succ x) (succ y) = cardinal_le x y). rw interval_Bnatco_related. ap iff_eq. ir. ee. wr lt_is_le_succ. wrr lt_n_succ_le0. fprops. fprops. fprops. ir. ee. srw. fprops. fprops. fprops. srw. fprops. fprops. fprops. fprops. wr H34. rw H32. uf r'. aw. app H16. rww interval_co_0a_pr2. app H16. rww interval_co_0a_pr2. am. am. assert (is_finite_set (substrate r')). aw. cp (finite_ordered_interval1 H5 H19). nin H20. assert (substrate r' = ns). uf r'. aw. nin H. am. rwi H22 H21. fold u in H21. cp (inverse_order_isomorphism H13). cp (inverse_order_isomorphism H18). cp (H21 _ _ H23 H24). cp (f_equal inverse_fun H25). rwi inverse_fun_involutive H26. rwi inverse_fun_involutive H26. rw H26. uf h. rw bl_W. tv. am. assert (source (tofd_to_iid_aux r') = source (tofd_to_iid r' f')). uf tofd_to_iid. aw. rwi H27 H1. rwi tofd_to_iid_pr5 H1. rwi H12 H1. ufi r' H1. awi H1. am. nin H; am. am. red. ee. am. am. am. am. nin H17. nin H17. am. red in H13. ee. nin H28; nin H28. nin H28; am. Qed. Definition composition_iid op f := let n := predc (cardinal (source f)) in W n (induction_defined1 (fun i x => op (W (predc (card_sub n i)) f) x) (W n f) n). Lemma composition_iid_pr1 : forall op f, iid_function f -> nonempty (source f) -> exists p, inc p Bnat & source f = interval_co_0a (succ p) & let h:= fun i x : Set => op (W (predc (card_sub p i)) f) x in let g := (induction_defined1 h (W p f) p) in (is_function g & source g = Bnat & W card_zero g = W p f & (forall i : Set, cardinal_lt i p -> W (succ i) g = h i (W i g)) & (composition_iid op f) = (W p g)). Proof. ir. nin H. nin H1. rw H1. set (n:= nat_to_B x) in *. assert (inc n Bnat). uf n. fprops. assert (n = cardinal (source f)). rw H1. rww cardinal_interval_co_0a1. assert (n <> card_zero). rw H3. app (cardinal_nonemptyset1 H0). wr H1. rwi inc_Bnat H2. nin (predc_pr H2 H4). wri inc_Bnat H5. exists (predc n). ee. am. wrr H6. set (p:=predc n) in *. set (h:= fun i x0 : Set => op (W (predc (card_sub p i)) f) x0). cp (induction_defined_pr1 h (W p f) H5). ee. simpl. ee; try am. nin H8. am. uf composition_iid. wr H3. fold p. fold h. tv. Qed. Lemma composition_iid_pr2 : forall op f E, Operations.is_law2I op E -> iid_function f -> nonempty (source f) -> sub (target f) E -> inc (composition_iid op f) E. Proof. ir. destruct (composition_iid_pr1 op H0 H1) as [p [H5 [H3 H4]]]. simpl in H4. ee. rw H9. set (h:= fun i x : Set => op (W (predc (card_sub p i)) f) x) in *. assert (forall i, cardinal_le i p -> inc (W i f) E). ir. app H2. app inc_W_target. red in H0; ee; am. rw H3. rww interval_co_0a_pr3. assert (forall n x, inc x E -> cardinal_lt n p -> inc (h n x) E). ir. uf h. app H. app H10. nin (sub_lt_symmetry H5 H12). am. assert (inc (W p f) E). app H10. fprops. cp (integer_induction_stable1 H5 H12 H11). app H13. app inc_W_target. rw H6. am. Qed. Lemma composition_iid_pr3 : forall op f, iid_function f -> nonempty (source f) -> cardinal (source f) = card_one -> (composition_iid op f) = W card_zero f. Proof. ir. destruct (composition_iid_pr1 op H H0) as [p [H5 [H3 H4]]]. simpl in H4. ee. rw H8. assert (p = card_zero). rwi H3 H1. rwi cardinal_interval_co_0a1 H1. app succ_injective. fprops. fprops. ufi succ H1. rw H1. aw. fprops. fprops. wri H9 H6. rww H6. rww H9. Qed. Definition composition_tofd op r f:= composition_iid op (tofd_to_iid r f). Lemma composition_iid_pr4: forall op f, iid_function f -> let r := interval_Bnatco (cardinal (source f)) in composition_iid op f = composition_tofd op r f. Proof. ir. destruct H as [H [n H0]]. set (m:= nat_to_B n). assert (inc m Bnat). uf m. fprops. assert (m = cardinal (source f)). rw H0. rww cardinal_interval_co_0a1. assert (r = interval_Bnatco m). uf r. wrr H2. assert (substrate r = source f). uf r. rww interval_Bnatco_substrate. red in H. ee. wr H2. sy; am. wrr H2. assert (worder r). rw H3. ap (interval_Bnatco_worder H1). assert (total_order r). ap (worder_total H5). assert (is_finite_set (substrate r)). rw H4. red. wr H2. wrr inc_Bnat. cp (tofd_to_iid_pr1 H6 H7). rwi H4 H8. wri H2 H8. wri H3 H8. red in H8. ee. nin H10. assert (is_segment r (range (graph (tofd_to_iid_aux r)))). rw (surjective_pr3 H14). wr H12. app substrate_is_segment. assert (order_morphism (tofd_to_iid_aux r) r r). red. intuition. cp (unique_isomorphism_onto_segment H5 H15 H16). uf composition_tofd. uf tofd_to_iid. rw H17. rw H4. rww compose_identity_right. nin H;am. Qed. Lemma composition_tofd_pr2 : forall op r f E, Operations.is_law2I op E -> tofd_function f r -> nonempty (source f) -> sub (target f) E -> inc (composition_tofd op r f) E. Proof. ir. uf composition_tofd. app composition_iid_pr2. app tofd_to_iid_pr6. rw (tofd_to_iid_pr5 H0). app nonempty_interval. rw inc_Bnat. red in H0. ee. rww H5. ap (cardinal_nonemptyset1 H1). uf tofd_to_iid. aw. Qed. Lemma composition_tofd_pr3 : forall op r f x, tofd_function f r -> source f = singleton x -> composition_tofd op r f = W x f. Proof. ir. uf composition_tofd. cp (tofd_to_iid_pr5 H). cp (tofd_to_iid_pr4 H). cp (tofd_to_iid_pr6 H). assert (nonempty (source f)). exists x. rw H0. fprops. assert (cardinal (source f) = card_one). rw H0. app cardinal_singleton. assert (nonempty (substrate r)). red in H; ee. wrr H8. assert (x = the_least_element r). red in H. ee. rwi H9 H0. rww (the_least_singleton H H0). rw H7. wr (the_least_tofd H H6). clear H7. nin H. ee. assert (cardinal (source (tofd_to_iid r f)) = card_one). rw H1. rww cardinal_interval_co_0a1. rw H5. fprops. assert (source (tofd_to_iid r f) = interval_co_0a card_one). wrr H5. assert (source (tofd_to_iid_aux r) = source (tofd_to_iid r f)). uf tofd_to_iid. aw. assert (inc card_zero (source (tofd_to_iid_aux r))). rw H12. rw H11. rw interval_co_0a_pr2. split. fprops. cp card_one_not_zero. intuition. fprops. assert (nonempty (source (tofd_to_iid r f))). exists card_zero. wrr H12. rww composition_iid_pr3. Qed. Lemma composition_tofd_pr4 : forall op r f, tofd_function f r -> cardinal_le card_two (cardinal (source f)) -> let least := the_least_element r in let ns := (complement (substrate r) (singleton least)) in let f':= restriction f ns in let r':= induced_order r ns in composition_tofd op r f = op (W least f) (composition_tofd op r' f'). Proof. ir. uf composition_tofd. set (g1:= tofd_to_iid r f). set (g2:= tofd_to_iid r' f'). assert (nonempty (substrate r)). red in H. ee. wr H3. app nonempty_card_ge2. cp (tofd_restriction2 H H1). fold least in H2. fold ns in H2. ee. assert (tofd_function f' r'). uf r'. uf f'. app tofd_restriction. assert (iid_function g1). uf g1. app (tofd_to_iid_pr6 H). assert (iid_function g2). uf g1. app (tofd_to_iid_pr6 H5). assert (nonempty (source g1)). uf g1. rww (tofd_to_iid_pr5 H). app nonempty_interval. rw inc_Bnat. red in H. ee. rww H10. assert (cardinal_lt card_zero card_two). split. fprops. cp card_two_not_zero. intuition. cp (cardinal_lt_le_trans H8 H0). nin H9. intuition. assert (Ht: source f' = ns). uf f'. uf restriction. aw. assert (Ha: inc (cardinal ns) Bnat). rw inc_Bnat. change (is_finite_set ns). app (sub_finite_set H2). red in H. ee. am. assert (nonempty (source g2)). uf g2. rww (tofd_to_iid_pr5 H5). simpl. exists card_zero. rw interval_co_0a_pr2. split. fprops. red. ir. rwi Ht H9. wri H9 H4. ufi succ H4. awi H4. nin H. ee. rwi H12 H0. wri H4 H0. assert (card_two = succ card_one). app card_two_pr. rwi H13 H0. srwi H0. nin H0. elim H14. tv. fprops. fprops. fprops. rww Ht. cp (composition_iid_pr1 op H6 H8). cp (composition_iid_pr1 op H7 H9). nin H10. nin H11. ee. simpl in H15. rename x into p. rename x0 into p'. simpl in H13. set (h1:= fun i x : Set => op (W (predc (card_sub p i)) g1) x) in *. set (h2:= fun i x : Set => op (W (predc (card_sub p' i)) g2) x) in *. set (rec1:= induction_defined1 h1 (W p g1) p) in *. set (rec2:= induction_defined1 h2 (W p' g2) p') in *. ee. rw H23. rw H19. clear H23. clear H19. assert (p = succ p'). cp (tofd_to_iid_pr5 H). fold g1 in H19. rwi H19 H14. cp (f_equal cardinal H14). rwi cardinal_interval_co_0a1 H23. rwi cardinal_interval_co_0a1 H23. nin H. ee. rwi H26 H23. wri H4 H23. cp (tofd_to_iid_pr5 H5). fold g2 in H27. rwi H27 H12. cp (f_equal cardinal H12). rwi cardinal_interval_co_0a1 H28. rwi cardinal_interval_co_0a1 H28. rwi Ht H28. rwi H28 H23. sy. app succ_injective. fprops. fprops. fprops. rww Ht. fprops. red in H. ee. rw H26. rww inc_Bnat. assert (Hw:forall n, inc n Bnat -> cardinal_lt n p' -> W (predc (card_sub p n)) g1 = W (predc (card_sub p' n)) g2). ir. set (a:= predc (card_sub p n)). set (b:=predc (card_sub p' n)). cp H24. nin H25. cp (card_sub_pr H11 H23 H25). set (w := card_sub p' n). assert (w <> card_zero). red. ir. ufi w H28. rwi H28 H27. awi H27. contradiction. fprops. assert (inc w Bnat). uf w. fprops. rwi inc_Bnat H29. cp (predc_pr H29 H28). ee. assert (cardinal_le b p'). wr H27. fold w. rw H31. uf w. fold b. uf succ. rw (card_plus_commutative b card_one). rw card_plus_associative. rw card_plus_commutative. app sum_increasing3. fprops. fprops. assert (a = succ b). uf b. fold w. wr H31. uf a. rw H19. uf succ. wr H27. fold w. wr card_plus_associative. rw card_plus_commutative. rw card_sub_pr1. change (predc (succ w) = w). rww predc_pr1. uf w. fprops. app Bnat_stable_plus. uf w. fprops. fprops. am. assert (inc a (source (tofd_to_iid_aux r))). assert (source (tofd_to_iid_aux r) = source g1). uf g1. uf tofd_to_iid. aw. rw H34. rw H14. rww interval_co_0a_pr3. rw H19. rw H33. uf succ. app sum_increasing2. fprops. assert (inc b (source (tofd_to_iid_aux r'))). assert (source (tofd_to_iid_aux r') = source g2). uf g2. uf tofd_to_iid. aw. rw H35. rw H12. rww interval_co_0a_pr3. uf g1. uf g2. uf tofd_to_iid. rw compose_W; try (exact H34); try exact (tofd_to_iid_pr2 H). rw compose_W; try (exact H35); try exact (tofd_to_iid_pr2 H5). cut (W (succ b) (tofd_to_iid_aux r) = (W b (tofd_to_iid_aux r'))). ir. rw H33. rw H36. uf f'. rw restriction_W. reflexivity. red in H. ee. am. red in H. ee. rww H39. uf ns. cp (tofd_to_iid_pr2 H5). red in H37. ee. red in H5. ee. ufi r' H42. awi H42. ufi ns H42. wr H42. rw H39. app inc_W_target. red in H. ee. nin H; am. am. uf r'. uf ns. uf least. apply tofd_restriction4 with (f:=f). am. am. nin H. ee. am. assert (cardinal_lt p' p). rw H19. rw lt_is_le_succ. fprops. wrr inc_Bnat. rw H19. rw (H22 _ H23). assert (predc (card_sub p p') = card_zero). rw H19. uf succ. rw card_plus_commutative. rww card_sub_pr1. wr succ_zero. app predc_pr1. fprops. fprops. rw H24. uf g1. uf least. rww the_least_tofd. app uneq. cp inc0_Bnat. cut (forall n, inc n (interval_cc Bnat_order card_zero p') -> W n rec1 = W n rec2). ir. app H26. rww Bnat_interval_cc_pr1. split. fprops. fprops. app cardinal_c_induction3_v. rw H17. rw H21. uf g1. uf g2. rww the_greatest_tofd. rww the_greatest_tofd. assert (nonempty ns). uf ns. app nonempty_compl_singleton. nin H. ee. wrr H28. cp (tofd_restriction3 H H1 H26). ee. exact H29. ir. rwii interval_co_0a_pr2 H26. rww H18. assert (cardinal_lt n p). nin H23. ap (cardinal_lt_le_trans H26 H23). rww H22. rww H27. rw Hw. tv. nin H28. rw inc_Bnat. apply le_int_is_int with p. wr inc_Bnat. am. am. am. Qed. Lemma singleton_when_card_one: forall x, cardinal x = card_one -> exists y, x = singleton y. Proof. ir. ufi card_one H. symmetry in H. awi H. nin H. ee. exists (W emptyset x0). set_extens. wri H1 H2. nin H. nin (surjective_pr2 H3 H2). ee. wr H5. rwi H0 H4. rw (singleton_eq H4). fprops. rw (singleton_eq H2). wr H1. app inc_W_target. app bij_is_function. rw H0. fprops. Qed. Lemma image_complement_singleton: forall g J l, bijective g -> sub J (source g) -> inc l J -> complement (image_by_fun g J) (singleton (W l g)) = image_by_fun g (complement J (singleton l)). Proof. ir. set_extens. srwi H2. ee. awi H2. aw. nin H2. exists x0. ee. srw. ee. am. wri H4 H3. red. ir. elim H3. rw (singleton_eq H5). fprops. am. app bij_is_function. apply sub_trans with J. app sub_complement. am. app bij_is_function. am. awi H2. nin H2. ee. srwi H2. ee. wr H3. srw. split. aw. exists x0. split. am. tv. app bij_is_function. red. ir. elim H4. cp (singleton_eq H5). nin H. nin H. cp (H0 _ H2). cp (H0 _ H1). rw (H8 _ _ H9 H10 H6). fprops. app bij_is_function. apply sub_trans with J. app sub_complement. am. Qed. Lemma double_restriction: forall f a b, is_function f -> sub a b -> sub b (source f) -> restriction (restriction f b) a = restriction f a. Proof. ir. assert (sub a (source f)). apply sub_trans with b. am. am. assert (is_function (restriction f b)). app restriction_function. ap function_exten. app restriction_function. uf restriction. aw. app restriction_function. uf restriction. aw. uf restriction. aw. ir. ufi restriction H4. awi H4. repeat rww restriction_W. app H0. uf restriction. aw. Qed. Lemma composition_tofd_pr5 : forall op r r' f g, tofd_function f r -> nonempty (source f) -> order_isomorphism g r' r -> composition_tofd op r f = composition_tofd op r' (compose f g). Proof. ir. assert (Hba: order r). red in H1; ee; am. assert (Hca: order r'). red in H1; ee; am. set (rJ' := fun J => induced_order r' J). set (IJ := fun J => image_by_fun g J). set (gJ := fun J => restriction2 g J (IJ J)). set (fJ := fun J=> restriction f (IJ J)). set (rJ := fun J=> induced_order r (IJ J)). assert (Hea: forall J, sub J (substrate r') -> source (fJ J) = IJ J). uf fJ. uf restriction. ir. aw. assert (Hfa: forall J, sub J (substrate r') -> source (gJ J) = J). uf gJ. uf restriction2. ir. aw. assert (Hga: forall J, sub J (substrate r') -> target (gJ J) = IJ J). uf gJ. uf restriction2. ir. aw. assert (Haa: is_function g). app bij_is_function. red in H1; ee; am. assert (Hda: is_function f). red in H; ee; am. assert(Ha: forall J, sub J (substrate r') ->sub (IJ J) (substrate r)). ir. red in H1. ee. rw H6. uf IJ. red. ir. awi H8. nin H8. ee. wr H9. app inc_W_target. wr H5. app H2. am. wrr H5. assert(Hb: forall J, sub J (substrate r') -> restriction2_axioms g J (IJ J)). red. red in H1. ee. ir. ee. am. wrr H4. wr H5. app Ha. uf IJ. fprops. assert(Hc: forall J, sub J (substrate r') -> bijective (gJ J)). red in H1. ee. ir. nin H3. assert (injective (gJ J)). uf gJ. app restriction2_injective. app Hb. split. am. app surjective_pr6. nin H9. am. rww Hfa. uf gJ. aw. ir. ufi IJ H10. ufi restriction2 H10. awi H10. nin H10. ee. wr H11. exists x. split. am. rww restriction2_W. app Hb. nin H3; am. wrr H4. assert (Hd:forall J : Set, sub J (substrate r') -> order_isomorphism (gJ J) (rJ' J) (rJ J)). ir. ir. red in H1. ee. red. rww Hfa. ee. uf rJ'. fprops. uf rJ. fprops. app Hc. uf rJ'. aw. rw Hga. uf rJ. aw. app Ha. am. ir. assert (W x (gJ J) = W x g). uf gJ. rww restriction2_W. app Hb. rw H10. assert (W y (gJ J) = W y g). uf gJ. rww restriction2_W. app Hb. rw H11. uf rJ. uf rJ'. aw. app H7. wrr H5. app H2. wrr H5. app H2. uf IJ. aw. exists x. ee. am. tv. wrr H5. uf IJ. aw. exists y. ee. am. tv. wrr H5. assert (He:tonefs_order r'). rw (tonefs_order_isomorphism1 H1). red. ee. red in H; ee; am. red in H; ee; am. red in H. ee. wrr H4. assert(Hf: forall J, sub J (substrate r') -> nonempty J -> tonefs_order (rJ' J)). ir. red. uf rJ'. aw. red in He. ee. app total_order_sub. ap (sub_finite_set H2 H5). am. assert (Hg:forall J, sub J (substrate r') -> nonempty J -> tofd_function (fJ J) (rJ J)). ir. red. cp (Hf _ H2 H3). rwi (tonefs_order_isomorphism1 (Hd _ H2)) H4. ee. red in H4. ee. am. uf fJ. app restriction_function. red in H. ee. rw H7. app Ha. red in H4; ee; am. rww Hea. uf rJ. aw. app Ha. assert (Hh:forall J, sub J (substrate r') -> nonempty J -> composable (fJ J) (gJ J)). ir. red. ee. nin (Hg _ H2 H3); ee; am. nin (Hd _ H2); ee; app bij_is_function. rww Hea. rww Hga. assert (Hi:forall J, sub J (substrate r') -> nonempty J -> tofd_function (compose (fJ J) (gJ J)) (rJ' J)). ir. red. nin (Hf _ H2 H3). ee. am. app compose_function. app Hh. am. aw. uf rJ'. rww Hfa. aw. set (p2:= fun n => forall J, sub J (substrate r') -> cardinal J = succ n -> composition_tofd op (rJ J) (fJ J) = composition_tofd op (rJ' J) (compose (fJ J) (gJ J))). assert (forall n, inc n Bnat -> p2 n). app cardinal_c_induction_v. uf p2. ir. rwi succ_zero H3. nin (singleton_when_card_one H3). assert (nonempty J). exists x. rw H4. fprops. assert (source (fJ J) = singleton (W x g)). rww Hea. red in H1. ee. uf IJ. set_extens. awi H11. nin H11. nin H11. wr H12. rwi H4 H11. rw (singleton_eq H11). fprops. am. wrr H8. aw. exists x. split. rw H4. fprops. rww (singleton_eq H11). wrr H8. rw (composition_tofd_pr3 op (Hg J H2 H5) H6). assert (source (compose (fJ J) (gJ J)) = singleton x). aw. rww Hfa. rw (composition_tofd_pr3 op (Hi J H2 H5) H7). rw compose_W. assert (W x g = W x (gJ J)). uf gJ. rw restriction2_W. tv. app Hb. rw H4. fprops. rww H8. app Hh. rww Hfa. rw H4. fprops. ir. ufi p2 H3. uf p2. ir. set (aux:= compose (fJ J) (gJ J)). assert (cardinal J = cardinal (source aux)). uf aux. aw. rww Hfa. fprops. assert (cardinal_le card_two (cardinal (source aux))). wr H6. rww H5. uf succ. wr card_plus_associative. wr card_two_pr. rw card_plus_commutative. app sum_increasing3. fprops. fprops. assert(nonempty J). nin (emptyset_dichot J). wri H6 H7. rwi H8 H7. rwi cardinal_zero H7. cp (zero_smallest2 H7). elim card_two_not_zero. am. am. uf aux. rw (composition_tofd_pr4 op (Hi _ H4 H8) H7). assert (cardinal_le card_two (cardinal (source (fJ J)))). rww Hea. assert (cardinal (source aux) = cardinal (IJ J)). uf aux. aw. rww Hfa. exists (gJ J). eee. wrr H9. rw (composition_tofd_pr4 op (Hg _ H4 H8) H9). cp (todf_order_isomorphism1 (Hf _ H4 H8) (Hd _ H4)). set (least := the_least_element (rJ J)) in *. set (least1 := the_least_element (rJ' J)) in *. assert (inc least1 J). cp (tonefs_least_element_pr (Hf _ H4 H8)). red in H11. ee. ufi rJ' H11. awi H11. am. am. am. assert (W least (fJ J) = W least1 aux). uf aux. rw compose_W. rww H10. app Hh. rww Hfa. rw H12. ap uneq. ufi gJ H10. rwi restriction2_W H10 ; [ idtac | apply (Hb _ H4) | exact H11 ]. set (J1 := complement (substrate (rJ' J)) (singleton least1)). assert (J1= complement J (singleton least1)). uf J1. uf rJ'. aw. assert (Hl: sub J1 J). rw H13. app sub_complement. assert (sub J1 (substrate r')). apply sub_trans with J. am. am. assert(cardinal J1 = succ n). assert (succ (cardinal J1) = succ (succ n)). rw H13. wrr cardinal_succ_pr1. wrr tack_on_complement. app succ_injective. fprops. fprops. assert (induced_order (rJ' J) J1 = (rJ' J1)). uf rJ'. sy. app induced_trans. assert (complement (substrate (rJ J)) (singleton least) = substrate (rJ J1)). uf rJ. aw. uf IJ. rw H13. wr H10. app image_complement_singleton. red in H1; ee; am. red in H1. ee. wrr H19. app Ha. app Ha. rw H16. rw H17. assert (sub (IJ J1) (IJ J)). uf IJ. uf image_by_fun. app image_by_increasing. fprops. assert (induced_order (rJ J) (substrate (rJ J1)) = rJ J1). uf rJ. aw. sy. app induced_trans. app Ha. app Ha. assert (restriction (fJ J) (substrate (rJ J1)) = fJ J1). uf fJ. assert (substrate (rJ J1) = IJ J1). uf rJ. aw. app Ha. rw H20. app double_restriction. red in H. ee. rww H23. app Ha. rw H20. rw H19. rw (H3 J1 H14 H15). assert (compose (fJ J1) (gJ J1) = restriction aux J1). uf aux. assert (nonempty J1). nin (emptyset_dichot J1). rwi H21 H15. elim (succ_nonzero (n:=n)). rwi cardinal_zero H15. sy; am. am. cp (Hi _ H14 H21). ap function_exten. red in H22; ee; am. app restriction_function. nin (Hi _ H4 H8). ee; am. aw. rww Hfa. uf restriction2. aw. uf restriction. aw. rww Hfa. uf restriction. aw. uf fJ. uf restriction. aw. aw. rww Hfa. ir. rw restriction_W. rw compose_W. rw compose_W. uf fJ. uf gJ. set (y:= W x (restriction2 g J (IJ J))). assert (y = W x g). uf y. rw restriction2_W. tv. app Hb. app Hl. assert (y= W x (restriction2 g J1 (IJ J1))). rw restriction2_W. am. app Hb. am. wr H25. assert (inc y (IJ J1)). uf IJ. aw. exists x. au. red in H1. ee. wrr H28. rw restriction_W. rw restriction_W. tv. red in H; ee; am. red in H. ee. rww H29. app Ha. app H18. red in H; ee; am. red in H. ee. rww H29. app Ha. am. app Hh. simpl. rww Hfa. app Hl. app Hh. rww Hfa. nin (Hi _ H4 H8). ee; am. aw. rww Hfa. am. rww H21. set (J:= substrate r'). assert (rJ' J = r'). uf J. uf rJ'. app induced_order_substrate. assert (sub J (substrate r')). uf J. fprops. assert (cardinal (substrate r) = cardinal (substrate r')). sy. aw. exists g. red in H1; ee. am. sy;am. sy;am. assert (is_finite_c (cardinal J)). uf J. wr H5. red in H. ee. am. assert (cardinal J <> card_zero). uf J. wr H5. red in H. ee. wr H9. app cardinal_nonemptyset1. cp (predc_pr H6 H7). nin H8. wri inc_Bnat H8. cp (H2 _ H8). cp (H10 _ H4 H9). rwi H3 H11. assert (IJ J = substrate r). uf IJ. uf J. red in H1. ee. rw H14. rw H15. wr image_of_fun_pr. nin H13. red in H17. ee. am. assert (rJ J = r). uf rJ. rw H12. app induced_order_substrate. rwi H13 H11. assert (fJ J = f). uf fJ. rw H12. red in H. ee. wr H16. app function_exten. app restriction_function. fprops. uf restriction. aw. uf restriction. aw. ir. ufi restriction H17. awi H17. rww restriction_W. fprops. rwi H14 H11. rw H11. assert (gJ J = g). uf gJ. red in H1. ee. app function_exten. app restriction2_function. app Hb. uf restriction2. aw. uf restriction2. aw. rww H12. ir. ufi restriction2 H20. awi H20. rww restriction2_W. app Hb. rw H15. app refl_equal. Qed. Definition composition_tofd_lr op r f := composition_tofd (fun u v => op v u) (opposite_order r) f. Lemma tofd_function_opposite: forall r f, tofd_function f r -> tofd_function f (opposite_order r). Proof. ir. red in H; red. assert (substrate (opposite_order r) = substrate r). aw. ee. nin H; am. rw H0. ee; tv. app total_order_opposite. Qed. Lemma composition_tofd_lr_pr3 : forall op r f x, tofd_function f r -> source f = singleton x -> composition_tofd_lr op r f = W x f. Proof. ir. uf composition_tofd_lr. app composition_tofd_pr3. app tofd_function_opposite. Qed. Lemma composition_tofd_lr_pr4 : forall op r f, tofd_function f r -> cardinal_le card_two (cardinal (source f)) -> let greatest := the_greatest_element r in let ns := (complement (substrate r) (singleton greatest)) in let f':= restriction f ns in let r':= induced_order r ns in composition_tofd_lr op r f = op (composition_tofd_lr op r' f') (W greatest f). Proof. ir. uf composition_tofd_lr. assert (order r). nin H. nin H; am. rw composition_tofd_pr4. assert (the_least_element (opposite_order r) = greatest). rww the_least_reverse. exists greatest. uf greatest. app tonefs_greatest_element_pr. red. red in H. ee. am. am. wr H4. app nonempty_card_ge2. rw H2. assert (substrate (opposite_order r) = substrate r). aw. rw H3. fold ns. fold f'. assert (induced_order (opposite_order r) ns = opposite_order r'). uf r'. app opposite_induced. rww H4. app tofd_function_opposite. am. Qed. Lemma composition_tofd_lr_pr5 : forall op r r' f g, tofd_function f r -> nonempty (source f) -> order_isomorphism g r' r -> composition_tofd_lr op r f = composition_tofd_lr op r' (compose f g). Proof. ir. uf composition_tofd_lr. app composition_tofd_pr5. app tofd_function_opposite. app order_isomorphism_opposite. Qed. Definition composition_graph op r f := composition_tofd op r (corresp (domain f) (range f) f). Lemma tofd_graph_prop: forall f r, tofd_graph f r -> tofd_function (corresp (domain f) (range f) f) r. Proof. ir. red in H. ee. red. eee. app is_function_pr. fprops. aw. Qed. Lemma composition_graph_pr3 : forall op r f x, tofd_graph f r -> domain f = singleton x -> composition_graph op r f = V x f. Proof. ir. uf composition_graph. assert (source (corresp (domain f) (range f) f) = singleton x). aw. rw (composition_tofd_pr3 op (tofd_graph_prop H) H1). uf W. aw. Qed. Lemma composition_tofd_pr6 : forall op r f f', tofd_function f r -> nonempty (source f) -> is_function f' -> source f = source f' -> graph f = graph f' -> composition_tofd op r f = composition_tofd op r f'. Proof. intro op. set (p := fun n => forall r f f', tofd_function f r -> cardinal (source f) = succ n -> is_function f' -> source f = source f' -> graph f = graph f' -> composition_tofd op r f = composition_tofd op r f'). assert (forall n, inc n Bnat -> p n). app cardinal_c_induction_v. red. ir. rwi succ_zero H0. nin (singleton_when_card_one H0). rw (composition_tofd_pr3 op H H4). assert (tofd_function f' r). red. red in H. ee. am. am. am. wrr H2. rwi H2 H4. rw (composition_tofd_pr3 op H5 H4). uf W. rww H3. ir. uf p. ir. assert (tofd_function f' r). red. red in H1. ee. am. am. am. wrr H4. assert (cardinal_le card_two (cardinal (source f))). rw H2. assert (card_two = succ card_one). app card_two_pr. rw H7. srw; fprops. wr succ_zero. wr lt_n_succ_le1; fprops. rw (composition_tofd_pr4 op H1 H7). rwi H4 H7. rw (composition_tofd_pr4 op H6 H7). set (ns:= complement (substrate r) (singleton (the_least_element r))). assert (W (the_least_element r) f = (W (the_least_element r) f')). uf W. rw H5. tv. rw H8. ap uneq. app H0. assert (sub ns (substrate r)). uf ns. app sub_complement. red. ee. app total_order_sub. red in H1; ee; am. app restriction_function. red in H1; ee; am. red in H1. ee. rww H12. aw. red in H1. ee. app (sub_finite_set H9 H11). red in H1. ee. nin H1. am. uf restriction. aw. red in H1. ee. nin H1. am. uf restriction. aw. uf ns. set (x := the_least_element r). cp (cardinal_succ_pr1 (substrate r) x). wri tack_on_complement H9. red in H1. ee. rwi H12 H2. rwi H2 H9. sy. app succ_injective. fprops. fprops. assert (tonefs_order r). red. red in H1. ee. am. am. nin (nonempty_compl_singleton x H7). srwi H13. ee. wr H12. rw H4. exists y. am. cp (tonefs_least_element_pr H10). nin H11. am. app restriction_function. wr H4. uf ns. red in H1. ee. rw H11. app sub_complement. uf restriction. aw. uf restriction. aw. rww H5. ir. set (m:= cardinal (source f)). assert (is_finite_c m). red in H0. ee. uf m. rww H7. assert (m <> card_zero). cp (cardinal_nonemptyset1 H1). intuition. cp (predc_pr H5 H6). nin H7. wri inc_Bnat H7. cp (H _ H7). ufi p H9. app H9. Qed. Lemma composition_graph_pr4 : forall op r f, tofd_graph f r -> cardinal_le card_two (cardinal (domain f)) -> let least := the_least_element r in let ns := (complement (substrate r) (singleton least)) in let f':= restr f ns in let r':= induced_order r ns in composition_graph op r f = op (V least f) (composition_graph op r' f'). Proof. ir. uf composition_graph. cp (tofd_graph_prop H). assert (cardinal_le card_two (cardinal (source (corresp (domain f) (range f) f)))). aw. rw composition_tofd_pr4; try exact H1; try exact H2. fold least. assert (W least (corresp (domain f) (range f) f)= V least f). uf W. aw. rw H3. ap uneq. fold ns. fold r'. set (f1 := corresp (domain f') (range f') f'). set (f2 := restriction (corresp (domain f) (range f) f) ns). assert (sub ns (substrate r)). uf ns. app sub_complement. app composition_tofd_pr6. red. red in H. ee. uf r'. app total_order_sub. uf f2. app restriction_function. red in H1; ee; am. aw. rww H7. uf r'. aw. app (sub_finite_set H4 H6). nin H;am. uf f2. aw. uf r'. uf restriction. aw. nin H; am. uf f2. uf restriction. aw. awi H2. uf ns. app nonempty_compl_singleton. red in H. ee. wrr H7. red in H. ee. cp (restr_fgraph ns H5). uf f1. app is_function_pr. fprops. uf f1. uf f2. uf restriction. aw. uf f'. rw restr_domain. set_extens. app intersection2_inc. nin H. ee. ue. ap (intersection2_second H5). nin H. ee; am. uf f1. uf f2. uf restriction. aw. Qed. (** ** Non empty lists *) Inductive nelist (A:Type): Type := singl: A -> nelist A | necons : A-> nelist A -> nelist A. Fixpoint nelist_to_list (A:Type) (u:nelist A): list A := match u with | singl u => cons u nil | necons a b => cons a (nelist_to_list b) end. Fixpoint list_to_nelist(A:Type)(u:list A)(e:A): nelist A := match u with | nil => singl e | cons a nil => singl a | cons a b => necons a (list_to_nelist b e) end. Lemma nonempty_nelist: forall (A:Type) (l:nelist A), nelist_to_list l <> nil. Proof. ir. induction l. unfold nelist_to_list. discriminate. unfold nelist_to_list. discriminate. Qed. Lemma list_is_nelist: forall (A:Type) (e:A) (l:list A), l <> nil -> nelist_to_list (list_to_nelist l e) = l. Proof. ir. induction l. elim H. tv. simpl. induction l. simpl. tv. simpl in IHl. simpl. rw IHl. tv. discriminate. Qed. Lemma nelist_is_nelist: forall (A:Type) (e:A) (l:nelist A), list_to_nelist (nelist_to_list l) e = l. Proof. ir. induction l. simpl. tv. simpl. rw IHl. set (w:= nelist_to_list l). assert (w <> nil). uf w. app nonempty_nelist. induction w. elim H; tv. tv. Qed. Fixpoint ne_app (A:Type) (l1 l2: nelist A){struct l1}: nelist A := match l1 with | singl a => necons a l2 | necons a b => necons a (ne_app b l2) end. Lemma ne_app_pr: forall (A:Type)(a b:nelist A), app(nelist_to_list a)(nelist_to_list b) = nelist_to_list (ne_app a b). Proof. ir. induction a. tv. simpl. rww IHa. Qed. Fixpoint ne_map (A B: Type)(f:A-> B)(l:nelist A) : nelist B := match l with | singl a => singl (f a) | necons a t => necons (f a) (ne_map f t) end. Lemma ne_map_pr1: forall (A B: Type)(f:A-> B)(l:nelist A), nelist_to_list (ne_map f l) = map f (nelist_to_list l). Proof. ir. induction l. tv. simpl. rww IHl. Qed. Lemma ne_map_pr2: forall (A B: Type)(f:A-> B)(l:list A) (e:A), list_to_nelist (map f l) (f e) = ne_map f (list_to_nelist l e). Proof. ir. induction l. tv. induction l. tv. simpl. simpl in IHl. rww IHl. Qed. Fixpoint ne_compose(A:Type)(p: A->A->A)(l:nelist A):A := match l with | singl a => a | necons a b => p a (ne_compose p b) end. Fixpoint n_compose(A:Type)(p: A->A->A)(e:A)(l:list A):A := match l with | nil => e | a :: nil => a | a :: b => p a (n_compose p e b) end. Lemma ne_compose_pr1: forall A p (e:A) (l:nelist A), n_compose p e (nelist_to_list l) = ne_compose p l. Proof. ir. induction l. tv. simpl. wrr IHl. cp (nonempty_nelist l). set (w:= nelist_to_list l) in *. induction w. elim H. tv. tv. Qed. Lemma ne_compose_pr2: forall A p (e:A) (l:list A), ne_compose p (list_to_nelist l e) = n_compose p e l. Proof. ir. induction l. tv. induction l. tv. simpl. simpl in IHl. rww IHl. Qed. Inductive ne_list_prop (A:Type) (q: A->Prop) : nelist A -> Prop := | nelist_prop_singl: forall (a:A), q a -> ne_list_prop q (singl a) | nelist_prop_cons: forall (a:A)(l:nelist A), q a -> ne_list_prop q l -> ne_list_prop q (necons a l). Fixpoint ne_contraction (A B:Type) (L: nelist A) (f: A-> B->B) (v: A->B):B := match L with | singl a => v a | necons a b => f a (ne_contraction b f v) end. Definition nelist_subset L E := ne_list_prop (fun x => inc x E) L. Definition nelist_range l := ne_contraction l (fun a b => tack_on b a) singleton. Lemma nelist_prop_pr: forall (A:Type) (L: nelist A) (q: A->Prop), ne_list_prop q L= list_prop q (nelist_to_list L). Proof. ir. app iff_eq. ir. induction L. inversion H. simpl. right. am. left. inversion H. simpl. right. am. app IHL. ir. induction L. simpl in H. inversion H. left. am. simpl in H. inversion H. right. am. app IHL. Qed. Lemma ne_contraction_pr: forall (A B:Type) (L: nelist A) (f: A->B->B) v, ne_contraction L f (fun a=> f a v) = contraction (nelist_to_list L) f v. Proof. ir. induction L. tv. simpl. rww IHL. Qed. Lemma nelist_range_pr0: forall L, nelist_range L = list_range (nelist_to_list L). Proof. ir. uf list_range. wr ne_contraction_pr. uf nelist_range. assert (singleton =fun a : Set => tack_on emptyset a). app arrow_extensionality. ir. set_extens. rw (singleton_eq H). fprops. rwi tack_on_inc H. nin H. elim (emptyset_pr H). rw H. fprops. rww H. Qed. Lemma nelist_range_pr: forall L, nelist_subset L (nelist_range L). Proof. ir. red. rw nelist_prop_pr. rw nelist_range_pr0. app list_range_pr. Qed. Lemma nelist_range_pr1: forall L E, nelist_subset L E -> sub (nelist_range L) E. Proof. ir. rw nelist_range_pr0. app list_range_pr1. uf list_subset. wrr nelist_prop_pr. Qed. Lemma map_prop_trans: forall (A B:Type) (f:A->B) (p:A-> Prop) (q:B->Prop), (forall a:A, p a -> q (f a)) -> (forall L:list A, list_prop p L -> list_prop q (map f L)). Proof. ir. induction L. simpl. left. simpl. inversion H0. right. app H. app IHL. Qed. Lemma list_map_inj: forall (A B:Type) (f: A->B) (L L': list A), (forall a b :A, f(a) = f(b) -> a = b) -> (map f L = map f L') -> L =L'. Proof. intros A B f L L' H. generalize L'. induction L. ir. induction L'0. tv. simpl in H0. elim (nil_cons H0). ir. induction L'0. simpl in H0. symmetry in H0. elim (nil_cons H0). simpl in H0. injection H0. ir. rw (IHL _ H1). rww (H _ _ H2). Qed. Lemma nemap_prop_trans: forall (A B:Type) (f:A->B) (p:A-> Prop) (q:B->Prop), (forall a:A, p a -> q (f a)) -> (forall L:nelist A, ne_list_prop p L -> ne_list_prop q (ne_map f L)). Proof. ir. induction L. simpl. left. inversion H0. app H. simpl. inversion H0. right. app H. app IHL. Qed. Lemma nelist_map_inj: forall (A B:Type) (f: A->B) (L L': nelist A), (forall a b :A, f(a) = f(b) -> a = b) -> (ne_map f L = ne_map f L') -> L =L'. Proof. intros A B f L L' H. generalize L'. induction L. ir. induction L'0. simpl in H0. injection H0. ir. rww (H _ _ H1). simpl in H0. discriminate H0. ir. induction L'0. simpl in H0. discriminate H0. simpl in H0. injection H0. ir. rw (IHL _ H1). rww (H _ _ H2). Qed. Lemma map_Ro_pr: forall (E:Set) (L: list E), sub (list_range (map (Ro (x:=E)) L)) E. Proof. ir. app list_range_pr1. red. assert (forall a:E, True -> inc (Ro a) E). ir. app R_inc. app (map_prop_trans _ (fun a:Set => inc a E) H). induction L. left. right. tv. am. Qed. Lemma nemap_Ro_pr: forall (E:Set) (L: nelist E), sub (nelist_range (ne_map (Ro (x:=E)) L)) E. Proof. ir. app nelist_range_pr1. red. assert (forall a:E, True -> inc (Ro a) E). ir. app R_inc. app (nemap_prop_trans _ (fun a => inc a E) H). induction L. left. tv. right. tv. am. Qed. Lemma map_Ro_inj: forall (E:Set) (L L': list E), (map (Ro (x:=E)) L = map (Ro (x:=E)) L') -> L =L'. Proof. ir. apply list_map_inj with (f:=(Ro (x:=E))). ir. app R_inj. am. Qed. Lemma nemap_Ro_inj: forall (E:Set) (L L': nelist E), (ne_map (Ro (x:=E)) L = ne_map (Ro (x:=E)) L') -> L =L'. Proof. ir. apply nelist_map_inj with (f:=(Ro (x:=E))). ir. app R_inj. am. Qed. Lemma nonempty_list_type: forall E, nonemptyT (list E). Proof. ir. pose (@nil E). app nonemptyT_intro. Qed. Lemma nonempty_nelist_type: forall E, nonemptyT E -> nonemptyT (nelist E). Proof. ir. induction H. pose (singl X). app nonemptyT_intro. Qed. Lemma nonempty_nelist_type2: forall (E:Set)(L:nelist Set), nelist_subset L E -> nonemptyT E. Proof. ir. induction L. red in H. inversion H. cp (Bo H1). app nonemptyT_intro. app IHL. red in H. inversion H. red. am. Qed. Definition list_Ro_inv (E: Set)(L:list Set) := chooseT (fun a : list E => (map (Ro (x:=E)) a = L)) (nonempty_list_type E). Definition nelist_Ro_inv (E: Set)(L:nelist Set)(hyp:nonemptyT E) := chooseT (fun a : nelist E => (ne_map (Ro (x:=E)) a = L)) (nonempty_nelist_type hyp). Lemma list_Ro_inv_pr: forall (E:Set)(L:list Set), list_subset L E -> map (Ro (x:=E)) (list_Ro_inv E L) = L. Proof. ir. uf list_Ro_inv. app chooseT_pr. induction L. exists (@nil E). simpl. tv. ufi list_subset H. inversion H. nin (IHL H3). exists ((Bo H2)::x). simpl. rw H4. rww (B_eq H2). Qed. Lemma list_Ro_inv_pr0: forall (E:Set), list_Ro_inv E (@nil Set) = @nil E. Proof. ir. set (n:= (@nil Set)). assert (list_subset n E). uf n. left. cp (list_Ro_inv_pr H). app map_Ro_inj. Qed. Lemma list_Ro_inv_pr1: forall (E:Set)(L:list Set)(a:Set) (H: inc a E), list_subset L E -> list_Ro_inv E (a::L) = (Bo H) :: (list_Ro_inv E L). Proof. ir. app map_Ro_inj. rw list_Ro_inv_pr. simpl. rww list_Ro_inv_pr. rww (B_eq H). uf list_subset. right; am. Qed. Lemma nelist_Ro_inv_pr0: forall (E:Set)(L:nelist Set)(hyp:nonemptyT E), nelist_subset L E -> ne_map (Ro (x:=E)) (nelist_Ro_inv L hyp) = L. Proof. ir. uf nelist_Ro_inv. app chooseT_pr. induction L. red in H. inversion H. exists (singl (Bo H1)). simpl. rww (B_eq H1). red in H. inversion H. assert (nelist_subset L E). am. nin (IHL H4). exists (necons (Bo H2) x). simpl. rw H5. rww (B_eq H2). Qed. Lemma nelist_Ro_inv_pr1: forall (E:Set)(L:nelist Set) (hyp1:nonemptyT E)(hyp2:nonemptyT E), nelist_subset L E -> (nelist_Ro_inv L hyp1) = (nelist_Ro_inv L hyp2). Proof. ir. app nemap_Ro_inj. transitivity L. app (nelist_Ro_inv_pr0 hyp1 H). sy. app (nelist_Ro_inv_pr0 hyp2 H). Qed. Lemma list_Ro_inv_pr2: forall (E:Set) a (H: inc a E), nelist_Ro_inv (singl a) (inc_nonempty H) = singl (Bo H). Proof. ir. app nemap_Ro_inj. assert (nelist_subset (singl a) E). red. left. am. rw (nelist_Ro_inv_pr0 (inc_nonempty H) H0). simpl. rww B_eq. Qed. Lemma list_Ro_inv_pr3: forall (E:Set)(L:nelist Set)(a:Set) (H: inc a E), nelist_subset L E -> nelist_Ro_inv (necons a L) (inc_nonempty H) = necons (Bo H) (nelist_Ro_inv L (inc_nonempty H) ). Proof. ir. app nemap_Ro_inj. assert (nelist_subset (necons a L) E). red. simpl. red in H0. right; am. rw (nelist_Ro_inv_pr0 (inc_nonempty H) H1). simpl. rw (nelist_Ro_inv_pr0 (inc_nonempty H) H0). rww B_eq. Qed. Definition tofd_to_listB r f := fct_to_listB (tofd_to_iid r f). Fixpoint ne_flatten (x:Type)(l:nelist (nelist x)):nelist x := match l with | singl a => a | necons a b => ne_app a (ne_flatten b) end. Fixpoint flatten (x:Type)(l:list (list x)):list x := match l with | nil => nil | cons a b => app a (flatten b) end. End Blist. Export Blist. Module Basic. Hint Resolve group_is_monoid cgroup_is_group ring_is_cgroup sfield_is_ring lmodule_is_cgroup rmodule_is_cgroup lrmodule_is_cgroup : mp. Hint Resolve lmodule_aux_is_ring rmodule_aux_is_ring llrmodule_aux_is_ring rlrmodule_aux_is_ring lrmodule_is_lmodule lrmodule_is_rmodule: mp. Ltac mp:= auto with mp. Lemma mzero_U: forall g, monoid_axioms g -> inc (zero g) (Ul g). Proof. ir. destruct H as [H _]. am. Qed. Lemma gzero_U: forall g, group_axioms g -> inc (zero g) (Ul g). Proof. ir. ap mzero_U. mp. Qed. Lemma cgzero_U: forall g, cgroup_axioms g -> inc (zero g) (Ul g). Proof. ir. ap gzero_U. mp. Qed. Lemma rzero_U: forall g, ring_axioms g -> inc (zero g) (Ul g). Proof. ir. app cgzero_U. mp. Qed. Lemma fzero_U: forall g, sfield_axioms g -> inc (zero g) (Ul g). Proof. ir. app rzero_U. mp. Qed. Lemma lmzero_U: forall g, lmodule_axioms g -> inc (zero g) (Ul g). Proof. ir. ap cgzero_U. mp. Qed. Lemma rmzero_U: forall g, rmodule_axioms g -> inc (zero g) (Ul g). Proof. ir. ap cgzero_U. mp. Qed. Lemma lrmzero_U: forall g, lrmodule_axioms g -> inc (zero g) (Ul g). Proof. ir. ap cgzero_U. mp. Qed. Lemma rone_U: forall g, ring_axioms g -> inc (one g) (Ul g). Proof. ir. destruct H as [_ Rp]. destruct Rp as [_ [o _]]. app o. Qed. Lemma fone_U: forall g, sfield_axioms g -> inc (one g) (Ul g). Proof. ir. ap rone_U. mp. Qed. Lemma mplus_internal: forall g x y, monoid_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. destruct H as [_ [H _]]. app H. Qed. Lemma gplus_internal: forall g x y, group_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app mplus_internal. mp. Qed. Lemma cgplus_internal: forall g x y, cgroup_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app gplus_internal. mp. Qed. Lemma rplus_internal: forall g x y, ring_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app cgplus_internal. mp. Qed. Lemma fplus_internal: forall g x y, sfield_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app rplus_internal. mp. Qed. Lemma lmplus_internal: forall g x y, lmodule_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app cgplus_internal. mp. Qed. Lemma rmplus_internal: forall g x y, rmodule_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app cgplus_internal. mp. Qed. Lemma lrmplus_internal: forall g x y, lrmodule_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dplus g x y) (Ul g). Proof. ir. app cgplus_internal. mp. Qed. Lemma gneg_internal: forall g x, group_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. destruct H as [_ [H _]]. app H. Qed. Lemma cgneg_internal: forall g x, cgroup_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app gneg_internal. mp. Qed. Lemma rneg_internal: forall g x, ring_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app cgneg_internal. mp. Qed. Lemma fneg_internal: forall g x , sfield_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app rneg_internal. mp. Qed. Lemma lmneg_internal: forall g x, lmodule_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app cgneg_internal. mp. Qed. Lemma rmneg_internal: forall g x, rmodule_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app cgneg_internal. mp. Qed. Lemma lrmneg_internal: forall g x, lrmodule_axioms g-> inc x (Ul g) -> inc (neg g x) (Ul g). Proof. ir. app cgneg_internal. mp. Qed. Lemma rmult_internal: forall g x y, ring_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dmult g x y) (Ul g). Proof. ir. destruct H as [_ [H _]]. app H. Qed. Lemma fmult_internal: forall g x y, sfield_axioms g-> inc x (Ul g) -> inc y (Ul g) -> inc (dmult g x y) (Ul g). Proof. ir. app rmult_internal. mp. Qed. Lemma lmmult_internal: forall g x y, lmodule_axioms g-> inc x (Ul (lauxiliary g)) -> inc y (Ul g) -> inc (lmult g x y) (Ul g). Proof. ir. destruct H as [_ [_ H]]. destruct H as [_ [_ [_ [H _]]]]. app H. Qed. Lemma rmmult_internal: forall g x y, rmodule_axioms g-> inc x (Ul (rauxiliary g)) -> inc y (Ul g) -> inc (rmult g x y) (Ul g). Proof. ir. destruct H as [_ [_ H]]. destruct H as [_ [_ [_ [H _]]]]. app H. Qed. Lemma llrmmult_internal: forall g x y, lrmodule_axioms g-> inc x (Ul (lauxiliary g)) -> inc y (Ul g) -> inc (lmult g x y) (Ul g). Proof. ir. destruct H as [_ [_ H]]. red in H. ee. app H8. Qed. Lemma rlrmmult_internal: forall g x y, lrmodule_axioms g-> inc x (Ul (rauxiliary g)) -> inc y (Ul g) -> inc (rmult g x y) (Ul g). Proof. ir. destruct H as [_ [_ H]]. red in H. ee. app H10. Qed. Lemma mplus_assoc: forall g x y z, monoid_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. destruct H as [_ [_ [a _]]]. app a. Qed. Lemma gplus_assoc: forall g x y z, group_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app mplus_assoc. mp. Qed. Lemma cgplus_assoc: forall g x y z, cgroup_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app gplus_assoc. mp. Qed. Lemma rplus_assoc: forall g x y z, ring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app cgplus_assoc. mp. Qed. Lemma fplus_assoc: forall g x y z, sfield_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app rplus_assoc. mp. Qed. Lemma lmplus_assoc: forall g x y z, lmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app mplus_assoc. mp. Qed. Lemma rmplus_assoc: forall g x y z, rmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app mplus_assoc. mp. Qed. Lemma lrplus_assoc: forall g x y z, lrmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dplus g (dplus g x y) z = dplus g x (dplus g y z). Proof. ir. app mplus_assoc. mp. Qed. Lemma cgplus_comm: forall g x y, cgroup_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. intros. destruct H as [_ G]. app G. Qed. Lemma rplus_comm: forall g x y, ring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. ir. app cgplus_comm. mp. Qed. Lemma fplus_comm: forall g x y, sfield_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. ir. app rplus_comm. mp. Qed. Lemma lmplus_comm: forall g x y, lmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. ir. app cgplus_comm. mp. Qed. Lemma rmplus_comm: forall g x y, rmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. ir. app cgplus_comm. mp. Qed. Lemma lrmplus_comm: forall g x y, lrmodule_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dplus g x y) = dplus g y x. Proof. ir. app cgplus_comm. mp. Qed. Lemma cfmult_comm: forall g x y, field_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dmult g x y) = dmult g y x. Proof. ir. destruct H as [_ H]. app H. Qed. Lemma crmult_comm: forall g x y, cring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> (dmult g x y) = dmult g y x. Proof. ir. destruct H as [_ H]. app H. Qed. Lemma rmult_assoc: forall g x y z, ring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dmult g (dmult g x y) z = dmult g x (dmult g y z). Proof. ir. destruct H as [_ [_ [_ [a _]]]]. app a. Qed. Lemma fmult_assoc: forall g x y z, sfield_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g)-> dmult g (dmult g x y) z = dmult g x (dmult g y z). Proof. ir. app rmult_assoc. mp. Qed. Lemma lmmult_assoc: forall g x y z, lmodule_axioms g ->inc x (Ul (lauxiliary g)) -> inc y (Ul (lauxiliary g)) -> inc z (Ul g)-> lmult g x (lmult g y z) = lmult g (dmult (lauxiliary g) x y) z. Proof. ir. destruct H as [_ [_ H]]. destruct H as [_ [_ [a _]]]. app a. Qed. Lemma rmmult_assoc: forall g x y z, rmodule_axioms g ->inc x (Ul (rauxiliary g)) -> inc y (Ul (rauxiliary g)) -> inc z (Ul g)-> rmult g x (rmult g y z) = rmult g (dmult (rauxiliary g) y x) z. Proof. ir. destruct H as [_ [_ H]]. destruct H as [_ [_ [a _]]]. app a. Qed. Lemma llrmmult_assoc: forall g x y z, lrmodule_axioms g ->inc x (Ul (lauxiliary g)) -> inc y (Ul (lauxiliary g)) -> inc z (Ul g)-> lmult g x (lmult g y z) = lmult g (dmult (lauxiliary g) x y) z. Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H7. Qed. Lemma rlrmmult_assoc: forall g x y z, lrmodule_axioms g ->inc x (Ul (rauxiliary g)) -> inc y (Ul (rauxiliary g)) -> inc z (Ul g)-> rmult g x (rmult g y z) = rmult g (dmult (rauxiliary g) y x) z. Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H8. Qed. Lemma rdistributive_left: forall g x y z, ring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g) -> dmult g x (dplus g y z) = dplus g (dmult g x y) (dmult g x z). Proof. ir. destruct H as [_ [_ [_ [_ [_ [_ [H _]]]]]]]. app H. Qed. Lemma rdistributive_right: forall g x y z, ring_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g) -> dmult g (dplus g y z) x = dplus g (dmult g y x) (dmult g z x). Proof. ir. destruct H as [_ [_ [_ [_ [_ [_ [_ H]]]]]]]. app H. Qed. Lemma fdistributive_left: forall g x y z, sfield_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g) -> dmult g x (dplus g y z) = dplus g (dmult g x y) (dmult g x z). Proof. ir. app rdistributive_left; mp. Qed. Lemma fdistributive_right: forall g x y z, sfield_axioms g ->inc x (Ul g) -> inc y (Ul g) -> inc z (Ul g) -> dmult g (dplus g y z) x = dplus g (dmult g y x) (dmult g z x). Proof. ir. app rdistributive_right; mp. Qed. Lemma lmdistributive_left: forall g x y z, lmodule_axioms g ->inc x (Ul (lauxiliary g)) -> inc y (Ul g) -> inc z (Ul g) -> lmult g x (dplus g y z) = dplus g (lmult g x y) (lmult g x z). Proof. ir. destruct H as [_ H]. destruct H as [_ [H _]]. app H. Qed. Lemma lmdistributive_right: forall g x y z, lmodule_axioms g ->inc x (Ul g) -> inc y (Ul (lauxiliary g)) -> inc z (Ul (lauxiliary g)) -> lmult g (dplus (lauxiliary g) y z) x = dplus g (lmult g y x) (lmult g z x). Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [H _]]]. app H. Qed. Lemma rmdistributive_left: forall g x y z, rmodule_axioms g ->inc x (Ul (rauxiliary g)) -> inc y (Ul g) -> inc z (Ul g) -> rmult g x (dplus g y z) = dplus g (rmult g x y) (rmult g x z). Proof. ir. destruct H as [_ H]. destruct H as [_ [H _]]. app H. Qed. Lemma rmdistributive_right: forall g x y z, rmodule_axioms g ->inc x (Ul g) -> inc y (Ul (rauxiliary g)) -> inc z (Ul (rauxiliary g)) -> rmult g (dplus (rauxiliary g) y z) x = dplus g (rmult g y x) (rmult g z x). Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [H _]]]. app H. Qed. Lemma llrmdistributive_left: forall g x y z, lrmodule_axioms g ->inc x (Ul (lauxiliary g)) -> inc y (Ul g) -> inc z (Ul g) -> lmult g x (dplus g y z) = dplus g (lmult g x y) (lmult g x z). Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H3. Qed. Lemma llrmdistributive_right: forall g x y z, lrmodule_axioms g ->inc x (Ul g) -> inc y (Ul (lauxiliary g)) -> inc z (Ul (lauxiliary g)) -> lmult g (dplus (lauxiliary g) y z) x = dplus g (lmult g y x) (lmult g z x). Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H4. Qed. Lemma rlrmdistributive_left: forall g x y z, lrmodule_axioms g ->inc x (Ul (rauxiliary g)) -> inc y (Ul g) -> inc z (Ul g) -> rmult g x (dplus g y z) = dplus g (rmult g x y) (rmult g x z). Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H5. Qed. Lemma rlrmdistributive_right: forall g x y z, lrmodule_axioms g ->inc x (Ul g) -> inc y (Ul (rauxiliary g)) -> inc z (Ul (rauxiliary g)) -> rmult g (dplus (rauxiliary g) y z) x = dplus g (rmult g y x) (rmult g z x). Proof. ir. destruct H as [_ [_ H]]. red in H; ee. app H6. Qed. Lemma mzero_unit_right: forall g x, monoid_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. intros. destruct H as [_ [_ [_ [H _]]]]. app H. Qed. Lemma mzero_unit_left: forall g x, monoid_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. intros. destruct H as [_ [_ [_ [_ H]]]]. app H. Qed. Lemma gzero_unit_right: forall g x, group_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app mzero_unit_right. mp. Qed. Lemma gzero_unit_left: forall g x, group_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app mzero_unit_left. mp. Qed. Lemma cgzero_unit_right: forall g x, cgroup_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app gzero_unit_right. mp. Qed. Lemma cgzero_unit_left: forall g x, cgroup_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app gzero_unit_left. mp. Qed. Lemma rzero_unit_right: forall g x, ring_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app cgzero_unit_right. mp. Qed. Lemma rzero_unit_left: forall g x, ring_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app cgzero_unit_left. mp. Qed. Lemma fzero_unit_right: forall g x, sfield_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app rzero_unit_right. mp. Qed. Lemma fzero_unit_left: forall g x, sfield_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app rzero_unit_left. mp. Qed. Lemma lmzero_unit_right: forall g x, lmodule_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app cgzero_unit_right. mp. Qed. Lemma lmzero_unit_left: forall g x, lmodule_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app cgzero_unit_left. mp. Qed. Lemma rmzero_unit_right: forall g x, rmodule_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app cgzero_unit_right. mp. Qed. Lemma rmzero_unit_left: forall g x, rmodule_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app cgzero_unit_left. mp. Qed. Lemma lrzero_unit_right: forall g x, lrmodule_axioms g -> inc x (Ul g) -> dplus g x (zero g) = x. Proof. ir. app cgzero_unit_right. mp. Qed. Lemma lrzero_unit_left: forall g x, lrmodule_axioms g -> inc x (Ul g) -> dplus g (zero g) x = x. Proof. ir. app cgzero_unit_left. mp. Qed. Lemma rone_unit_right: forall g x, ring_axioms g -> inc x (Ul g) -> dmult g x (one g) = x. Proof. intros. destruct H as [_ [_ [_ [_ [H _]]]]]. app H. Qed. Lemma rone_unit_left: forall g x, ring_axioms g -> inc x (Ul g) -> dmult g (one g) x = x. Proof. intros. destruct H as [_ [_ [_ [_ [_ [H _]]]]]]. app H. Qed. Lemma fone_unit_right: forall g x, sfield_axioms g -> inc x (Ul g) -> dmult g x (one g) = x. Proof. ir. app rone_unit_right. mp. Qed. Lemma fone_unit_left: forall g x, sfield_axioms g -> inc x (Ul g) -> dmult g (one g) x = x. Proof. ir. app rone_unit_left. mp. Qed. Lemma lmone_unit_left: forall g x, lmodule_axioms g -> inc x (Ul g) -> lmult g (one (lauxiliary g)) x = x. Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [_ [_ [_ H]]]]]. app H. Qed. Lemma rmone_unit_left: forall g x, rmodule_axioms g -> inc x (Ul g) -> rmult g (one (rauxiliary g)) x = x. Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [_ [_ [_ H]]]]]. app H. Qed. Lemma llrmone_unit_left: forall g x, lrmodule_axioms g -> inc x (Ul g) -> lmult g (one (lauxiliary g)) x = x. Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [_ [_ [_ H]]]]]. destruct H as [_ [_ [_ [_ [H _]]]]]. app H. Qed. Lemma rlrmone_unit_left: forall g x, lrmodule_axioms g -> inc x (Ul g) -> rmult g (one (rauxiliary g)) x = x. Proof. ir. destruct H as [_ H]. destruct H as [_ [_ [_ [_ [_ H]]]]]. destruct H as [_ [_ [_ [_ [_ [_ H]]]]]]. app H. Qed. Lemma gopp_right: forall g x, group_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. intros. destruct H as [_ [_ [H _]]]. app H. Qed. Lemma gopp_left: forall g x, group_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. intros. destruct H as [_ [_ [_ H]]]. app H. Qed. Lemma cgopp_right: forall g x, cgroup_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app gopp_right. mp. Qed. Lemma cgopp_left: forall g x, cgroup_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app gopp_left. mp. Qed. Lemma ropp_right: forall g x, ring_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app cgopp_right. mp. Qed. Lemma ropp_left: forall g x, ring_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app cgopp_left. mp. Qed. Lemma fopp_right: forall g x, sfield_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app ropp_right. mp. Qed. Lemma fopp_left: forall g x, sfield_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app ropp_left. mp. Qed. Lemma lmopp_right: forall g x, lmodule_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app cgopp_right. mp. Qed. Lemma lmopp_left: forall g x, lmodule_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app cgopp_left. mp. Qed. Lemma rmopp_right: forall g x, rmodule_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app cgopp_right. mp. Qed. Lemma rmopp_left: forall g x, rmodule_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app cgopp_left. mp. Qed. Lemma lrmopp_right: forall g x, lrmodule_axioms g -> inc x (Ul g) -> dplus g x (neg g x) = zero g. Proof. ir. app cgopp_right. mp. Qed. Lemma lrmopp_left: forall g x, lrmodule_axioms g -> inc x (Ul g) -> dplus g (neg g x) x = zero g. Proof. ir. app cgopp_left. mp. Qed. Lemma finv_right: forall g x, sfield_axioms g -> inc x (Ul g) -> x <> (zero g) -> dmult g x (inv g x) = one g. Proof. intros. destruct H as [_ [_ [H _]]]. app H. Qed. Lemma finv_left: forall g x, sfield_axioms g -> inc x (Ul g) -> x <> (zero g) -> dmult g (inv g x) x = one g. Proof. intros. destruct H as [_ [H _]]. app H. Qed. Lemma ginv_internal: forall g x, sfield_axioms g -> inc x (Ul g) -> inc (inv g x) (Ul g). Proof. intros. destruct H as [_ [_ [_ [H _]]]]. app H. Qed. Hint Resolve mzero_U gzero_U cgzero_U rzero_U fzero_U lmzero_U rmzero_U lrmzero_U :mp. Hint Resolve rone_U fone_U : mp. Hint Resolve mplus_internal gplus_internal cgplus_internal rplus_internal fplus_internal lmplus_internal rmplus_internal lrmplus_internal : mp. Hint Resolve gneg_internal cgneg_internal rneg_internal fneg_internal lmneg_internal rmneg_internal lrmneg_internal : mp. Hint Resolve rmult_internal fmult_internal lmmult_internal rmmult_internal llrmmult_internal rlrmmult_internal ginv_internal : mp. End Basic. Export Basic. Module Basic1. Lemma gneg_a_a_b_is_b :forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g)-> dplus g (neg g a) (dplus g a b) = b. Proof. ir. wrr gplus_assoc. rww gopp_left. rww gzero_unit_left. mp. Qed. Lemma gb_a_neg_a_is_b :forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g)-> dplus g (dplus g b a) (neg g a) = b. Proof. intros. rww gplus_assoc. rww gopp_right. rww gzero_unit_right. mp. Qed. Lemma ga_neg_a_b_is_b :forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g)-> dplus g a (dplus g (neg g a) b) = b. Proof. ir. wrr gplus_assoc. rww gopp_right. rww gzero_unit_left. mp. Qed. Lemma gb_bneg_a_a_is_b :forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g)-> dplus g (dplus g b (neg g a)) a = b. Proof. intros. rww gplus_assoc. rww gopp_left. rww gzero_unit_right. mp. Qed. Lemma gleft_simpl: forall g a x y, group_axioms g -> inc a (Ul g)-> inc x (Ul g)-> inc y (Ul g) -> dplus g a x = dplus g a y -> x = y. Proof. intros. rewrite <- gneg_a_a_b_is_b with g a x; try am. rw H3. rewrite gneg_a_a_b_is_b with g a y; try am. tv. Qed. Lemma gright_simpl: forall g a x y, group_axioms g -> inc a (Ul g)-> inc x (Ul g)-> inc y (Ul g) -> dplus g x a = dplus g y a -> x = y. Proof. intros. rewrite <- gb_a_neg_a_is_b with g a x; try am. rw H3. rewrite gb_a_neg_a_is_b with g a y; try am. tv. Qed. Lemma gzero_unique_right: forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g) -> dplus g a b = a -> b = zero g. Proof. ir. apply gleft_simpl with g a. am. mp. am. mp. rww gzero_unit_right. Qed. Lemma gzero_unique_left: forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g) -> dplus g b a = a -> b = zero g. Proof. ir. apply gright_simpl with g a. am. mp. am. mp. rww gzero_unit_left. Qed. Lemma rzero_left_abs: forall g a, ring_axioms g -> inc a (Ul g) -> dmult g (zero g) a = (zero g). Proof. ir. set (x:= dmult g (zero g) a). assert (inc x (Ul g)). unfold x. mp. assert (inc (zero g) (Ul g)). mp. apply gzero_unique_right with x; try am. mp. unfold x. wrr rdistributive_right. rww rzero_unit_right. Qed. Lemma rzero_right_abs: forall g a, ring_axioms g -> inc a (Ul g) -> dmult g a (zero g) = (zero g). Proof. ir. set (x:= dmult g a (zero g)). assert (inc x (Ul g)). unfold x. mp. assert (inc (zero g) (Ul g)). mp. apply gzero_unique_right with x; try am. mp. unfold x. wrr rdistributive_left. rww rzero_unit_right. Qed. Lemma fone_not_zero: forall g, sfield_axioms g -> (one g) <> (zero g). Proof. ir. assert (Ha:=H). red in H. red in H. ee. nin H3. ee. red; ir. red in H4. app H4. pose (fone_unit_right Ha H3). rwi H5 e. rwi rzero_right_abs e. sy. am. mp. am. Qed. Lemma lmzero_left_abs: forall g a, lmodule_axioms g -> inc a (Ul g) -> lmult g (zero (lauxiliary g)) a = (zero g). Proof. ir. set (D:= lauxiliary g). assert (ring_axioms D). unfold D; mp. assert (inc (zero D) (Ul D)). mp. set (x:= lmult g (zero D) a). assert (inc x (Ul g)). unfold x. mp. apply gzero_unique_right with x; try am. mp. unfold x. wrr lmdistributive_right. fold D. rww rzero_unit_right. Qed. Lemma rmzero_left_abs: forall g a, rmodule_axioms g -> inc a (Ul g) -> rmult g (zero (rauxiliary g)) a = (zero g). Proof. ir. set (D:= rauxiliary g). assert (ring_axioms D). unfold D; mp. assert (inc (zero D) (Ul D)). mp. set (x:= rmult g (zero D) a). assert (inc x (Ul g)). unfold x. mp. apply gzero_unique_right with x; try am. mp. unfold x. wrr rmdistributive_right. fold D. rww rzero_unit_right. Qed. Lemma llrmzero_left_abs: forall g a, lrmodule_axioms g -> inc a (Ul g) -> lmult g (zero (lauxiliary g)) a = (zero g). Proof. ir. app lmzero_left_abs. mp. Qed. Lemma rlrmzero_left_abs: forall g a, lrmodule_axioms g -> inc a (Ul g) -> rmult g (zero (rauxiliary g)) a = (zero g). Proof. ir. app rmzero_left_abs. mp. Qed. Lemma gright_inv_unique: forall g a x, group_axioms g -> inc a (Ul g)-> inc x (Ul g) -> dplus g x a = zero g -> x = neg g a. Proof. intros. rewrite <- gopp_left with (x:=a) in H2; try am. apply gright_simpl with g a; try am. mp. Qed. Lemma gleft_inv_unique: forall g a x, group_axioms g -> inc a (Ul g)-> inc x (Ul g) -> dplus g x a = zero g -> a = neg g x. Proof. intros. rewrite <- gopp_right with (x:=x) in H2; try am. apply gleft_simpl with g x; try am. mp. Qed. Lemma gunit_self_inverse: forall g, group_axioms g -> neg g (zero g) = zero g. Proof. intros. set (x:= zero g). assert (inc (zero g) (Ul g)). mp. assert (dplus g x x=x). pose (H2:=gzero_unit_left H H0). unfold x. am. symmetry. app gleft_inv_unique. Qed. Lemma gdouble_inverse: forall g a, group_axioms g -> inc a (Ul g) -> neg g (neg g a) = a. Proof. intros. assert (dplus g (neg g a) a = (zero g)). app gopp_left. symmetry. app gleft_inv_unique. mp. Qed. Lemma prod_inverse: forall g a b, group_axioms g -> inc a (Ul g)-> inc b (Ul g) -> neg g (dplus g a b) = dplus g (neg g b) (neg g a). Proof. intros. symmetry. assert (inc (neg g a) (Ul g)). mp. assert (inc (neg g b) (Ul g)). mp. assert (inc (dplus g (neg g b) (neg g a)) (Ul g)). mp. app gleft_inv_unique. mp. rewrite gplus_assoc; try am. rww ga_neg_a_b_is_b. app gopp_right. Qed. Lemma finv_a_a_b_is_b :forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g)-> a <> (zero g) -> dmult g (inv g a) (dmult g a b) = b. Proof. ir. wrr fmult_assoc. rww finv_left. rww fone_unit_left. mp. Qed. Lemma fb_a_inv_a_is_b :forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g)-> a <> (zero g) -> dmult g (dmult g b a) (inv g a) = b. Proof. intros. rww fmult_assoc. rww finv_right. rww fone_unit_right. mp. Qed. Lemma fa_inv_a_b_is_b :forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g)-> a <> (zero g) -> dmult g a (dmult g (inv g a) b) = b. Proof. ir. wrr fmult_assoc. rww finv_right. rww fone_unit_left. mp. Qed. Lemma fb_binv_a_a_is_b :forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g)-> a <> (zero g) -> dmult g (dmult g b (inv g a)) a = b. Proof. intros. rww fmult_assoc. rww finv_left. rww fone_unit_right. mp. Qed. Lemma fleft_simpl: forall g a x y, sfield_axioms g -> inc a (Ul g)-> inc x (Ul g)-> inc y (Ul g)-> a <> (zero g) -> dmult g a x = dmult g a y -> x = y. Proof. intros. rewrite <- finv_a_a_b_is_b with g a x; try am. rw H4. rewrite finv_a_a_b_is_b with g a y; try am. tv. Qed. Lemma funit_self_inverse: forall g, sfield_axioms g -> inv g (one g) = one g. Proof. intros. set (x:= one g). assert (inc (one g) (Ul g)). mp. assert (x = dmult g x x). pose (H2:=fone_unit_left H H0). sy. unfold x. am. set (y := (inv g x)). assert (dmult g y x = dmult g y (dmult g x x)). wr H1. tv. wri fmult_assoc H2; try am. assert (dmult g y x = y). unfold x. app fone_unit_right. uf y. mp. assert (dmult g y x = x). unfold y;unfold x. app finv_left. app fone_not_zero. wr H3. am. unfold y. mp. Qed. Lemma fright_simpl: forall g a x y, sfield_axioms g -> inc a (Ul g)-> inc x (Ul g)-> inc y (Ul g)-> a <> (zero g) -> dmult g x a = dmult g y a -> x = y. Proof. intros. rewrite <- fb_a_inv_a_is_b with g a x; try am. rw H4. rewrite fb_a_inv_a_is_b with g a y; try am. tv. Qed. Lemma fright_inv_unique: forall g a x, sfield_axioms g -> inc a (Ul g)-> inc x (Ul g) -> dmult g x a = one g -> x = inv g a. Proof. intros. apply by_cases with (a= zero g). ir. assert (zero g = one g). rwi H3 H2. rwi rzero_right_abs H2. tv. mp. am. symmetry in H4. elim (fone_not_zero H H4). ir. rewrite <- finv_left with (x:=a) in H2; try am. apply fright_simpl with g a; try am. mp. Qed. Lemma fleft_inv_unique: forall g a x, sfield_axioms g -> inc a (Ul g)-> inc x (Ul g) -> dmult g x a = one g -> a = inv g x. Proof. ir. apply by_cases with (x= zero g). ir. assert (zero g = one g). rwi H3 H2. rwi rzero_left_abs H2. tv. mp. am. symmetry in H4. elim (fone_not_zero H H4). ir. rewrite <- finv_right with (x:=x) in H2; try am. apply fleft_simpl with g x; try am. mp. Qed. Lemma fdouble_inverse: forall g a, sfield_axioms g -> inc a (Ul g) -> a <> (zero g) -> inv g (inv g a) = a. Proof. intros. assert (dmult g (inv g a) a = (one g)). app finv_left. symmetry. app fleft_inv_unique. mp. Qed. Lemma sfield_integral_domain : forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g) -> (dmult g a b) = (zero g) -> (a= (zero g)) \/ (b= (zero g)). Proof. ir. apply by_cases with (a= zero g). ir. left. tv. ir. right. assert (ring_axioms g). mp. pose (rzero_right_abs H4 H0). symmetry in e. rwi e H2. apply fleft_simpl with g a; try am. mp. Qed. Lemma fprod_inverse: forall g a b, sfield_axioms g -> inc a (Ul g)-> inc b (Ul g) -> a <> (zero g)-> b <> (zero g) -> inv g (dmult g a b) = dmult g (inv g b) (inv g a). Proof. intros. symmetry. assert (inc (inv g a) (Ul g)). mp. assert (inc (inv g b) (Ul g)). mp. assert (inc (dmult g (inv g b) (inv g a)) (Ul g)). mp. app fleft_inv_unique. mp. rewrite fmult_assoc; try am. rww fa_inv_a_b_is_b. app finv_right. Qed. Definition lzero_divisor (g a:Set):= (inc a (Ul g)) & (exists b, (inc b (Ul g)) & b<> (zero g) & dmult g a b = zero g). Definition rzero_divisor (g a:Set):= (inc a (Ul g)) & (exists b, (inc b (Ul g)) & b<> (zero g) & dmult g a b = zero g). Definition lring_domain g:= forall a:Set, inc a (Ul g) -> a<> (zero g) -> ~ (lzero_divisor g a). Definition rring_domain g:= forall a:Set, inc a (Ul g) -> a<> (zero g) -> ~ (rzero_divisor g a). Definition ring_domain g := (ring_axioms g) & (lring_domain g) & (lring_domain g). Lemma sfield_integral_domain_bis: forall g, sfield_axioms g-> ring_domain g. Proof. ir. red. split. mp. split. red. ir. uf not. ir. red in H2. nin H2. nin H3. ee. pose (sfield_integral_domain H H0 H3 H5). nin o. apply (H1 H6). apply (H4 H6). red. ir. uf not. ir. red in H2. nin H2. nin H3. ee. pose (sfield_integral_domain H H0 H3 H5). nin o. apply (H1 H6). apply (H4 H6). Qed. Lemma rtimes_mone_is_neg_left: forall g x, ring_axioms g -> inc x (Ul g)-> dmult g (neg g (one g)) x = neg g x. Proof. ir. assert (inc (one g) (Ul g)). mp. apply gright_simpl with g x; try am. mp. mp. mp. rww ropp_left. set (u:=dmult g (neg g (one g)) x). assert (dmult g (one g) x =x). app rone_unit_left. wr H2. uf u. wrr rdistributive_right. rww ropp_left. app rzero_left_abs. mp. Qed. Lemma rtimes_mone_is_neg_right: forall g x, ring_axioms g -> inc x (Ul g)-> dmult g x (neg g (one g)) = neg g x. Proof. ir. assert (inc (one g) (Ul g)). mp. apply gright_simpl with g x; try am. mp. mp. mp. rww ropp_left. set (u:=dmult g x (neg g (one g))). assert (dmult g x (one g) =x). app rone_unit_right. wr H2. uf u. wrr rdistributive_left. rww ropp_left. app rzero_right_abs. mp. Qed. Lemma lmtimes_mone_is_neg: forall g x, lmodule_axioms g -> inc x (Ul g)-> lmult g (neg (lauxiliary g) (one (lauxiliary g))) x = neg g x. Proof. ir. set (D:= lauxiliary g). set (o:= (one D)). assert (ring_axioms D). red in H. ee. am. assert (inc (one D) (Ul D)). mp. apply gright_simpl with g x; try am. mp. mp. mp. rww lmopp_left. set (u:=lmult g (neg D o) x). assert (lmult g (one D) x =x). unfold D. app lmone_unit_left. wr H3. uf u. wrr lmdistributive_right. rww ropp_left. unfold D. app lmzero_left_abs. mp. Qed. Lemma rmtimes_mone_is_neg: forall g x, rmodule_axioms g -> inc x (Ul g)-> rmult g (neg (rauxiliary g) (one (rauxiliary g))) x = neg g x. Proof. ir. set (D:= rauxiliary g). set (o:= (one D)). assert (ring_axioms D). unfold D; mp. assert (inc (one D) (Ul D)). mp. apply gright_simpl with g x; try am. mp. mp. mp. rww rmopp_left. set (u:=rmult g (neg D o) x). assert (rmult g (one D) x =x). unfold D. app rmone_unit_left. wr H3. uf u. wrr rmdistributive_right. rww ropp_left. unfold D. app rmzero_left_abs. mp. Qed. End Basic1. Export Basic1. Module CommutativeGroup. Definition gconjugate (g x y:Set) := (dplus g x (dplus g y (neg g x))). Definition gconjugate' (g x y:Set) := (dplus g (dplus g x y) (neg g x)). Lemma conj_assoc: forall g x y, group_axioms g ->inc x (Ul g) -> inc y (Ul g) -> gconjugate g x y = gconjugate' g x y. Proof. intros. unfold gconjugate. unfold gconjugate'. rww gplus_assoc. mp. Qed. Lemma cg_conjugation_trivial: forall g x y, cgroup_axioms g ->inc x (Ul g) -> inc y (Ul g) -> gconjugate g x y = y. Proof. intros. unfold gconjugate. assert (group_axioms g). app cgroup_is_group. assert ((dplus g y (neg g x)) = (dplus g (neg g x) y)). app cgplus_comm. mp. rw H3. wrr gplus_assoc. rww gopp_right. app gzero_unit_left. mp. Qed. End CommutativeGroup. (* dans un anneau -1.x = -x dans un module idem *) (*EOD *)