This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open tactic | |
open smt_tactic | |
meta def blast : tactic unit := using_smt $ intros >> try simp >> try eblast | |
notation `♮` := by abstract { blast } | |
universe variables u v | |
structure Category := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
universes u v | |
variables {ι : Type u} {α : Type v} | |
/- the usual definitions of indexed union and intersection -/ | |
def Union (s : ι → set α) : set α := { a | ∃ i, a ∈ s i } | |
def Inter (s : ι → set α) : set α := { a | ∀ i, a ∈ s i } | |
notation `⋃` binders `, ` r:(scoped f, Union f) := r | |
notation `⋂` binders `, ` r:(scoped f, Inter f) := r |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import tactic | |
open_locale classical | |
#check 2 | |
#check 2 + 2 | |
#check 2 + 2 = 4 | |
#check (2.05 : real) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- 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 |
OlderNewer