Skip to content

Instantly share code, notes, and snippets.

View ice1000's full-sized avatar
♾️
Generalizing something

Tesla Zhang‮ ice1000

♾️
Generalizing something
3.9k followers · 726 following
View GitHub Profile
@ice1000
ice1000 / unsubscribe.py
Last active September 11, 2024 03:21
My take on unsubscription automation of Deadline Hollywood, Variety Breaking News, and Billboard, inspired from the scripts by Alex Chi and Felix Yan
from email.parser import HeaderParser
import imaplib
import time
import requests
from concurrent.futures import ThreadPoolExecutor, as_completed
imaplib._MAXLINE = 40000000
ONE_TIME_LIMIT = 10
mailparser = HeaderParser()
@ice1000
ice1000 / Brozozowski.agda
Last active June 3, 2024 20:56
OPLSS 2024
open import Data.Bool.Base
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Nullary
module _ (A : Set) (dec : (a b : A) → Dec (a ≡ b)) where
record DFA (S : Set) : Set where
field F : S → Bool
field t : A -> S -> S
data RE : Set where
@ice1000
ice1000 / ThisSucks.agda
Created February 23, 2024 18:39
This version of + sucks
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat using (Nat; suc; zero)
cong : (f : Nat → Nat) → ∀ {a b} → a ≡ b → f a ≡ f b
cong f refl = refl
trans : ∀ {a b c : Nat} → a ≡ b → b ≡ c → a ≡ c
trans refl p = p
sym : ∀ {a b : Nat} → a ≡ b → b ≡ a
sym refl = refl
@ice1000
ice1000 / Parth.ard
Created February 14, 2024 02:29
Seemingly impossible functional program
\import Data.Bool
\import Data.List
\import Logic.Meta
\import Paths
\func CoNat =>
\Sigma (f : Nat -> Bool)
(\Pi (i : _) -> f i = false -> f (suc i) = false)
\where {
\func blt (n m : Nat) : Bool
@ice1000
ice1000 / Agda-report.agda
Last active February 3, 2024 18:19
Not so secret
module PSet3 where
record TermStructure : Set₁ where
field
Term : Set
module QPER (TS TS' : TermStructure) where
open TermStructure TS
open TermStructure TS'
renaming (Term to Term')
@ice1000
ice1000 / CoqNatUIP.v
Last active January 19, 2024 09:06
UIP on Nat in Coq
Definition lemma {n m : nat} (p : n = m) : pred n = pred m := f_equal pred p.
Definition lemma2 {n m : nat} (p : n = m) : S n = S m := f_equal S p.
Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p
:= match p with | eq_refl => eq_refl end.
(* Definition bruh {n} (a : nat) (p : S n = a) : Prop.
Proof.
destruct a.
- exact True.
- exact (@lemma2 n a (@lemma (S n) (S a) p) = p).
@ice1000
ice1000 / LightQuantum.v
Last active January 3, 2024 09:30
A proof that inductive-inductive even is equivalent to directly defined even
Inductive nat: Type :=
| S (n: nat)
| O.
Inductive even: nat -> Prop :=
| Base: even O
| Ind: forall n, even n -> even (S (S n)).
Inductive ev: nat -> Prop :=
| ev_Base: ev O
@ice1000
ice1000 / N-add-comm-lf.agda
Last active April 23, 2024 02:53
Purely axiomatic proof of +-comm on nat in extensional type theory
variable
A B : Set
postulate
Eq : A → A → Set
refl : (a : A) → Eq a a
rw : {x y : A} → Eq x y → (B : A → Set) → B x → B y
-- UIP missing but not needed
N : Set
Z : N
S : N → N
@ice1000
ice1000 / List-rev-ind.agda
Created September 7, 2023 12:33
Answering someone's question from WeChat
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
open import Cubical.Data.List
private variable X : Type
rev-ind : (P : List X → Type)
→ P []
→ (∀ x xs → P xs → P (xs ∷ʳ x))
@ice1000
ice1000 / Int.agda
Last active August 7, 2023 14:06
Useless code
{-# OPTIONS --cubical #-}
open import Cubical.Data.Int
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.SetTruncation
-- Maps out of a set-truncated int can only target sets,
-- yet it's equivalent to the normal int