Alexander Chichigin gabriel-fallen

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

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

Инструменты

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

Лично у меня сильный прогресс в английском связан с 3 вещами.

В 7 классе отец заставил меня выписывать английские слова на карточки и учить их. Очень эффективный способ пополнения и поддержания словарного запаса. Теперь для этого принято использовать Anki, хотя я в своё время карточки вырезал из ватмана. :)
В 10-11 классах у нас была очень крутая учительница английского — строго требовала и не стеснялась ставить двойки. Выдала распечатанную табличку со схемами образования разных времён глаголов — лучшее руководство, которое я видел. Жаль, что табличка куда-то потерялась.
Примерно тогда же начал читать книжки на английском. Сначала адаптированные, для чтения в 6-8-10 классе, потом и неадаптированные почитывал. Главное — книги прочитывать. Словарь не обязателен, необязательно понимать 100% текста, можно понимать меньше половины. Если оказалось сильно непонятно &mdash можно тут же начать читать книгу заново, будет намного понятнее, можно сильно незнакомые слова в словаре посмотреть


	-- Addition

	theorem add_comm : ∀ (n m : Int), n + m = m + n := by
	intro n m
	simp [HAdd.hAdd, Add.add]
	match n, m with
	\| Int.ofNat m, Int.ofNat n =>
	simp [Int.add]
	apply Nat.add_comm


	#print List

	/-
	inductive List A where
	\| nil : List A
	\| cons : A -> List A -> List A
	-/

	/-

	namespace ADTs

	/-
	In the game we have two banks of a river: left and right,
	and four characters: a wolf, a goat, a cabbage, and a farmer.
	The farmer prevents abybody from eathing anything, otherweise
	the wolf eats the goat, or the goat eats the cabbage.
	The game starts with all the characters on the left bank and
	the goal is to move everyone to the right bank safe and sound.
	The farmer can carry a single other character at a time

	theory LogEquiv
	imports Main
	begin

	(* NOTATION:
	In Isabelle/HOL we write ‹(A x)› instead of ‹A(x)›
	and ‹∀x. (P x)› instead of ‹∀x: P(x)›
	*)
	lemma "¬(∃x.∀y. (A x) ∧ ¬(B y)) ⟷ (∀x.∃y. (A x) ⟶ (B y))"
	by blast (* Isabelle/HOL can prove this statement automatically all by itself which proves the statement is correct. *)

	theory IndGen
	imports Main
	begin

	(* From "Exercises on Generalizing the Induction Hypothesis" by James Wilcox
	https://jamesrwilcox.com/InductionExercises.html
	*)

	section ‹Summing lists›

	<!DOCTYPE html>
	<html lang="en">
	<head>
	<meta charset="utf-8"/>
	<title>GPU.js ray marching</title>
	<script src="gpu-browser.js"></script>
	</head>
	<body>
	<button id="render">Render!</button>
	<p>Render:</p>

	#! /usr/bin/env Rscript

	input_con <- file("stdin")
	open(input_con)

	prevLine <- ""
	while (length(curLine <- readLines(con = input_con,
	n = 1,
	warn = FALSE)) > 0) {
	if (length(grep("^/home/[^:]+:$", curLine)) > 0) {