The critical new ideas arepolymorphism (abstracting functions over the types of the data they manipulate) andhigher-order fu...

Pair of NumbersQ: Why name inductive?A: Inductive means building things bottom-up, it doesn’t have to self-referencial (recur...

apply exactly the same as some hypothesis can be used to finish a proof (shorter than rewrite then reflexivity) It also work...

We have seen… propositions: factual claims equality propositions (e1 = e2) implications (P → Q) quantified propositions (∀ x...

Inductively Defined Propositions The 3rd way to state Evenness…Besides: 123Theorem even_bool_prop : ∀n, evenb n = true ↔ ∃k...

useful as env Map == Dictionary building data structure. use of reflection to streamline proofs. Two flavors of...

“Algorithms are the computational content of proofs.” —Robert Harper So the book material is designed to be gradually revea...

relation 与injective/surjective/bijective function 等相关的知识在 5. Tactics 里，为了避免每次都要 grep 我在这里写一下。 RelationsRecalling ...

Basic 每次我们使用 Inductive 来声明数据类型时，Coq 会自动为这个类型生成 _归纳原理_。Every time we declare a new Inductive datatype, Coq automatically gener...

123456Z ::= X;;Y ::= 1;;WHILE ~(Z = 0) DO Y ::= Y * Z;; Z ::= Z - 1END A weird convention through out all IMP is: a-: ari...