automorphisms of Z2

lol.agda

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.List

data Void : Set where

data Pair (L R : Set) : Set where
  pair : L -> R -> Pair L R

id : forall {T : Set} -> T -> T
id v = v

data Unit : Set where
  pt : Unit

fold : {T A : Set} -> (T -> A -> A) -> A -> List T -> A
fold {T}{A} f a l = rec a l
  where
    rec : A -> List T -> A
    rec a [] = a
    rec a (h ∷ t) = rec (f h a) t

map : {A B : Set} -> (A -> B) -> List A -> List B
map f [] = []
map f (a ∷ b) = (f a) ∷ (map f b)


data Aut (C : Set) : Set where
  aut : List C -> List (C -> C) -> Aut C

_++_ : ∀ {T} -> List T -> List T -> List T
[] ++ a = a
(c ∷ t) ++ a = c ∷ (t ++ a)

genPairs : {T : Set} -> List T -> List (Pair T T)
genPairs l =
  fold (_++_) [] (map (λ i -> map (λ i' -> (pair i  i')) l) l)


data Maybe (T : Set) : Set where
  some : T -> Maybe T
  none : Maybe T

itemAt : {T : Set} -> (ix : Nat) -> (l : List T) -> Maybe T
itemAt _ [] = none
itemAt zero (x ∷ _) = some x
itemAt (suc i) (_ ∷ l) = itemAt i l


_>>>=_ : {T : Set} -> Maybe T -> (T -> Maybe T) -> Maybe T
none >>>= _ = none
some v >>>= f = f v
NoStuckPointsTRec : {T : Set} -> List (T -> T) -> List (Pair T T) -> Set
NoStuckPointsTRec _ []  = Unit 
NoStuckPointsTRec {T} fs ((pair l r) ∷ t) =
  Pair (Σ (List Nat) λ ixs -> unwrap ((composeSeqv id ixs)) l r)
       (NoStuckPointsTRec fs t)
  where
    composeSeqv : (T -> T) -> List Nat -> Maybe (T -> T)
    composeSeqv f [] = some f
    composeSeqv p (n ∷ t) =
      itemAt n fs >>>= λ f -> composeSeqv (λ k -> f (p k)) t
    unwrap : Maybe (T -> T) -> T -> T -> Set
    unwrap (some f) l r = f l ≡ r
    unwrap none _ _ = Void

NoStuckPointsT : {T : Set} -> Aut T -> Set
NoStuckPointsT (aut o ms) = 
  let instPairs = genPairs o
  in NoStuckPointsTRec ms instPairs

not : Bool -> Bool
not false = true
not true = false

BoolAut : Aut Bool
BoolAut = aut (true ∷ false ∷ []) (not ∷ id ∷ [])

pattern Proof-Lol =
  pair (0 ∷ [] , refl)
  (pair (1 ∷ []  , refl)
  (pair (1 ∷ [] , refl )
  (pair (0 ∷ [] , refl) pt)))

BoolAutNSP : NoStuckPointsT BoolAut
BoolAutNSP = Proof-Lol

reverseR : {T : Set} -> List T ->  List T -> List T
reverseR a (h ∷ t) = reverseR (h ∷ a) t
reverseR a [] = a
invert-base : {T : Set} -> Aut T -> Aut T
invert-base (aut l m) = aut (reverseR [] l) m

BoolAutAut : Aut (Aut Bool)
BoolAutAut = aut (BoolAut ∷ invert-base BoolAut ∷ []) (invert-base ∷ id ∷ [])
  
BoolAutInvNSP : NoStuckPointsT (invert-base BoolAut)
BoolAutInvNSP = Proof-Lol
    
BoolAutAutNSP : NoStuckPointsT BoolAutAut
BoolAutAutNSP = Proof-Lol

BoolAutAutAut : Aut (Aut (Aut Bool))
BoolAutAutAut =
  aut (BoolAutAut ∷ invert-base BoolAutAut ∷ []) (invert-base ∷ id ∷ [])

BoolAutAutAutNSP : NoStuckPointsT (BoolAutAutAut)
BoolAutAutAutNSP = Proof-Lol


BoolAutNT : Nat -> Set
BoolAutNT (suc n) = Aut (BoolAutNT n)
BoolAutNT zero = Aut Bool


BoolAutN : (n : Nat) -> BoolAutNT n
BoolAutN zero = BoolAut
BoolAutN (suc zero) =
  let k = BoolAutN 0
  in aut (k ∷ invert-base k ∷ []) (invert-base ∷ id ∷ [])
BoolAutN (suc (suc n)) =
  let k = BoolAutN (suc n)
  in aut (k ∷ invert-base k ∷ []) (invert-base ∷ id ∷ [])


BoolAutN9999 : BoolAutNT 9999 
BoolAutN9999 = BoolAutN 9999

BoolAutNSP' : NoStuckPointsT (BoolAutN 9999) -- enter number you like :3
BoolAutNSP' = Proof-Lol