mbk/simple-counterexamples
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

all: use standard theorem identifier scheme

Browse source 
https://leanprover-community.github.io/contribute/naming.html
This commit is contained in:
mehbark 2025-04-08 22:13:50 -04:00
parent 3f9948eaf9
commit d914baf772
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
SimpleCounterexamples/FinitudeOfPropositions.lean
View file

@ -1,13 +1,13 @@
-- I actually thought that ∀p, ∃q, (q ≠ p) ∧ q! -- I actually thought that ∀p, ∃q, (q ≠ p) ∧ q!
-- However, propositional extensionality tells us that (p ↔ q) → p = q -- However, propositional extensionality tells us that (p ↔ q) → p = q
theorem finiteTrueProps theorem finite_true_props
: ¬∀p, ∃q, (q ≠ p) ∧ q := by : ¬∀p, ∃q, (q ≠ p) ∧ q := by
intro h intro h
have := h True have := h True
simp at this simp at this
theorem finiteFalseProps theorem finite_false_props
: ¬∀p, ∃q, (q ≠ p) ∧ ¬q := by : ¬∀p, ∃q, (q ≠ p) ∧ ¬q := by
intro h intro h
have := h False have := h False

4
SimpleCounterexamples/RunMEvil.lean
View file

@ -1,8 +1,8 @@
theorem runMEvil theorem runM_evil
(runM : {α : Type} → {m : Type → Type} → [Monad m] → m α → α) : False := (runM : {α : Type} → {m : Type → Type} → [Monad m] → m α → α) : False :=
runM (none : Option Empty) |>.elim runM (none : Option Empty) |>.elim
theorem lawfulRunMEvil theorem lawfulRunM_evil
(runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α) (runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α)
: False := : False :=
runM (none : Option Empty) |>.elim runM (none : Option Empty) |>.elim