From 22cac47a7629888506e25334efdf90e717fc8975 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 19 Nov 2022 01:49:58 -0600
Subject: [PATCH] lol

---
 src/Crypto/RSA.agda     | 36 +++++++++++++++++
 src/Crypto/RSA/Nat.agda | 39 ++++++++++++++++++
 src/Lemma641.agda       | 88 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 163 insertions(+)
 create mode 100644 src/Crypto/RSA.agda
 create mode 100644 src/Crypto/RSA/Nat.agda
 create mode 100644 src/Lemma641.agda

diff --git a/src/Crypto/RSA.agda b/src/Crypto/RSA.agda
new file mode 100644
index 0000000..0a82c8f
--- /dev/null
+++ b/src/Crypto/RSA.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --cubical #-}
+
+module Crypto.RSA where
+
+open import Agda.Builtin.Cubical.Path
+open import Crypto.RSA.Nat
+
+refl : {A : Set} {x y : A} → x ≡ y
+refl {A} {x} {y} i = x
+
+data Σ (A : Set) (B : A → Set) : Set where
+  ⟨_,_⟩ : (x : A) → B x → Σ A B
+
+∃ : ∀ {A : Set} (B : A → Set) → Set
+∃ {A} B = Σ A B
+
+∃-syntax = ∃
+syntax ∃-syntax (λ x → B) = ∃[ x ] B
+
+record divides (d n : ℕ) : Set where
+  constructor mkDivides
+  field
+    p : ∃[ m ] (d * m ≡ n)
+
+-- doesDivide : (d n : ℕ) → Dec (divides d n)
+-- doesDivide zero n = yes refl
+-- doesDivide (suc d) n = ?
+
+record prime (n : ℕ) : Set where
+  constructor mkPrime
+  field
+    p : ∀ (x y : ℕ) → ¬ (x * y ≡ n)
+
+isPrime : (n : ℕ) → Dec (prime n)
+isPrime zero = ?
+isPrime (suc n) = ?
diff --git a/src/Crypto/RSA/Nat.agda b/src/Crypto/RSA/Nat.agda
new file mode 100644
index 0000000..74ee5e3
--- /dev/null
+++ b/src/Crypto/RSA/Nat.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --cubical #-}
+
+module Crypto.RSA.Nat where
+
+open import Agda.Builtin.Cubical.Path
+
+infixl 6 _+_
+infixl 7 _*_
+
+data Bool : Set where
+  true : Bool
+  false : Bool
+
+record ⊥ : Set where
+
+¬_ : Set → Set
+¬ x = ⊥
+
+data Dec (A : Set) : Set where
+  yes : A → Dec A
+  no : ¬ A → Dec A
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+{-# BUILTIN NATURAL ℕ #-}
+
+data Fin : ℕ → Set where
+  zero : {n : ℕ} → Fin (suc n)
+  suc : {n : ℕ} → (i : Fin n) → Fin (suc n)
+
+_+_ : ℕ → ℕ → ℕ
+zero + y = y
+suc x + y = suc (x + y)
+
+_*_ : ℕ → ℕ → ℕ
+zero * y = zero
+suc x * y = y + x * y
diff --git a/src/Lemma641.agda b/src/Lemma641.agda
new file mode 100644
index 0000000..0b473e7
--- /dev/null
+++ b/src/Lemma641.agda
@@ -0,0 +1,88 @@
+{-# OPTIONS --cubical #-}
+
+module Lemma641 where
+
+open import Level
+open import Cubical.Foundations.Prelude 
+  using (_≡_; refl; _∙_; _≡⟨⟩_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Foundations.Equiv using (isEquiv; equiv-proof)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.Core using (Rel)
+
+_≢_ : {ℓ : Level} {A : Set ℓ} → Rel A ℓ
+x ≢ y = ¬ x ≡ y
+
+data S¹ : Set where
+  base : S¹
+  loop : base ≡ base
+
+data Bool : Set where
+  true : Bool
+  false : Bool
+
+bool-id : Bool → Bool
+bool-id true = true
+bool-id false = false
+
+bool-id≡bool : (b : Bool) → bool-id b ≡ b
+bool-id≡bool true _ = true
+bool-id≡bool false _ = false
+
+bool-id-is-equiv : isEquiv bool-id
+bool-id-is-equiv .equiv-proof y .fst = ( y , bool-id≡bool y )
+bool-id-is-equiv .equiv-proof y .snd (y′ , p) i = let b = p (~ i) in (? , bool-id≡bool y)
+
+bool-flip : Bool → Bool
+bool-flip true = false
+bool-flip false = true
+
+f : {A : Set} (x : A) → (p : x ≡ x) → S¹ → A
+f x p base = x
+f x p (loop i) = p i
+
+refl-base : base ≡ base
+refl-base = refl
+
+refl-x : {A : Set} → (x : A) → x ≡ x
+refl-x _ = refl
+
+-- p : x ≡ x
+-- p : PathP (λ _ → A) x x
+-- p : I → A
+
+-- f : S¹ → A
+-- loop : I → S¹
+-- λ i → f (loop i) : I → A
+
+-- f : S¹ → A
+-- refl-base : base ≡ base
+-- refl-base : I → S¹
+-- λ i → f (refl-base i) : I → A
+
+-- refl-x : x ≡ x
+-- refl-x : I → A
+
+-- p ≡ refl : I → (I → A)
+
+types-arent-sets : {A : Set} (x : A) → (p : x ≡ x) → p ≡ refl → ⊥
+types-arent-sets x p p≡refl = ?
+
+-- This is the consequence of loop ≡ refl, which says that for any p : x ≡ x, it
+-- also equals refl. It is then used with a proof that p ≡ refl → ⊥
+consequence : {A : Set} (x : A) → (p : x ≡ x) → loop ≡ refl → p ≡ refl
+consequence x p loop≡refl = p
+  ≡⟨ refl ⟩
+    (λ i → f x p (loop i))
+  ≡⟨ cong (λ l i → f x p (l i)) loop≡refl ⟩
+    (λ i → f x p (refl-base i))
+  ≡⟨ refl ⟩
+    refl-x x
+  ∎
+
+lemma641 : loop ≢ refl
+lemma641 x = ?
+
+-- https://serokell.io/blog/playing-with-negation
+
+-- f : {A : Set} (x : A) → (p : x ≡ x) → (S¹ → A)