Skip to content

Instantly share code, notes, and snippets.

@lovely-error

lovely-error/ln.lean

Created August 7, 2024 19:13
Show Gist options
  • Save lovely-error/82e83e68ddf9454038988ca1dc153cdc to your computer and use it in GitHub Desktop.
Save lovely-error/82e83e68ddf9454038988ca1dc153cdc to your computer and use it in GitHub Desktop.
Download ZIP
what the hell..
Raw
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 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_general {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_general2 {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_general3 {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]
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 :
List.append (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_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_general3 list_int @fmap_append_plus2 (a:=a1) (b:=a2)
rw [List.append_eq, List.append_eq, x1]
let x2 := fmap_general3 list_int @fmap_append_plus2 (a:=a2) (b:=a1)
rw [x2]
rw [Nat.add_comm]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment