Ssreflect Users Discussion List

[Ian Zimmerman <>]

On 2019-10-20 16:29, Assia Mahboubi wrote:

> Could you try to send your message again on the list, cc-ing us for
> once, so that we receive at least a copy of it?

Thanks for your help.  Ok, here's my next stupid question / stumbling
block on the way to doing math with ssreflect.

Below I enclose a file where I prove some trivial facts about arbitrary
groups.  Proving the last lemma, group_morph_respects_inv, after the
first two steps I expected the lemma group_inverse_unique_right to be
directly applicable; but it isn't because the shape of its conclusion is
(b ⁻ = a) and my present goal looks rather like (a = b ⁻).  In fact I'd
faced this situation many times in the previous lemmas, but I could work
around it each time with a clever rewrite; but not this last time.  So
my question is, is there a general work-around for this, saving many
lines of boilerplate?



  From mathcomp Require Import ssreflect ssrfun ssrbool.
  Require Import FunctionalExtensionality.
  Require Import ClassicalEpsilon.
  Require Import PropExtensionality.
  Set Implicit Arguments.
  Unset Strict Implicit.
  Unset Printing Implicit Defensive.
  Require Import Utf8.


  Delimit Scope G_scope with G.

  Class group_binop (A:Type) := group_op: A → A → A.

  Infix "*" := group_op: G_scope.

  Class group_invop (A: Type) := group_inv: A → A.

  Notation "x ⁻" := (group_inv x) (at level 5): G_scope.

  Open Scope G_scope.

  Class group (A: Type) (star: group_binop A) (I: A) (inv: group_invop A) := {
    star_assoc: associative star;
    unity_left_id: left_id I star;
    unity_right_id: right_id I star;
    inv_left_inverse: left_inverse I inv star;
    inv_right_inverse: right_inverse I inv star;
  }.

  Section Group_def.

  Variables (A: Type) (star: group_binop A) (I: A) (inv: group_invop A) (G: 
group star I inv).

  Lemma group_right_anni a b: a * (a ⁻ * b) = b.
  Proof.
    by rewrite star_assoc inv_right_inverse unity_left_id.
  Qed.

  Lemma group_left_anni a b: (a * b ⁻) * b = a.
  Proof.
    by rewrite -star_assoc inv_left_inverse unity_right_id.
  Qed.

  Lemma group_right_anni2 a b: a ⁻ * (a * b) = b.
  Proof.
    by rewrite star_assoc inv_left_inverse unity_left_id.
  Qed.

  Lemma group_left_anni2 a b: (a * b) * b ⁻ = a.
  Proof.
    by rewrite -star_assoc inv_right_inverse unity_right_id.
  Qed.

  Lemma group_inverse_unique_left a b: a * b = I → a ⁻ = b.
  Proof.
    have: a ⁻ * (a * b) = b by [apply: group_right_anni2] => A'AB ABI.
    by rewrite -[in RHS] A'AB ABI -[in LHS] /a⁻ unity_right_id.
  Qed.

  Lemma group_inverse_unique_right a b: a * b = I → b ⁻ = a.
  Proof.
    have: (a * b) * b ⁻ = a by [apply: group_left_anni2] => ABB' ABI.
    by rewrite -[in RHS] ABB' ABI unity_left_id.
  Qed.

  Lemma group_inverse_involutive a: (a ⁻)⁻ = a.
  Proof.
    have: a * a ⁻ = I by apply: inv_right_inverse a.
    by apply: group_inverse_unique_right.
  Qed.

  Proposition group_left_cancel a x y: a * x = a * y → x = y.
  Proof.
    move => AxAy; have: a ⁻ * (a * x) = a ⁻ * (a * y) by [rewrite AxAy] => 
{AxAy}.
    by rewrite 2! star_assoc inv_left_inverse 2! unity_left_id.
  Qed.

  Proposition group_right_cancel a x y: x * a = y * a → x = y.
  Proof.
    move => xAyA; have: (x * a) * a ⁻ = (y * a) * a ⁻ by [rewrite xAyA] => 
{xAyA}.
    by rewrite -2! star_assoc inv_right_inverse 2! unity_right_id.
  Qed.

  Proposition group_unity_unique_right a b: a * b = a → b = I.
  Proof.
     move => ABA; have: a ⁻ * (a * b) = a ⁻ * a by [rewrite ABA] => {ABA}.
     by rewrite star_assoc inv_left_inverse unity_left_id.
  Qed.

  Proposition group_unity_unique_left a b: a * b = b → a = I.
  Proof.
    move => ABB; have: (a * b) * b ⁻ = b * b ⁻ by [rewrite ABB] => {ABB}.
    by rewrite -star_assoc inv_right_inverse unity_right_id.
  Qed.

  Lemma group_unity_if_idem a: a * a = a → a = I.
  Proof.
    by apply: group_unity_unique_right.
  Qed.

  Proposition group_connected a b: ∃ x y, a * x = b ∧ y * b = a.
  Proof.
    exists (a ⁻ * b); exists (a * b ⁻).
    split; [apply: group_right_anni | apply: group_left_anni].
  Qed.

  End Group_def.

  Section Group_morph.

  Variables (A: Type) (star: group_binop A) (I: A) (inv: group_invop A) (G: 
group star I inv).

  Variables (B: Type) (star': group_binop B) (I': B) (inv': group_invop B) 
(G': group star' I' inv').

  Definition group_morphism (f: A → B) := {morph f: x y / x * y >-> x * y}.

  Proposition group_morph_respects_unity f: group_morphism f → f I = I'.
  Proof.
    have: f (I * I) = f I by [rewrite unity_left_id] => III MorphF.
    have: f I * f I = f I by [rewrite MorphF in III] => {III} {MorphF}.
    by apply: group_unity_if_idem.
  Qed.

  Proposition group_morph_respects_inv f a: group_morphism f → f a ⁻ = (f a) 
⁻.
  Proof.
    have: f (a ⁻ * a) = f I by [rewrite inv_left_inverse] => A'AI MorphF.
    have: f a ⁻ * f a = I' by [rewrite MorphF group_morph_respects_unity in 
A'AI] => fA'fAI {A'AI} {MorphF}.
    have: (f a)⁻ = f a⁻ by [apply: group_inverse_unique_right fA'fAI]. by [].
  Qed.

  End Group_morph.

  Close Scope G_scope.


-- 
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.