gyro_mul_left_inj

Stream: new members

[James Arthur]

I'm trying to create a mul_left_inj for a new group that I'm formalising and developing. Heres basically as far as I have got:

import tactic


noncomputable theory
open_locale classical
universe u

class has_gyrop        (α : Type u) := (gyrop : α → α → α)
class has_subgyrop     (α : Type u) := (subgyrop : α → α → α)
class has_neggyrop     (α : Type u) := (neggyrop : α → α)
class has_cogyrop      (α : Type u) := (cogyrop : α → α → α)
class has_subcogyrop      (α : Type u) := (subcogyrop : α → α → α)
class has_negcogyrop      (α : Type u) := (negcogyrop : α → α)

infix `⊙`:75 := has_gyrop.gyrop
infix `⊝`:75 := has_subgyrop.subgyrop
prefix `⊝`:65 := has_neggyrop.neggyrop
infix `⊞`:80 := has_cogyrop.cogyrop
infix `⊟`:80 := has_subcogyrop.subcogyrop -- what a long name
infix `⊟`:85 := has_negcogyrop.negcogyrop

/-?
A gyrogroup (G, ⊕) is gyrocommutative if its binary operation obeys the gyrocommutative law
(G6) a ⊕ b = gyr[a, b](b ⊕ a) for all a, b ∈ G.
-/

class gyrocomm_gyrogroup (C : Type) extends has_gyrop C, has_subgyrop C, has_neggyrop C, has_zero C :=
-- axiom 1: 0 ⊕ a = a
(zero_gyro : ∀ (a : C), 0 ⊙ a = a)
-- axiom 2: ⊖a⊕a = 0
(gyr_add_left_neg : ∀ (a : C), ⊝a ⊙ a = 0)
(gyr : C → C → C → C) -- gyr a b c is gyr[a, b]c in the notation from the Wiki
-- axiom 3: ∀ a b c ∈ G, a + (b + c) = (a + b) + gyr a b c
(add_gyr_assoc : ∀ a b c, a ⊙ (b ⊙ c) = (a ⊙ b) ⊙ gyr a b c)
(add_gyr_assoc' : ∀ a b c d, a ⊙ (b ⊙ c) = (a ⊙ b) ⊙ d → d = gyr a b c) -- uniqueness
-- axiom 5: gyr a b = gyr (a + b) b
(gyr_loop : ∀ a b, gyr a b = gyr (a ⊙ b) b)
--axiom 6: a ⊕ b = gyr[a, b](b ⊕ a) for all a, b ∈ G
(gyro_comm: ∀ (a b : C), a ⊙ b = gyr a b (b ⊙ a))
variables (C : Type) [gyrocomm_gyrogroup C]
variables (a b c d : C)
namespace gyrocomm_gyrogroup

axiom gyr_a_b_zero : gyr a b 0 = 0
axiom gyr_distrib : gyr a b (c ⊙ d) = gyr a b c ⊙ gyr a b d

end gyrocomm_gyrogroup


lemma gyrocomm_equal : a ⊙ b = a ⊙ c ↔ b = c :=
begin
  split,
  {intros fabc,
    sorry},
  { intros fbc,
    rw fbc,}
end

(I think thats all is needed to get it to work. I have too many files. The full code can be found here)

Basically, my goal is at

C : Type,
_inst_1 : gyrocomm_gyrogroup C,
a b c : C,
fabc : a⊙b = a⊙c
⊢ b = c

and I want to do refine congr rfl _ at fabc, but lean disagrees with me throwing many errors all saying that I have given it a wrong command. So how to I apply something like this command to fabc?

[Scott Morrison]

It seems you're asking for magic. Why couldn't there be some other reason that they are equal? What is the maths proof here?

[Mario Carneiro]

At first I thought those axioms were for the sake of the #mwe but they are also in your actual project. That's a really weird thing to do; you almost certainly either want them to be theorem ... := sorry if they should be provable, or fields of the structure if they are not