Skip to content

Instantly share code, notes, and snippets.

View lengyijun's full-sized avatar
🦄

lyj lengyijun

🦄
70 followers · 152 following
View GitHub Profile
@lengyijun
lengyijun / weak_Collatz_conjecture_42_3.txt
Created November 14, 2024 00:32
; https://terrytao.wordpress.com/2011/08/25/the-collatz-conjecture-littlewood-offord-theory-and-powers-of-2-and-3/
blank_symbol: #
initial_state: bootstrap_stage_1
bootstrap_stage_1
# 1 R bootstrap_stage_2
0 0 R unreachable
1 1 R unreachable
@lengyijun
lengyijun / weak_Collatz_conjecture_45_3.txt
Created November 13, 2024 00:30
; https://terrytao.wordpress.com/2011/08/25/the-collatz-conjecture-littlewood-offord-theory-and-powers-of-2-and-3/
blank_symbol: #
initial_state: bootstrap_stage_1
bootstrap_stage_1
# 1 R cp_stage_5
0 0 R unreachable
1 1 R unreachable
@lengyijun
lengyijun / list27.txt
Last active October 16, 2024 09:47 — forked from anonymous/list27.txt
000(023Rb|001Rb)
001(017La|002Rb) find 1
002(021La|003Rb) find 2
003(021La|004La) place c2
004(009Rb|005Lb)
005(004Ra|005La) 向左找到 0, 1 -> 0
006(008La|007La)
007(009Rb|007La) 向左找到 0, 重写成 0
008(009Ra|008La) 向左找到 0, 重写成 0
009(010Ra|026Ra)
@lengyijun
lengyijun / dnscrypt-proxy.md
Last active September 22, 2022 02:19 — forked from ndlrx/dnscrypt-proxy.md
Install dnscrypt-proxy on Archlinux or Manjaro

Step 1 - Install and Configure dnscrypt-proxy

sudo su
pacman -S dnscrypt-proxy

cd /etc/dnscrypt-proxy/
@lengyijun
lengyijun / learn_record.v
Last active July 15, 2022 11:53
Require Import
Coq.FSets.FMapAVL
Coq.FSets.FMapFacts
Coq.Structures.OrderedTypeEx
PeanoNat.
Module Import M := FMapAVL.Make(Nat_as_OT).
Print Module M.
Check (M.t (list nat)).
@lengyijun
lengyijun / mergesort.v
Created June 5, 2022 13:55
Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.
Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
match x with
| x1 :: xs =>
match y with
| y1 :: ys => if x1 <=? y1
then x1::(merge xs y)
@lengyijun
lengyijun / hello.v
Created May 28, 2022 10:39
try Program Fixpoint
Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.
Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
match x with
| x1 :: xs =>
match y with
| y1 :: ys => if x1 <? y1
then x1::(merge xs y)
@lengyijun
lengyijun / mutual-merge.agda
Created April 24, 2022 05:49
open import Data.String as String using (String; fromList)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
open import Data.Nat.Properties
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.List hiding (merge; partition)
open import Data.List.Properties using (map-id; map-compose)
open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; map)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
@lengyijun
lengyijun / Merge.v
Created April 20, 2022 04:11
recursive induction
(** * Merge: Merge Sort, With Specification and Proof of Correctness*)
From VFA Require Import Perm.
From VFA Require Import Sort.
From Coq Require Import Recdef. (* needed for [Function] feature *)
(** Mergesort is a well-known sorting algorithm, normally presented
as an imperative algorithm on arrays, that has worst-case
O(n log n) execution time and requires O(n) auxiliary space.
@lengyijun
lengyijun / merge.v
Last active April 19, 2022 15:48
length decrease version
(** * Merge: Merge Sort, With Specification and Proof of Correctness*)
From VFA Require Import Perm.
From VFA Require Import Sort.
From Coq Require Import Recdef. (* needed for [Function] feature *)
(** Mergesort is a well-known sorting algorithm, normally presented
as an imperative algorithm on arrays, that has worst-case
O(n log n) execution time and requires O(n) auxiliary space.