Skip to content

Commit

Permalink
EqN -> Eqv
Browse files Browse the repository at this point in the history
  • Loading branch information
@tjjfvi
tjjfvi committed Feb 27, 2025
1 parent 484f953 commit beb812a
Show file tree
Hide file tree
Showing 5 changed files with 104 additions and 108 deletions.
110 changes: 55 additions & 55 deletions Algebrainet/EqN.lean → Algebrainet/Eqv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,101 +2,101 @@ import Algebrainet.Net

open Net

inductive EqA (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
inductive EqvA (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
| mix_nil :
{xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
EqA S # (mix x nil) x
EqvA S # (mix x nil) x
| nil_mix :
{xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
EqA S # (mix nil x) x
EqvA S # (mix nil x) x
| mix_assoc :
{xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
{yᵢ yₒ : Nat} -> {y : Net S yᵢ yₒ} ->
{zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
EqA S # (mix (mix x y) z) (mix x (mix y z))
EqvA S # (mix (mix x y) z) (mix x (mix y z))

| cat_wires :
{xᵢ xₒ n : Nat} -> {x : Net S xᵢ xₒ} ->
{h : _} ->
EqA S # (cat h x (wires n)) x
EqvA S # (cat h x (wires n)) x
| wires_cat :
{xᵢ xₒ n : Nat} -> {x : Net S xᵢ xₒ} ->
{h : _} ->
EqA S # (cat h (wires n) x) x
EqvA S # (cat h (wires n) x) x
| cat_assoc :
{xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
{yᵢ yₒ : Nat} -> {y : Net S yᵢ yₒ} ->
{zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
{h₀ h₁ h₂ h₃ : _} ->
EqA S # (cat h₀ (cat h₁ x y) z) (cat h₂ x (cat h₃ y z))
EqvA S # (cat h₀ (cat h₁ x y) z) (cat h₂ x (cat h₃ y z))

| swap_swap : EqA S # (cat # swap swap) (mix wire wire)
| cup_swap : EqA S # (cat # cup swap) cup
| swap_cap : EqA S # (cat # swap cap) cap
| swap_swap : EqvA S # (cat # swap swap) (mix wire wire)
| cup_swap : EqvA S # (cat # cup swap) cup
| swap_cap : EqvA S # (cat # swap cap) cap

| move_cup : EqA S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire))
| move_cap : EqA S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap))
| move_swap : EqA S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire)))
| move_agent {A : S.Agent} : EqA S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A)))
| move_cup : EqvA S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire))
| move_cap : EqvA S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap))
| move_swap : EqvA S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire)))
| move_agent {A : S.Agent} : EqvA S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A)))

| cup_cap : EqA S # (cat # (mix cup wire) (mix wire cap)) wire
| cup_cap : EqvA S # (cat # (mix cup wire) (mix wire cap)) wire

| exch :
{xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
{yᵢ yₒ : Nat} -> {y : Net S yᵢ yₒ} ->
{zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
{wᵢ wₒ : Nat} -> {w : Net S wᵢ wₒ} ->
{h₀ h₁ h₂ : _} ->
EqA S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w))
EqvA S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w))

| cat₀ :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h₀ h₁ h₂ : _} ->
EqA S h₀ a b ->
EqA S # (cat h₁ a c) (cat h₂ b c)
EqvA S h₀ a b ->
EqvA S # (cat h₁ a c) (cat h₂ b c)

| cat₁ :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h₀ h₁ h₂ : _} ->
EqA S h₀ a b ->
EqA S # (cat h₁ c a) (cat h₂ c b)
EqvA S h₀ a b ->
EqvA S # (cat h₁ c a) (cat h₂ c b)

| mix₀ :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h : _} ->
EqA S h a b ->
EqA S # (mix a c) (mix b c)
EqvA S h a b ->
EqvA S # (mix a c) (mix b c)

| mix₁ :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h : _} ->
EqA S h a b ->
EqA S # (mix c a) (mix c b)
EqvA S h a b ->
EqvA S # (mix c a) (mix c b)

inductive EqN (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
| refl : {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} -> EqN S # x x
inductive Eqv (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
| refl : {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} -> Eqv S # x x
| fw :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h₀ h₁ : _} -> EqA S h₀ a b -> EqN S h₁ b c ->
EqN S # a c
{h₀ h₁ : _} -> EqvA S h₀ a b -> Eqv S h₁ b c ->
Eqv S # a c
| bk :
{aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
{bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
{cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
{h₀ h₁ : _} -> EqA S h₀ b a -> EqN S h₁ b c ->
EqN S (by rcases h₀ with ⟨⟨⟩,⟨⟩⟩; simp [*]) a c
{h₀ h₁ : _} -> EqvA S h₀ b a -> Eqv S h₁ b c ->
Eqv S (by rcases h₀ with ⟨⟨⟩,⟨⟩⟩; simp [*]) a c

namespace EqN
namespace Eqv

variable
{S : System}
Expand All @@ -107,68 +107,68 @@ variable
{n : Nat}

def cast_ {i₁ o₁ i₂ o₂ : Nat} {x : Net S i₁ o₁} :
{h : (i₁ = i₂) ∧ (o₁ = o₂)} -> EqN S # (castₙ h x) x
{h : (i₁ = i₂) ∧ (o₁ = o₂)} -> Eqv S # (castₙ h x) x
| (And.intro rfl rfl) => refl

def trans {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ b c) : EqN S # a c := by
def trans {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ b c) : Eqv S # a c := by
induction e with
| refl => exact f
| fw a _ ih => exact fw a (ih f)
| bk a _ ih => exact bk a (ih f)

def symm {h : _} (e : EqN S h a b) : EqN S # b a := by
def symm {h : _} (e : Eqv S h a b) : Eqv S # b a := by
induction e with
| refl => exact refl
| fw a _ ih => exact trans ih (bk a refl)
| bk a _ ih => exact trans ih (fw a refl)

def cat₀ {h₀ : _} (e : EqN S h₀ a b) {h₁ h₂ : _} : EqN S # (cat h₁ a c) (cat h₂ b c) := by
def cat₀ {h₀ : _} (e : Eqv S h₀ a b) {h₁ h₂ : _} : Eqv S # (cat h₁ a c) (cat h₂ b c) := by
induction e with
| refl => exact refl
| fw a _ ih => exact fw (b := (cat # _ _)) (.cat₀ a) ih
| bk a _ ih => exact bk (b := (cat # _ _)) (.cat₀ a) ih

def cat₁ {h₀ : _} (e : EqN S h₀ a b) {h₁ h₂ : _} : EqN S # (cat h₁ c a) (cat h₂ c b) := by
def cat₁ {h₀ : _} (e : Eqv S h₀ a b) {h₁ h₂ : _} : Eqv S # (cat h₁ c a) (cat h₂ c b) := by
induction e with
| refl => exact refl
| fw a _ ih => exact fw (b := (cat # _ _)) (.cat₁ a) ih
| bk a _ ih => exact bk (b := (cat # _ _)) (.cat₁ a) ih

def mix₀ {h : _} (e : EqN S h a b) : EqN S # (mix a c) (mix b c) := by
def mix₀ {h : _} (e : Eqv S h a b) : Eqv S # (mix a c) (mix b c) := by
induction e with
| refl => exact refl
| fw a _ ih => exact fw (.mix₀ a) ih
| bk a _ ih => exact bk (.mix₀ a) ih

def mix₁ {h : _} (e : EqN S h a b) : EqN S # (mix c a) (mix c b) := by
def mix₁ {h : _} (e : Eqv S h a b) : Eqv S # (mix c a) (mix c b) := by
induction e with
| refl => exact refl
| fw a _ ih => exact fw (.mix₁ a) ih
| bk a _ ih => exact bk (.mix₁ a) ih

def cat_ {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ c d) {h₁ h₂ : _} : EqN S # (cat h₁ a c) (cat h₂ b d) := by
def cat_ {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ c d) {h₁ h₂ : _} : Eqv S # (cat h₁ a c) (cat h₂ b d) := by
apply trans (cat₀ e) (cat₁ f); simp [*]

def mix_ {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ c d) : EqN S # (mix a c) (mix b d) :=
def mix_ {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ c d) : Eqv S # (mix a c) (mix b d) :=
trans (mix₀ e) (mix₁ f)

def mix_nil : EqN S # (mix a nil) a := fw .mix_nil refl
def nil_mix : EqN S # (mix nil a) a := fw .nil_mix refl
def mix_assoc : EqN S # (mix (mix a b) c) (mix a (mix b c)) := fw .mix_assoc refl
def mix_nil : Eqv S # (mix a nil) a := fw .mix_nil refl
def nil_mix : Eqv S # (mix nil a) a := fw .nil_mix refl
def mix_assoc : Eqv S # (mix (mix a b) c) (mix a (mix b c)) := fw .mix_assoc refl

def cat_wires {h : _} : EqN S # (cat h a (wires n)) a := fw .cat_wires refl
def wires_cat {h : _} : EqN S # (cat h (wires n) a) a := fw .wires_cat refl
def cat_assoc {h₀ h₁ h₂ h₃ : _} : EqN S # (cat h₀ (cat h₁ a b) c) (cat h₂ a (cat h₃ b c)) := fw .cat_assoc refl
def cat_wires {h : _} : Eqv S # (cat h a (wires n)) a := fw .cat_wires refl
def wires_cat {h : _} : Eqv S # (cat h (wires n) a) a := fw .wires_cat refl
def cat_assoc {h₀ h₁ h₂ h₃ : _} : Eqv S # (cat h₀ (cat h₁ a b) c) (cat h₂ a (cat h₃ b c)) := fw .cat_assoc refl

def swap_swap : EqN S # (cat # swap swap) (mix wire wire) := fw .swap_swap refl
def cup_swap : EqN S # (cat # cup swap) cup := fw .cup_swap refl
def swap_cap : EqN S # (cat # swap cap) cap := fw .swap_cap refl
def swap_swap : Eqv S # (cat # swap swap) (mix wire wire) := fw .swap_swap refl
def cup_swap : Eqv S # (cat # cup swap) cup := fw .cup_swap refl
def swap_cap : Eqv S # (cat # swap cap) cap := fw .swap_cap refl

def move_cup : EqN S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire)) := fw .move_cup refl
def move_cap : EqN S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap)) := fw .move_cap refl
def move_swap : EqN S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire))) := fw .move_swap refl
def move_agent {A : S.Agent} : EqN S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A))) := fw .move_agent refl
def move_cup : Eqv S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire)) := fw .move_cup refl
def move_cap : Eqv S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap)) := fw .move_cap refl
def move_swap : Eqv S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire))) := fw .move_swap refl
def move_agent {A : S.Agent} : Eqv S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A))) := fw .move_agent refl

def cup_cap : EqN S # (cat # (mix cup wire) (mix wire cap)) wire := fw .cup_cap refl
def cup_cap : Eqv S # (cat # (mix cup wire) (mix wire cap)) wire := fw .cup_cap refl

def exch {h₀ h₁ h₂ : _} : EqN S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w)) := fw .exch refl
def exch {h₀ h₁ h₂ : _} : Eqv S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w)) := fw .exch refl
14 changes: 7 additions & 7 deletions Algebrainet/EqN/Move.lean → Algebrainet/Eqv/Move.lean
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
import Algebrainet.Net
import Algebrainet.EqN.Twist
import Algebrainet.Eqv.Twist

open Net
namespace EqN
namespace Eqv

variable {S : System}

Expand All @@ -11,7 +11,7 @@ set_option autoImplicit false
def twist_net_wire
{aᵢ aₒ: Nat}
{A : Net S aᵢ aₒ}
: EqN S #
: Eqv S #
(cat # (mix A wire) (twist aₒ 1))
(cat # (twist aᵢ 1) (mix wire A))
:= by
Expand Down Expand Up @@ -154,7 +154,7 @@ def twist_net_wire
def twist_net_wires
{aᵢ aₒ b : Nat}
{A : Net S aᵢ aₒ}
: EqN S #
: Eqv S #
(cat # (mix A (wires b)) (twist aₒ b))
(cat # (twist aᵢ b) (mix (wires b) A))
:= by
Expand Down Expand Up @@ -191,7 +191,7 @@ def twist_net_wires

def twist_wires_net
{a bᵢ bₒ : Nat} {B : Net S bᵢ bₒ}
: EqN S #
: Eqv S #
(cat # (mix (wires a) B) (twist a bₒ))
(cat # (twist a bᵢ) (mix B (wires a)))
:= by
Expand All @@ -213,7 +213,7 @@ def twist_wires_net
def twist_nets
{aᵢ aₒ : Nat} {A : Net S aᵢ aₒ}
{bᵢ bₒ : Nat} {B : Net S bᵢ bₒ}
: EqN S #
: Eqv S #
(cat # (mix A B) (twist aₒ bₒ))
(cat # (twist aᵢ bᵢ) (mix B A))
:= by
Expand All @@ -227,7 +227,7 @@ def twist_nets
apply cat₁ (symm down_up)
repeat simp

def cap_cup : EqN S # (cat # (mix wire cup) (mix cap wire)) wire := by
def cap_cup : Eqv S # (cat # (mix wire cup) (mix cap wire)) wire := by
apply trans; apply cat₀; .
apply trans (mix_ wire_cat.symm cup_swap.symm)
apply exch.symm
Expand Down
Loading

0 comments on commit beb812a

Please sign in to comment.