amaze_your_friends_at_parties.lean

import Mathlib.Logic.Basic
import Mathlib.Tactic.GeneralizeProofs
import Mathlib.Logic.Function.Basic
-- import Mathlib.Tactic
-- import Aesop

def wmap : Sort _ -> Sort _ -> Sort _ | A, B => @Subtype ((A -> B) ×' (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i

def fiber (h:B->A)(a:A) := @Subtype B fun b => h b = a

def wtransp : (w:wmap A B) -> ∀ a:A , fiber w.val.snd a := by
  intro w
  let ⟨ ⟨ f , h ⟩ , p ⟩ := w
  intro a
  refine ⟨ f a , ?_ ⟩
  apply p

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 mkwmap (f: A->B)(h:B->A)(p: ∀ i, h (f i) = i) : wmap A B := ⟨ ⟨ f , h ⟩  , p ⟩

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

def hmor1 (op1:B->B)(op2:A->A)(p:A->B) := ∀ a1, op1 (p a1) = p (op2 a1)
@[reducible]
def hmor2 (op1:B->B->B)(op2:A->A->A)(p:A->B) := ∀ a1 a2, op1 (p a1) (p a2) = p (op2 a1 a2)

def hmor2_exists {A:Sort _}{B:Sort _}(w:wmap A B) (op:A->A->A):
  let (.mk (.mk f h) _) := w;
  @Subtype (B->B->B) fun opm => (hmor2 op opm h) ∧
                                (opm = fun (b1:B) (b2:B) => f (op (h b1) (h b2)))
:= by
  let (.mk (.mk f h) p1) := w
  simp
  refine ⟨?val, ?property⟩
  exact fun b1 b2 =>
    f (op (h b1) (h b2))
  simp at p1
  unfold hmor2
  dsimp
  apply And.intro
  intro a b
  rewrite [(p1 (op (h a) (h b)))]
  rfl
  rfl

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

@[reducible]
def hmor_append_plus :
  hmor2 (List.append) (Nat.add) (nat2list)
:= by
  unfold hmor2
  intro a1 a2
  dsimp only [List.append_eq, Nat.add_eq]
  cases a1
  {
    cases a2 <;> unfold nat2list <;> simp
  }
  {
    cases a2
    {
      case _ a =>
        unfold nat2list
        simp
    }
    {
      case _ a b =>
        dsimp only [Nat.succ_eq_add_one]
        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]
        }
    }
  }


example : (a:List Unit) ++ b = b ++ a := by
  let (.mk a1 r1) := wtransp list_nat a
  let (.mk a2 r2) := wtransp list_nat b
  rw [<-r1, <-r2]
  unfold list_nat mkwmap
  simp
  let h := hmor_append_plus
  unfold hmor2 at h
  dsimp at h
  repeat rw (config := { transparency := Lean.Meta.TransparencyMode.all }) [h]
  apply congrArg -- the juice!
  rw [Nat.add_comm]


def cast_rfl_irrel : cast rfl v = v := by rfl

def heq_to_eq (h:HEq a b) : a = b := by
  cases h
  rfl

axiom reduce_cast_subtype_proj_1 {A:Type}{v1:A}{p1 p2:A->Prop}{k1: p1 v1}(eq:{ i // p1 i } = { i // p2 i }):
  (@cast { i // p1 i } { i // p2 i } (eq) ⟨v1, k1⟩).val = v1

@[simp]
def transp_eq_1 (w:wmap A B): (wtransp w k).val = w.val.fst k := by
  unfold wtransp
  let (.mk (.mk f h) _) := w
  dsimp

def strict_wmap (w:wmap A B) := ∀ i, w.val.fst (w.val.snd i) = i

set_option pp.proofs true in
def shift_tr_fun (w:wmap A B)(h1:w.val.fst a = b): w.val.snd b = a := by
  let (.mk (.mk f h) p1) := w
  dsimp at p1 h1
  dsimp
  let eq1 : h (f a) = h b := by
    exact congrArg h h1
  rw [p1] at eq1
  exact Eq.symm eq1

set_option pp.proofs true in
def shift_rt_fun (w:wmap A B)(c1:strict_wmap w)(h1:w.val.snd b = a): w.val.fst a = b := by
  let (.mk (.mk f h) p1) := w
  dsimp at p1 h1
  dsimp
  unfold strict_wmap at c1
  dsimp at c1
  rw [<-h1]
  rw [c1]

def prune_symm {f:a=b->a=b} : Eq.symm (f (Eq.symm k)) = k := by
  rfl

set_option pp.proofs true in
set_option pp.parens true in
set_option pp.fieldNotation false in
def reduce_cast_subtype_proj_1_ {A : Type}{p1 p2 : A → Prop}{k:{i // p1 i}} (eq : {i // p1 i} = {i // p2 i}):
  (cast eq k).val = k.val
:= by
  let eq0 : ({ i // (p2 i) } → A) = ({ i // (p1 i) } → A) := implies_congr (Eq.symm eq) rfl
  apply congr_heq
  {
    refine heq_of_eqRec_eq ?_ ?_
    exact eq0
    rw [@eqRec_eq_cast]
    generalize eq1 : (implies_congr (Eq.symm eq) rfl) = k
    -- let eq3 
    -- : HEq (@Eq.rec Type ({ i // (p2 i) } → A) (fun x h => (({ i // (p2 i) } → A) = x)) rfl ({ i // (p1 i) } → A) k) 
    --       (@rfl Type ({ i // (p2 i) } → A)) 
    -- := by
    --   exact (eqRec_heq k rfl)
    let eq4 : 
      (@Eq.rec Type ({ i // (p2 i) } → A) (fun x h => (({ i // (p2 i) } → A) = x)) rfl ({ i // (p1 i) } → A) k)
      = 
      (by rewrite [eq0]; rfl)
    := by
      exact eq1
    dsimp at eq4
    rw [eq4]
    rw [(cast_eq rfl k)]
    let eq5 : (@Subtype.val A fun i => (p1 i)) = cast rfl (@Subtype.val A fun i => (p1 i)) := by rfl
    rw [eq5]
    let eq7 : HEq k (@rfl Type ({ i // (p1 i) } → A)) := by
      exact (heq_of_eqRec_eq (congrFun (congrArg Eq eq0) ({ i // (p1 i) } → A)) rfl)
    congr
    let eq8 : (@Subtype.val A fun i => (p2 i)) = (by rw [<-eq]; exact @Subtype.val A fun i => (p1 i)) := by
      dsimp
      -- rw [prune_symm]
      
      admit
    rw [eq8]
    dsimp
    apply cast_heq
  }
  exact cast_heq eq k


#check heq_cast_iff_heq
#check Subtype.val.eq_1
#check Subtype.val

def OEq {A:Sort l} (a b:A) := ∀ (P:A->Prop), P a -> P b

def oeq_is_eq : OEq a b <-> a = b := by
  apply Iff.intro
  {
    intro k
    unfold OEq at k
    let eq := k (fun i => a = i) rfl
    dsimp at eq
    exact eq
  }
  {
    intro i
    cases i
    intro k
    apply id
  }

def is_contr (T:Sort _) := (cc:T) ×' ∀ i, i = cc

def contr_to_contr_fun_sp: is_contr T -> is_contr (T -> T) := by
  intro (.mk cc p)
  refine .mk id ?_
  intro f
  funext i
  generalize f i = k
  rewrite [p i, p k, id_def]
  rfl

def contr_sp_fun_irrel (c:is_contr T){f h:T->T}: f = h := by
  let (.mk cc cp) := contr_to_contr_fun_sp c
  rw [cp f, <-cp h]


def id_wmap : wmap T T := by
  refine mkwmap id id ?_
  intro i
  rfl

set_option pp.proofs true in
def contr_ty_to_contr_wmap : is_contr T -> is_contr (wmap T T) := by
  intro cpo
  let (.mk cc cp) := cpo
  refine .mk ?_ ?_
  exact id_wmap
  intro w
  let (.mk (.mk f h) p1) := w
  dsimp at p1
  let eq1 := contr_sp_fun_irrel cpo (f:=f) (h:=id)
  let eq2 := contr_sp_fun_irrel cpo (f:=h) (h:=id)
  subst eq1
  subst eq2
  rfl


inductive Just {A:Sort _} : A -> Sort _ where | mk (v:A) : Just v

def just_contr : is_contr (Just m) := by
  refine .mk (.mk m) ?_
  intro i
  cases i
  rfl


def glued : wmap (Just a) (Just b) := by
  refine mkwmap ?_ ?_ ?_
  exact fun _ => Just.mk b
  exact fun _ => Just.mk a
  intro i
  exact rfl

def true_false_glued : wmap (Just true) (Just false) := glued

-- example : False := by
--   let (.mk v1 p) := wtransp true_false_glued (Just.mk true)
--   unfold true_false_glued glued mkwmap at p
--   dsimp at p


def is_glued (w:wmap (Just a) (Just b)): w = glued ∨ Not (w = glued) := by
  exact eq_or_ne w glued

-- def wmap_to_eq (w:wmap (Just a) (Just b))(p1:Not (w = glued)): a = b := by
--   -- let (.mk v1 p2) := just_contr (m:=a)
--   -- let (.mk v2 p3) := just_contr (m:=b)
--   -- apply just_ctor_inj
--   refine False.elim (p1 ?_)
--   rfl -- WHAT???
  
  


def W : T -> (T -> Sort _) -> Sort _ | t, P => P t

def tail2 (l:List T): W l (fun i => if !i.isEmpty then T else Unit) :=
  match l with
  | .nil => by unfold W; simp; exact ()
  | .cons t .nil => by unfold W; simp; exact t
  | (.cons _ (.cons a b)) => by exact tail2 (.cons a b)

#eval tail2 [1,2,3]
#eval tail2 ([]:List Unit)


-- set_option pp.proofs true in
-- def eq_is_oeq_wmap (a b : Sort _) : wmap (a = b) (OEq a b) := by
--   refine mkwmap ?_ ?_ ?_
--   {
--     intro i
--     cases i
--     intro _
--     apply id
--   }
--   {
--     intro eq
--     unfold OEq at eq
--     let k := eq (fun i => EQ i a) .rfl
--     dsimp at k
--     let k2 := EQ_to_eq k
--     exact Eq.symm k2
--   }
--   dsimp only [id_eq]
--   intro i
--   cases i
--   rfl
  


def invertible {A:Sort _}{B:Sort _}(f:A->B) := { h:B->A // ∀ i, h (f i) = i }

def inv_to_wmap {f:A->B} : (invertible f) -> (wmap A B) := by
  intro (.mk h eq1)
  exact mkwmap f h eq1
def wmap_to_inv : (w:wmap A B) -> let (.mk (.mk f _) _) := w; (invertible f) := by
  intro (.mk (.mk f h) eq1)
  exact .mk h eq1

example {f k:A->B}{eq1:f = k}: wmap (invertible f) ({ w:wmap A B // w.val.fst = k }) := by
  refine mkwmap ?_ ?_ ?_
  {
    intro (.mk h eq2)
    refine .mk (.mk (.mk f h) ?_) ?_
    exact eq2
    dsimp
    exact eq1
  }
  {
    intro (.mk (.mk (.mk f2 h2) eq3) eq2)
    refine .mk h2 ?_
    dsimp at eq3
    dsimp at eq2
    rw [eq1, <-eq2]
    exact eq3
  }
  intro _
  rfl

def wmap_left_injective (w:wmap A B) : Function.Injective w.val.fst := by
  let (.mk (.mk f h) eq) := w
  exact Function.LeftInverse.injective eq

set_option pp.proofs true in
def wtransp_over_map_strict
  (P:A->Sort _)
  (w:wmap A A)
  {a b:A}
  (eq: ((wtransp w a).val) = ((wtransp w b).val))
: P a -> P b
:= by
  revert P
  let eq2 : ({P : A → Sort _} → P a → P b) = OEq a b := by
    rfl
  rw [eq2]
  rw [oeq_is_eq]
  let eq5 := wmap_left_injective w
  let eq6 := eq5 eq
  exact eq6

set_option pp.proofs true in
def wtransp_over_map
  (P:A->Sort _)
  (w:wmap A B)
  {a:A}
: let (.mk b _) := wtransp w a ; P (w.val.snd b) -> P a
:= by
  let (.mk (.mk f h) eq) := w
  unfold wtransp
  dsimp
  dsimp at eq
  rw [eq]
  apply id


example : (p:List Unit) ++ q = q ++ p := by
  apply wtransp_over_map (fun i => i ++ q = q ++ i) list_nat
  apply wtransp_over_map (fun i => _ ++ i = i ++ _) list_nat
  generalize (list2nat p) = a
  generalize (list2nat q) = b
  unfold list_nat mkwmap
  dsimp
  let h := hmor_append_plus
  unfold hmor2 at h
  dsimp at h
  repeat rewrite [h]
  apply congrArg
  apply Nat.add_comm



def wmap_to_quot (w:wmap A B) : wmap A (@Quot B (fun a b => w.val.snd a = w.val.snd b)) := by
  let (.mk (.mk f h) p) := w
  dsimp at p
  refine Subtype.mk (.mk ?_ ?_) ?_
  {
    intro i
    dsimp
    refine Quot.mk _ ?_
    exact f i
  }
  {
    dsimp
    intro i
    refine Quot.lift ?_ ?_ i
    exact h
    intro _ _ h
    exact h
  }
  {
    dsimp only [id_eq]
    intro _
    apply p
  }

set_option pp.proofs true in
def wmap_to_quot_inv (w:wmap A B) : wmap (@Quot B (fun a b => w.val.snd a = w.val.snd b)) A := by
  let (.mk (.mk f h) p1) := w
  dsimp at p1
  dsimp
  refine .mk (.mk ?_ ?_) ?_
  {
    intro i
    refine Quot.lift h ?_ i
    exact fun a b a => a
  }
  {
    intro a
    exact Quot.mk _ (f a)
  }
  {
    dsimp
    intro i
    let ⟨ _ , p ⟩  := Quot.exists_rep i
    rewrite [<-p]
    apply Quot.sound
    rewrite [p1]
    rfl
  }

set_option pp.proofs true in
def transp_eqn_1 : (wtransp (wmap_to_quot_inv m1) (wtransp (wmap_to_quot m1) k).val).val = k := by
  generalize (wtransp (wmap_to_quot m1) k) = j1
  simp at j1
  let (.mk v1 p) := j1
  dsimp
  rw [<-p]
  rfl

def fun_to_prod_fun (f:A->B->C): PProd A B -> C := fun (.mk a b) => f a b
def fun_to_prod_fun_inv (f:PProd A B -> C): A->B->C := fun a b => f (.mk a b)

def wmap_uncurry_1 : wmap (A->B->C) (PProd A B -> C) := by
  refine mkwmap ?_ ?_ ?_
  exact fun_to_prod_fun
  exact fun_to_prod_fun_inv
  intro f
  unfold fun_to_prod_fun_inv fun_to_prod_fun
  dsimp

def hmor_shl {A:Sort _}{B:Sort _}{op:A->A->A}{opm:B->B->B}{a b:B}(w:wmap A B):
  let (.mk (.mk f h) _) := w;
  ((opm a b) = f (op (h a) (h b))) ->
  (h (opm a b) = op (h a) (h b))
:= by
  let ⟨ (.mk f h), p ⟩ := w
  simp at p; simp
  intro i
  rw [i, p]

def hmor_shr {A:Sort _}{B:Sort _}{op:A->A->A}{opm:B->B->B}{a b:B}(w:wmap A B):
  let (.mk (.mk f h) _) := w;
  (op (h a) (h b) = h (opm a b)) -> 
  (f (op (h a) (h b)) = (opm a b))
:= by
  let ⟨ (.mk f h), p ⟩ := w
  simp at p; simp
  intro i
  rw [i]
  admit

example :
  hmor2 (List.append) (Nat.add) (nat2list)
:= by
  let (.mk k (.intro h p)) := hmor2_exists list_nat List.append
  let x : Nat.add = k := by
    rw [p]
    funext a b
    dsimp
    refine Eq.symm (hmor_shr list_nat ?_)
    let h := hmor_append_plus
    unfold hmor2 at h
    dsimp at h
    apply h
  rw [<-x] at h
  exact h