Zulip Chat Archive

Stream: new members

Topic: gyro_mul_left_inj


view this post on Zulip James Arthur (Aug 13 2020 at 09:45):

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 : ab = ac
 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?

view this post on Zulip Scott Morrison (Aug 13 2020 at 09:52):

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?

view this post on Zulip Mario Carneiro (Aug 13 2020 at 12:56):

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


Last updated: May 13 2021 at 18:26 UTC