jorendorff

-- Uniqueness of limits in a metric space.
-- https://www.codewars.com/kata/5ea1f341014f0c0001ec7c5e

import algebra.order
import algebra.ordered_field
import topology.metric_space.basic

def converges_to {X : Type*} [metric_space X] (s : ℕ → X) (x : X) :=
∀ (ε : ℝ) (hε : 0 < ε), ∃ N : ℕ, ∀ (n : ℕ) (hn : N ≤ n), dist x (s n) < ε

jorendorff

-- Formalization of Hofstadter's "TNT" system

import init.data.list

namespace tnt

-- TNT terms and formulas -----------------------------------------------------

inductive term : Type
| zero : term

jorendorff

namespace zfc

universe u

constant set : Type 1
constant is_element_of : set → set → Prop

local notation a `∈` b := is_element_of a b

def is_subset_of (a : set) (b : set) : Prop :=

jorendorff

-- An exercise from _Theorem Proving In Lean_.
-- https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#exercises

namespace expressions
  -- 6. Consider the following type of arithmetic expressions. The idea is that
  --    `var n` is a variable, v_n, and `const n` is the constant whose value
  --    is n.
  inductive aexpr : Type
  | const : ℕ → aexpr
  | var : ℕ → aexpr

jorendorff

-- https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#exercises

-- 6. Consider the following type of arithmetic expressions. The idea is that
--    `var n` is a variable, v_n, and `const n` is the constant whose value
--    is n.
inductive aexpr : Type
| const : ℕ → aexpr
| var : ℕ → aexpr
| plus : aexpr → aexpr → aexpr
| times : aexpr → aexpr → aexpr

jorendorff

"use strict";

Iterator.prototype = {
  *map(mapper) {
    for (let value of this) {
      yield mapper(value);
    }
  },
  ...
};

jorendorff

open nat

theorem my_add_assoc
    -- what we are trying to prove
    : ∀ a b c : nat,
      (a + b) + c = a + (b + c)

-- base case
| 0 b c := by rewrite [
    -- goal is (0 + b) + c = 0 + (b + c)

jorendorff

-- Proof by induction that every natural number is either even or odd.
--
-- I did this after seeing the statement "showing every number is even or odd
-- is easier in binary than in unary, as binary is just unary partitioned by
-- evenness". <https://twitter.com/TaliaRinger/status/1261465453282512896>
--
-- I believe it, but the hidden part of the work is showing that they're the
-- natural numbers and defining addition and multiplication on them.

def is_even (n : ℕ) : Prop := ∃ k, 2 * k = n

jorendorff

details

• Reflect.getOwnPropertyDescriptor(%Iterator.prototype%, "map")
• %Iterator.prototype%.map.length === 1
• %Iterator.prototype%.map.[[Prototype]] is %Generator%
• %Iterator.prototype%.map.prototype
  • is an extensible object
• has no properties

jorendorff

-- Rule of Modus Ponens. The postulated inference rule of propositional
-- calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if 𝜑 is
-- true, and 𝜑 implies 𝜓, then 𝜓 must also be true." This rule is sometimes
-- called "detachment," since it detaches the minor premise from the major
-- premise. "Modus ponens" is short for "modus ponendo ponens," a Latin phrase
-- that means "the mode that by affirming affirms" - remark in [Sanford]
-- p. 39. This rule is similar to the rule of modus tollens mto 176.
--
-- Note: In some web page displays such as the Statement List, the symbols
-- "& " and "⇒ " informally indicate the relationship between the hypotheses