Ssreflect Users Discussion List

[Ian Zimmerman <>]

Hello kind Coq+ssreflect experts,

The last rewrite step in the last proof below fails, with the error
message 

Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
The LHS of assoc
    (_ _ (_ _ _))
does not match any subterm of the goal

Why is that?  Superficially and to a newbie's eye, it doesn't look so
different from the other (earlier) "rewrite assoc" steps, and those work.


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 (car: Type) (op: group_binop car) (I: car) (inv: group_invop car) 
:= {
  assoc: associative op;
  unity_left_id: left_id I op;
  unity_right_id: right_id I op;
  inv_left_inverse: left_inverse I inv op;
  inv_right_inverse: right_inverse I inv op;
}.

Section Group_def.

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

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

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

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

Lemma group_left_anni2 a b: (a * b) * b ⁻ = a.
Proof.
  by rewrite -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.

Lemma group_inverse_unique_left2 a b: a ⁻ * b = I → a = b.
Proof.
  move => A'BI; have: (a⁻)⁻ = b by [apply: group_inverse_unique_left] => 
{A'BI}.
  by rewrite group_inverse_involutive.
Qed.

Lemma group_inverse_unique_right2 a b: a * b ⁻ = I → a = b.
Proof.
  move => AB'I. have: (b⁻)⁻ = a by [apply: group_inverse_unique_right] => 
{AB'I}.
  by rewrite group_inverse_involutive.
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! 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! 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 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 -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 ⁻).
  by split; [apply: group_right_anni | apply: group_left_anni].
Qed.

Proposition group_translate_bijective_left a: bijective (λ x, a * x).
Proof.
  set f := λ x, a * x; set g := λ x, a ⁻ * x.
  have: ∀ x, g x = a ⁻ * x by [] => Gx.
  have: ∀ x, f x = a * x by [] => Fx.
  have: ∀ x, g (f x) = a ⁻ * (a * x) by [move => x; rewrite -Fx -Gx] => GFx.
  rewrite assoc in GFx.  (* This doesn't work! *)
Abort.

End Group_def.

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.