Index

_

_ :: _ (the list constructor) _ at _ (tCPA keyword, revisited)

_ in _ (tCPA keyword, revisited) _ semicolon _ (tCPA keyword)

A

addition (associativity) (commutativity) (left identity element) (left neutral element) (right identity element) (right neutral element) Aha! moment

apply (tCPA tactic, revisited)

C

Check (tCPA command, revisited) clear (tCPA keyword, revisited) completeness (of an addition function) (of an equality predicate) (of an equality predicate, the remaining case) Compute (tCPA command, revisited) cons (the list constructor)

Coq tactic (induction, using) Corollary (tCPA keyword, revisited) correspondence (Curry-Howard) coverage (code) (test)

D

Danger, Will Robinson! Definition (tCPA keyword, revisited) denotation

destruct (tCPA tactic, revisited) discriminate (tCPA tactic, revisited) do (tCPA tactic)

E

emacs eqn (tCPA keyword, revisited) equality (functional) (Leibniz) (structural) Euclid's division lemma eureka lemma

ex_intro (tCPA tactic) exact (tCPA tactic, revisited) existential quantifier (exists) exists (among the assumptions) (in the goal) (tCPA tactic, revisited)

F

f_equal (tCPA lemma) fold-left (list) (list, conditional equivalence with fold-right) (nat) fold-right (list) (list, conditional equivalence with fold-left) (nat)

fold-unfold lemmas forall (in the goal)

G

Gallina Gallina keyword (Inductive)

generative AI

I

implicit parameters index (tCPA tactic, revisited) Inductil (the Light of) induction (mathematical) (over Peano numbers, course of values) (over Peano numbers, first order) (over Peano numbers, fourth order) (over Peano numbers, second order) (over Peano numbers, strong) (over Peano numbers, third order) (over Peano numbers, weak) (routine) (structural, for Peano numbers) (structural, for binary trees) (tCPA tactic, revisited) induction hypotheses induction hypothesis (strengthening the) Inductive (Gallina keyword)

injection (tCPA tactic, revisited) intro, with one argument (tCPA tactic, revisited) intros (destructuring -- tCPA tactic, revisited) (with several arguments -- tCPA tactic, revisited) involution involutory function isomorphism (type)

L

lambda-dropped programs (revisited) lambda-dropped proofs lambda-lifted programs (revisited) lambda-lifted proofs left (tCPA tactic, revisited) Lemma (tCPA keyword, revisited)

lists (comparing) (concatenating) (copying) (folding left over) (folding right over) (length) (mapping functions over) (polymorphic) (reversing) (singleton) logical conjunction logical disjunction logical equivalence logical negation

M

modus ponens modus tollens multiplication (associativity) (commutativity) (left absorbing element) (left identity element) (left neutral element) (left-distributivity over addition) (right absorbing element) (right identity element) (right neutral element) (right-distributivity over addition)

muscle memory mystery functions

N

naming conventions nat_ind

nats (folding left over) (folding right over) nil (the empty list)

P

Peano numbers polymorphic data types polymorphic functions polymorphism (etymology) (in Gallina)

Proof (tCPA keyword, revisited) Property (tCPA keyword, revisited) Proposition (tCPA keyword, revisited)

Q

Qed (tCPA keyword, revisited)

quantifier (existential) (universal)

R

referential transparency reflexivity (tCPA tactic, re2visited) (tCPA tactic, revisited) remember (tCPA tactic, revisited) resetting the accumulator Restart (tCPA keyword, revisited)

revert (with one argument -- tCPA tactic, revisited) (with several arguments -- tCPA tactic, revisited) rewrite (tCPA tactic, revisited) right (tCPA tactic, revisited) routine proof

S

Search (tCPA command, revisited) semi-colon (tCPA keyword) simpl (tCPA tactic) soundness (of a unit-test function for addition) (of an addition function) (of an equality predicate) (of an equality predicate, the remaining case)

specification (ambiguous) (satisfying a) (vacuous) split (tCPA tactic, revisited) syntactic sugar

T

tCPA (the Coq Proof Assistant) tCPA command (Check) (Compute) (Search) tCPA constructor (conj) tCPA keyword (... at ...) (... in ...) (Proof) (Qed) (_ semicolon _) (clear) (eqn)

tCPA lemma (f_equal) tCPA tactic (apply) (assert) (case) (compute) (contradiction) (destruct) (discriminate) (do) (ex_intro) (exact) (exists) (induction) (injection) (intro) (intros) (reflexivity) (reflexivity, revisited) (remember) (revert) (rewrite) (simpl) (split) (symmetry) (unfold) Theorem (tCPA keyword, revisited)

U

unfold (tCPA tactic, revisited) uniformity and unity

unit-test functions universal quantifier (forall)

W

WYSIWYG