Alexander Chichigin gabriel-fallen

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

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

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

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

Инструменты

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

	(* This file is generated by Why3's Coq driver *)
	(* Beware! Only edit allowed sections below *)
	Require Import BuiltIn.
	Require BuiltIn.
	Require HighOrd.
	Require int.Int.
	Require map.Map.

	(* Why3 assumption *)
	Inductive ref (a:Type) :=

	%% Primitive AST->WASM (text format) compiler.

	%% Type =
	%% \| bool
	%% \| int
	%% \| float
	%% \| void

	show_type(bool) = "i32".
	show_type(int) = "i32".

	#! /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) {

	<!DOCTYPE html>
	<html lang="en">
	<head>
	<meta charset="utf-8"/>
	<title>GPU.js — blur</title>
	<script src="gpu-browser.min.js"></script>
	</head>
	<body>
	<input id="image" type="file" accept="image/*">
	<p>Original:</p>

	<!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>

	theory IndGen
	imports Main
	begin

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

	section ‹Summing lists›

	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. *)

	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