what the hell..

ln.lean

def wmap : Type _ -> Type _ -> Type _ := 
  fun A B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i


def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by
  intro w
  let ⟨ ⟨ f , h ⟩ , p ⟩ := w
  simp at p
  simp
  intro a
  refine ⟨ f a , ?_ ⟩ 
  apply p

def mkwmap (f: A -> B)(h:B->A)(p: ∀ i, h (f i) = i) : wmap A B := ⟨ ⟨ f , h ⟩  , p ⟩ 

def bool_not_wmap : wmap Bool Bool := by 
  refine mkwmap ?f ?h ?p
  exact not 
  exact not
  intro i
  rw [Bool.not_not]


example : a = (not (not a)) := by
  let ⟨ b , p ⟩ := p1 bool_not_wmap a
  rw [<- p]
  let prf : ∀ i, not i = not (not (not i)) := by intro i; cases i <;> rfl
  exact prf b


def iterf : Nat -> (T -> T) -> (T -> T)
| .zero, _ => id
| .succ a, f => fun i => f ((iterf a f) i)

-- #reduce (iterf 4 (Nat.mul 2)) 1

def orbit : (T -> T) -> Type _ | f => @Subtype Nat fun n => (iterf n f) = id

def orbit_id {T:Type _}: orbit (@id T) := by
  refine ⟨ 0 , ?p ⟩ 
  unfold iterf
  rfl

def id_wmap : wmap T T := by 
  refine mkwmap ?f ?h ?p
  exact id
  exact id
  simp

def orbit_id_map {T:Type _}: wmap (orbit (@id T)) (orbit (@id T)) := id_wmap


def iscontr (T:Type _): Type _ := @Subtype T fun cp => ∀ i , cp = i



-- unsafe
axiom same_if_same_eval {A:Type _}{f:A->A}{p1 p2:orbit f}: (iterf p1.val f = iterf p2.val f) -> p1 = p2


example : Empty := by
  let v1 : orbit (@id Unit) := ⟨ 0 , rfl ⟩
  let v2 : orbit (@id Unit) := ⟨ 1 , rfl ⟩
  let p : v1 = v2 := by
    apply same_if_same_eval
    simp
    rfl
  let eq : v1 = v2 -> v1.val = v2.val := congrArg Subtype.val
  let k := eq p
  simp at k




def id_map_contr {T} : iscontr (orbit (@id T)) := by
  unfold iscontr
  refine ⟨ orbit_id , ?p ⟩ 
  intro i
  unfold orbit at i
  simp at i
  let ⟨ n , prf ⟩ := i
  unfold orbit_id
  apply same_if_same_eval
  simp
  induction n
  {
    simp
  }
  {
    case _ n2 ih => 
      cases n2
      {
        unfold iterf
        rfl
      }
      {
        exact ih prf
      }
  }

example : wmap Bool Nat := by
  refine mkwmap ?f ?h ?p
  {
    exact fun i =>
      match i with 
      | .false => 0
      | .true => 1
  }
  {
    exact fun i =>
      match i with
      | .zero => .false
      | .succ .zero => .true
      | .succ (.succ _) => .false
  }
  intro i
  cases i <;> simp



def iso : Type _ -> Type _ -> Type _
| A, B =>
  @Subtype (Prod (A -> B) (B -> A)) fun (.mk f h) =>
    And (∀ i, f (h i) = i) (∀ i, h (f i) = i)

def mkiso (f:A->B)(h:B->A)(p1:∀ i, f (h i) = i)(p2:∀ i, h (f i) = i): iso A B := ⟨ ⟨ f , h ⟩ , ⟨ p1 , p2 ⟩ ⟩ 

def promote_wmap (w:wmap A B): (∀ i, w.val.fst (w.val.snd i) = i) -> iso A B := by
  let (.mk (.mk f h) p) := w
  simp at p
  simp
  intro k
  exact mkiso f h k p
  

def p2 (p:iso A B) : ∀ i:A, @Subtype B fun k => p.val.snd k = i := by
  intro i
  refine ⟨p.val.fst i, ?property⟩
  let ⟨ ⟨ f , h ⟩ , ⟨ p1 , p2 ⟩ ⟩ := p
  simp
  apply p2


def zmod3rel (a b:Nat) : Prop := a % 3 = b % 3

def zmod3 : Type _ := Quot zmod3rel
  
#check Nat.le_of_succ_le_succ

  

def lt : Nat -> Nat -> Prop 
| .zero, .succ _ => True
| .succ a, .succ b => lt a b
| _ , _ => False

example : lt 0 (n + 1) := by
  cases n <;> unfold lt <;> trivial

-- def zmod3_add : zmod3 -> zmod3 -> zmod3 := by
--   intro a b
--   induction a using Quot.rec
--   {
--     case _ k => 
--       induction b using Quot.rec
--       case _ j => 
--         exact Quot.mk zmod3rel (k + j)
--       case _ a b d => 
--         unfold zmod3rel at d
--         induction a
--         induction b 
--         simp
--         case _ n ih => 
          
--   }

-- def zmod3lt : zmod3 -> zmod3 -> Prop := by
--   intro a b
--   induction a using Quot.rec
--   {
--     case _ k => 
--       induction b using Quot.rec
--       case _ j  => 

--   }
--   {

--   }

def fmap_exists {A:Type _}{B:Type _}{op:A->A->A}{a b:B}:
  (w:wmap A B) -> let (.mk (.mk f h) _) := w;
  @Subtype (B->B->B) fun opm => (op (h a) (h b) = h (opm a b)) ∧
                                (opm = fun (b1:B) (b2:B) => f (op (h b1) (h b2)))
:= by
  intro w
  let (.mk (.mk f h) p1) := w
  simp
  refine ⟨?val, ?property⟩
  exact fun b1 b2 =>
    f (op (h b1) (h b2))
  rw [(p1 (op (h a) (h b)))]
  exact ⟨rfl, rfl⟩

def fmap_iso {op:A->A->A}{opm:B->B->B}
  (w:iso A B)(p:∀ a b, w.val.fst (op (w.val.snd a) (w.val.snd b)) = opm a b)
  : op (w.val.snd a) (w.val.snd b) = w.val.snd (opm a b)
:= by
  let ⟨ ⟨ f , h ⟩ , ⟨ p1 , p2 ⟩ ⟩ := w
  simp at *
  rw [<-p, p2]

def fmap_through {op:A->A->A}{opm:B->B->B}
  (w:wmap A B): let (.mk (.mk f h) _) := w; 
  (p:∀ a b, f (op (h a) (h b)) = opm a b)
  -> op (h a) (h b) = h (opm a b)
:= by
  let (.mk (.mk f h) p) := w
  simp at p
  simp
  intro prf
  rw [<-prf,p]

@[simp]
def fmap_less {op:A->A->A}{opm:B->B->B} (w:iso A B) : let (.mk ⟨ f , h ⟩ _) := w; (f (op (h a) (h b))) = opm a b <-> (op (h a) (h b) = h (opm a b)) := by
  let (.mk ⟨ f , h ⟩ ⟨ p1 , p2 ⟩ ) := w
  simp
  apply Iff.intro
  {
    intro k
    rw [<-k, p2]
  }
  {
    intro k
    rw [k, p1]
  }


def nat2list : Nat -> List Unit
| .zero => .nil
| .succ a => .cons () (nat2list a)
def list2nat : List Unit -> Nat
| .nil => .zero
| .cons .unit t => .succ (list2nat t)

def ln_coh : (a : List Unit) -> nat2list (list2nat a) = a := by
  intro i
  match i with
  | .cons () a => unfold list2nat nat2list; simp; exact (ln_coh a)
  | .nil => unfold list2nat nat2list; simp;

def nl_coh : (a : Nat) -> list2nat (nat2list a) = a := by
  intro i
  match i with
  | .succ a => unfold list2nat nat2list; simp; exact (nl_coh a)
  | .zero => unfold list2nat nat2list; simp;

def list_int : wmap (List Unit) Nat := mkwmap list2nat nat2list ln_coh


def fmap_append_plus :
    (nat2list a1) ++ (nat2list a2) = nat2list (a1 + a2)
:= by
  cases a1
  {
    cases a2 <;> unfold nat2list <;> simp
  }
  {
    cases a2
    {
      case _ a =>
        unfold nat2list
        simp
    }
    {
      case _ a b =>
        rw [Nat.add_add_add_comm]
        unfold nat2list
        simp
        induction a
        {
          simp [nat2list]
        }
        {
          case _ n ih =>
            simp [nat2list]
            rw [ih]
            rw [Nat.add_right_comm _ 1 b]
        }
    }
  }

def fmap_append_plus3 : list2nat (nat2list a1 ++ nat2list a2) = a1 + a2 := by
  let e1 := fmap_less (promote_wmap list_int nl_coh) (op:=List.append) (opm:=Nat.add) (a:=a1) (b:=a2)
  unfold promote_wmap list_int mkwmap mkiso at e1
  dsimp at e1
  rw [e1]
  apply fmap_append_plus
  

def fmap_append_plus2 : list2nat (nat2list a1 ++ nat2list a2) = a1 + a2 := by
  cases a1 
  {
    cases a2 <;> unfold nat2list list2nat <;> simp
    apply nl_coh
  }
  {
    case _ p => 
      cases a2
      unfold nat2list
      simp
      unfold list2nat
      simp
      apply nl_coh
      case _ k => 
        induction p
        simp
        unfold nat2list nat2list
        simp
        rw [list2nat.eq_2]
        simp
        rw [Nat.add_comm _ 1, Nat.add_comm k 1]
        apply congrArg
        unfold list2nat
        simp
        rw [Nat.add_comm]
        apply congrArg
        rw [<-nat2list.eq_def]
        apply nl_coh
        case _ d ih =>
          rw [<-Nat.succ_eq_add_one]
          unfold nat2list
          rw [<-Nat.succ_eq_add_one]
          unfold list2nat
          simp
          let pi1 : d + 1 + 1 + (k + 1) = (d + 1 + 1 + k) + 1 := by omega
          rw [pi1]
          rw [Nat.add_comm, Nat.add_comm (d + 1 + 1 + k) 1]
          apply congrArg
          rw [<-nat2list.eq_2, Nat.succ_eq_add_one]
          let pi2 : (d + 1) + (k + 1) = ((d + 1) + 1) + k := by omega
          rw [<-pi2]
          apply ih
  }



example : List.append (a:List Unit) (b:List Unit) = List.append b a := by
  let (.mk a1 r1) := p1 list_int a
  let (.mk a2 r2) := p1 list_int b
  rw [<-r1, <-r2]
  let x1 := fmap_through list_int @fmap_append_plus2 (a:=a1) (b:=a2)
  rw [List.append_eq, List.append_eq, x1]
  let x2 := fmap_through list_int @fmap_append_plus2 (a:=a2) (b:=a1)
  rw [x2]
  apply congrArg
  rw [Nat.add_comm]


example : (a:List Unit) ++ b = b ++ a := by
  let (.mk a1 r1) := p1 list_int a
  let (.mk a2 r2) := p1 list_int b
  rw [<-r1, <-r2]
  rw [fmap_append_plus, fmap_append_plus]
  apply congrArg
  rw [Nat.add_comm]