Сухарик suhr

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.

How to use Nix Flakes system wide

There are some articles you want to read first:

Nix Flakes is currently an experimental feature, so this tutorial assumes that you are using the unstable channel.

Why so slow? Creating a flamegraph of your program with perf

Flamegraphs can help to optimize the program a lot. So let's create one!

Install perf with use flag unwind enabled
Download flamegraph.pl and stackcolllapse-perf.pl
Run perf record -F 99 --call-graph dwarf -- ‹your program›
Do all the things that make your program slow
Close your program
Run perf script | stackcollapse-perf.pl > out.folded

	s:+: ConjugateAdd :g
	s:-: NegateSubtract :g
	s:×: SignMultiply :g
	s:÷: ReciprocalDivide :g
	s:⋆: ExponentialPower :g
	s:√: SquareRootRoot :g
	s:⌊: FloorMinimum :g
	s:⌈: CeilingMaximum :g
	s:∧: SortUpAnd :g
	s:∨: SortDownOr :g

	s:∘.: outerProduct_ :g
	s:+: ConjugatePlus :g
	s:-: NegateMinus :g
	s:×: DirectionTimes :g
	s:÷: ReciprocalDivide :g
	s:⌊: FloorMinimum :g
	s:⌈: CeilingMaximum :g
	s:\|: MagnitudeResidue :g
	s:*: ExponentialPower :g
	s:⍟: NatualLogarithmLogarithm :g

	# SSE to BQN dictonary

	# This is an implementation of SSE SIMD intristics in BQN. The purpose of it
	# is understanding: it's a look at SIMD instructions from an array programmer POV.

	# There are limit of what you can can represent in a programming language without
	# losing clarity. Bit hackery is one of such features. So instead of converting
	# from floats to bits and back, we just assume that the data already is
	# represented the way we need.

	# APL keyboard
	<Multi_key> <space> <z> : "⊂"
	<Multi_key> <space> <Z> : "⊆"
	<Multi_key> <space> <x> : "⊃"
	<Multi_key> <space> <c> : "∩"
	<Multi_key> <space> <v> : "∪"
	<Multi_key> <space> <b> : "⊥"
	<Multi_key> <space> <n> : "⊤"
	<Multi_key> <space> <less> : "⍝"
	<Multi_key> <space> <comma> : "⍪"

	{
	PendingTask \| EndedTask \| WaitingTask \| RecurringParrentTask \| RecurringChildTask
	...
	}

	Task :: {
	status: Status
	uuid: Uuid
	entry: Date
	description: string