-
Notifications
You must be signed in to change notification settings - Fork 2
/
Braid.lean
33 lines (26 loc) · 797 Bytes
/
Braid.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
import Basic
import Tangle
def isBraid : Wall → Prop
| [] => true
| bs::w => !bs.elem Brick.Cap ∧ !bs.elem Brick.Cup ∧
match w with
| [] => true
| bs'::w => bs.codomain = bs'.domain ∧ isBraid (bs'::w)
def Braid := { w : Wall // isBraid w }
namespace Braid
theorem is_tangle : isBraid w → isTangle w := by
intro hb
induction w with
| nil => simp [isTangle]
| cons bs w hi =>
cases w with
| nil => simp [isTangle]
| cons bs' w =>
rewrite [isBraid] at hb
rewrite [isTangle]
exact And.intro hb.right.right.left (hi hb.right.right.right)
def tangle (b : Braid) : Tangle := ⟨b.val, is_tangle b.property⟩
-- TODO
def permute (b : Braid ) (as : List α) (hdom : b.tangle.domain = as.length) : List α :=
sorry
end Braid