Alexander Chichigin gabriel-fallen

## int_lemmas.lean

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

## examples.lean

#print List

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

/-

## adts.lean
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

## LogEquiv.thy
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. *)

## IndGen.thy
theory IndGen
  imports Main
begin

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

section ‹Summing lists›

## proofs.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              1 star
            
          
                gabriel-fallen
                / proofs.md
            
            
              Last active
              January 29, 2022 13:53
                — forked from suhr/proofs.md
            
          
    Упражнения по формальным доказательствам

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

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

  
## gpu_march.html
<!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>

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

## english.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                gabriel-fallen
                / english.md
            
            
              Created
              April 2, 2020 09:52
            
              
                Про изучение английского
              
          
    Лично у меня сильный прогресс в английском связан с 3 вещами.


В 7 классе отец заставил меня выписывать английские слова на карточки и учить их. Очень эффективный способ пополнения и поддержания словарного запаса. Теперь для этого принято использовать Anki, хотя я в своё время карточки вырезал из ватмана. :)


В 10-11 классах у нас была очень крутая учительница английского — строго требовала и не стеснялась ставить двойки. Выдала распечатанную табличку со схемами образования разных времён глаголов — лучшее руководство, которое я видел. Жаль, что табличка куда-то потерялась.


Примерно тогда же начал читать книжки на английском. Сначала адаптированные, для чтения в 6-8-10 классе, потом и неадаптированные почитывал. Главное — книги прочитывать. Словарь не обязателен, необязательно понимать 100% текста, можно понимать меньше половины. Если оказалось сильно непонятно &mdash можно тут же начать читать книгу заново, будет намного понятнее, можно сильно незнакомые слова в словаре посмотреть


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

	-- 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) {