avigad

/-
Notes on dependent type theory and Lean's formal foundation
Jeremy Avigad
Hausdorff School: Formal Mathematics and Computer-Assisted Proving
September 18 - 22, 2023
https://tinyurl.com/bonn-dtt
-/

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Basic

avigad

import Init

/- Facts about Nat -/

theorem Nat.le_refl (a : Nat) : a ≤ a := sorry
theorem Nat.le_trans {a b c : Nat} : a ≤ b → b ≤ c → a ≤ c := sorry
theorem Nat.lt_trans {a b c : Nat} : a < b → b < c → a < c := sorry
theorem Nat.le_of_lt {a b : Nat} : a < b → a ≤ b := sorry
theorem Nat.not_le_of_lt {a b : Nat} : a < b → ¬ b ≤ a := sorry
theorem Nat.le_of_not_le {a b : Nat} : ¬ a ≤ b → b ≤ a := sorry

avigad

/- By JA, with improvements by Floris van Doorn. -/
import data.matrix.notation tactic.ring

namespace finset

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w} [comm_monoid β]

open_locale big_operators

avigad

import tactic
open_locale classical

#check 2
#check 2 + 2

#check 2 + 2 = 4

#check (2.05 : real)

avigad

import tactic
open classical

/-
Cheat sheet:

to prove `p → q`, use `intro h`
to use `h : p → q`, use `apply h`

to prove `p ∧ q`, use `split`

avigad

/-
Experimenting with unbundled classes.
Author: Jeremy Avigad

Definitions are in the namespace "experiment" to avoid clashing with definitions in init.
-/
namespace experiment

/-
Calculation lemmas for multiplicative notation.

avigad

/-
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad

The mutilated chessboard problem.

Consider an eight-by-eight chessboard and a set of dominos with the property that each domino
can cover exactly two adjacent chessboard squares. Remove the bottom left and top right corners.
The *mutilated chessboard problem* asks whether it is possible to cover the remaining squares

avigad

import tactic.tauto tactic.finish

section

variables {A B C D : Prop}

example (h1 : A ∨ B) (h2 : ¬ A) : B :=
or.elim h1
  (assume h3 : A, 
    have h4 : false, from h2 h3,

avigad

import data.fintype tactic.ring

structure graph :=
(vertex : Type*)
(edge   : vertex → vertex → bool)

namespace graph

class undirected (G : graph) :=
(symm : ∀ x y : G.vertex, G.edge x y = G.edge y x)

avigad

import data.finset data.nat.choose

variables {α : Type*} [decidable_eq α]

namespace finset

/-
`insert_empty_eq_singleton` in the library should be replaced by this.
-/
theorem insert_empty_eq_singleton' (a : α) : insert a ∅ = finset.singleton a := rfl