Kata Library: Coq Practice
Sign Up
Time to claim your honor
Training
Practice
Complete challenging
Kata
to earn honor and ranks. Re-train to hone technique
Freestyle Sparring
Take turns remixing and refactoring others code through
Kumite
Community
Leaderboards
Achieve honor and move up the global leaderboards
Chat
Join our
Discord
server and chat with your fellow code warriors
Discussions
View our
Github Discussions
board to discuss general Codewars topics
About
Docs
Learn about all of the different aspects of Codewars
Blog
Read the latest news from Codewars and the community
Log In
Sign Up
Library
Collections
Newest
Oldest
Popularity
Positive Feedback
Most Completed
Least Completed
Hardest
Easiest
Name
Relevance
Low Satisfaction
All
My Languages
Agda (Beta)
BF (Beta)
C
CFML (Beta)
Clojure
COBOL (Beta)
CoffeeScript
CommonLisp (Beta)
Coq
C++
Crystal
C#
D (Beta)
Dart
Elixir
Elm (Beta)
Erlang (Beta)
Factor (Beta)
Forth (Beta)
Fortran (Beta)
F#
Go
Groovy
Haskell
Haxe (Beta)
Idris (Beta)
Java
JavaScript
Julia (Beta)
Kotlin
λ Calculus (Beta)
Lean
Lua
NASM
Nim (Beta)
Objective-C (Beta)
OCaml (Beta)
Pascal (Beta)
Perl (Beta)
PHP
PowerShell (Beta)
Prolog (Beta)
PureScript (Beta)
Python
R (Beta)
Racket
Raku (Beta)
Reason (Beta)
RISC-V (Beta)
Ruby
Rust
Scala
Shell
Solidity (Beta)
SQL
Swift
TypeScript
VB (Beta)
Approved & Beta
Approved
Beta
All
Kata I have not trained on
Kata I have not completed
Kata I have completed
8 kyu
easiest
7 kyu
6 kyu
5 kyu
4 kyu
3 kyu
2 kyu
1 kyu
hardest
Algorithms
1
Discrete Mathematics
1
Fundamentals
6
Logic
10
Mathematics
2
Theorem Proving
9
FEATURED TAGS
Cryptography
Data Science
Debugging
Games
Tutorials
10 Kata Found
6 kyu
Conversion to Negation Normal Form
21
malcolmsharpe
Logic
Theorem Proving
Beta
From Hilbert to Gentzen, and back
5
dramforever
Status:
Ranking feedback needed
Estimated Rank:
3 kyu
Logic
Theorem Proving
6 kyu
Is nat equal to bool?
100
dramforever
Theorem Proving
Logic
Fundamentals
Beta
Induction toolbox: Generalized m-induction
8
donaldsebleung
Status:
Ranking feedback needed
Estimated Rank:
6 kyu
Theorem Proving
Logic
Mathematics
Discrete Mathematics
7 kyu
Yet another random fact about filtering
39
donaldsebleung
Theorem Proving
Logic
Fundamentals
7 kyu
Another random fact about filtering
40
donaldsebleung
Theorem Proving
Logic
Fundamentals
8 kyu
Triple negation
206
khanh93
1 Issue Reported
Logic
Fundamentals
5 kyu
But WHY is LEM unprovable?
24
dramforever
Logic
Theorem Proving
Fundamentals
6 kyu
Duality in Boolean logic
56
dramforever
Theorem Proving
Logic
Fundamentals
5 kyu
EM implies LPO, LPO implies LLPO
81
solitude
Theorem Proving
Mathematics
Logic
Algorithms
Confirm
Collect:
undefined
Loading collection data...