Eckmann-Hilton 論法を Coq, Idris で。

eckmann-hilton.idr

import Syntax.PreorderReasoning
G : Type
m : G -> G -> G
n : G -> G -> G
u_m : G
u_n : G
postulate m_unit_l : (x : G) -> (m u_m x = x)
postulate m_unit_r : (x : G) -> (m x u_m = x)
postulate n_unit_l : (x : G) -> (n u_n x = x)
postulate n_unit_r : (x : G) -> (n x u_n = x)
postulate eckmann_hilton_law : (g1, h1, g2, h2 : G) -> n (m g1 h1) (m g2 h2) = m (n g1 g2) (n h1 h2)

total unit_eq : u_m = u_n
unit_eq = ?unit_eq_rhs

total unit_eq' : u_m = u_n
unit_eq' =
  u_m
    ={ sym (m_unit_l u_m) }=
  (m u_m u_m)
    ={ cong {f = flip m u_m} $ sym (n_unit_r u_m) }=
  (m (n u_m u_n) u_m)
    ={ cong $ sym (n_unit_l u_m) }=
  (m (n u_m u_n) (n u_n u_m))
    ={ sym $ eckmann_hilton_law u_m u_n u_n u_m }=
  (n (m u_m u_n) (m u_n u_m))
    ={ cong $ m_unit_r u_n }=
  (n (m u_m u_n) u_n)
    ={ n_unit_r _ }=
  (m u_m u_n)
    ={ m_unit_l u_n }=
  u_n
    QED

total unit_l_n : (x : G) -> n u_m x = x
unit_l_n x = replace {P = \z => n z x = x} (sym unit_eq) (n_unit_l x)

total unit_r_n : (x : G) -> n x u_m = x
unit_r_n x = replace {P = \z => n x z = x} (sym unit_eq) (n_unit_r x)

total op_eq : (x, y : G) -> m x y = n x y
op_eq = ?op_eq_rhs

total op_eq' : (x, y : G) -> m x y = n x y
op_eq' x y =
  (m x y)
    ={ cong {f = flip m y} $ sym $ unit_r_n x }=
  (m (n x u_m) y)
    ={ cong $ sym $ unit_l_n y }=
  (m (n x u_m) (n u_m y))
    ={ sym $ eckmann_hilton_law _ _ _ _ }=
  (n (m x u_m) (m u_m y))
    ={ cong $ m_unit_l _ }=
  (n (m x u_m) y)
    ={ cong {f = flip n _} $ m_unit_r _ }=
  (n x y)
    QED

total commutative : (x, y : G) -> m x y = m y x
commutative x y = ?commutative_rhs

total commutative' : (x, y : G) -> m x y = m y x
commutative' x y =
  (m x y)
    ={ cong {f = flip m _} $ sym $ unit_l_n _ }=
  (m (n u_m x) y)
    ={ cong $ sym $ unit_r_n _ }=
  (m (n u_m x) (n y u_m))
    ={ sym $ eckmann_hilton_law _ _ _ _ }=
  (n (m u_m y) (m x u_m))
    ={ cong { f = flip n _ } $ m_unit_l _ }=
  (n y (m x u_m))
    ={ cong $ m_unit_r _ }=
  (n y x)
    ={ sym $ op_eq' _ _ }=
  (m y x)
    QED

syntax "[" [b] "]" [a] = cong {f = b} a

syntax "{" {target} "}" at "[" [application] "]" [pf] = cong {f = \ target => application} pf

unit_eq_rhs = proof
  rewrite m_unit_l u_m
  rewrite [m u_m] n_unit_r u_m
  rewrite [flip m (n u_m u_n)] n_unit_l u_m
  rewrite eckmann_hilton_law u_n u_m u_m u_n
  rewrite sym (m_unit_r u_n)
  rewrite sym (m_unit_l u_n)
  rewrite sym (n_unit_r u_n)
  trivial

op_eq_rhs = proof
  intros
  rewrite {y} at [m x y] n_unit_l y
  rewrite {x} at [m x (n u_n y)] n_unit_r x
  rewrite eckmann_hilton_law x u_n u_n y
  rewrite unit_eq
  rewrite m_unit_l y
  rewrite m_unit_r x
  trivial

commutative_rhs = proof
  intros
  rewrite {x} at [m x y] m_unit_l x
  rewrite {y} at [m (m u_m x) y] m_unit_r y
  rewrite sym (op_eq (m u_m x) (m y u_m))
  rewrite sym (eckmann_hilton_law u_m x y u_m)
  rewrite sym unit_eq
  rewrite n_unit_l y
  rewrite n_unit_r x
  trivial

eckmann-hilton.v

Axiom G : Set.
Axiom m : G -> G -> G.
Axiom n : G -> G -> G.
Axiom u_m : G.
Axiom u_n : G.
Axiom m_unit_l : forall (x : G), m u_m x = x.
Axiom m_unit_r : forall (x : G), m x u_m = x.
Axiom n_unit_l : forall (x : G), n u_n x = x.
Axiom n_unit_r : forall (x : G), n x u_n = x.
Axiom Eckmann_Hilton_law : forall (g1 h1 g2 h2 : G), n (m g1 h1) (m g2 h2) = m (n g1 g2) (n h1 h2).

Theorem unitEq : u_m = u_n.
Proof.
  rewrite <-(n_unit_l u_n).
  pattern u_n at 1.
  rewrite <-(m_unit_r u_n).
  pattern u_n at 2.
  rewrite <-(m_unit_l u_n).
  rewrite Eckmann_Hilton_law.
  rewrite n_unit_r.
  rewrite n_unit_l.
  rewrite m_unit_l.
  reflexivity.
Qed.

Theorem multEq : forall (x y : G), m x y = n x y.
Proof.
  intros.
  rewrite <-(n_unit_r x).
  rewrite <-(n_unit_l y).
  rewrite <-Eckmann_Hilton_law.
  rewrite n_unit_r.
  rewrite n_unit_l.
  rewrite <-unitEq.
  rewrite m_unit_r.
  rewrite m_unit_l.
  reflexivity.
Qed.

Definition u : G := u_m.
Definition o : G -> G -> G := m.

Definition unit_l : forall (x : G), o u x = x := m_unit_l.
Definition unit_r : forall (x : G), o x u = x := m_unit_r.

Definition unitEq_n : u = u_n := unitEq.
Lemma unitEq_m : u = u_m.
Proof.
  reflexivity.
Qed.
Lemma o_eq_m : forall (x y : G), o x y = m x y.
Proof.
  reflexivity.
Qed.
Definition o_eq_n : forall (x y : G), o x y = n x y := multEq.

Lemma Eckmann_Hilton_distr : forall (g1 g2 h1 h2 : G), o (o g1 h1) (o g2 h2) = o (o g1 g2) (o h1 h2).
Proof.
  intros.
  rewrite (o_eq_m g1 h1).
  rewrite (o_eq_m g2 h2).
  rewrite o_eq_n.
  rewrite (o_eq_n g1 g2).
  rewrite (o_eq_n h1 h2).
  rewrite (o_eq_m (n g1 g2) (n h1 h2)).
  rewrite Eckmann_Hilton_law.
  reflexivity.
Qed.

Theorem commutative : forall (x y : G), o x y = o y x.
Proof.
  intros.
  pattern x at 1.
  rewrite <-unit_l.
  pattern y at 1.
  rewrite <-unit_r.
  rewrite Eckmann_Hilton_distr.
  rewrite unit_l.
  rewrite unit_r.
  reflexivity.
Qed.