Index

_

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

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

A

Abel's lemma (for int-valued functions) (for nat-valued functions) accumulators addition (associativity) (commutativity) (left identity element) (left neutral element) (right identity element) (right neutral element)

Aha! moment apply (tCPA tactic, revisited)

B

binomial coefficients

bisimilarity

C

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

continuations Coq tactic (induction, using) Corollary (tCPA keyword, revisited) correctness (of a unit-test function for addition) correspondence (Curry-Howard) coverage (code) (test)

D

Danger, Will Robinson! Definition (Gallina keyword) (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) equivalence (observational) Euclid's division lemma

Eureka lemma (revisited) 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) Fixpoint (Gallina keyword) fold-left (list) (list, conditional equivalence with fold-right) fold-right (list) (list, conditional equivalence with fold-left)

fold-unfold lemmas forall (in the goal) fundamental theorem of calculus (for int-valued functions) (for nat-valued functions)

G

Gallina Gallina keyword (CoInductive) (Definition) (Fixpoint) (Inductive) (match)

generative AI good style (for ordering the clauses in a match-expression)

H

hockey-stick identity (the)

I

implicit parameters index (tCPA tactic, revisited) Inductil (the Light of) (the Light of, revisited) induction (mathematical) (routine) (structural, for Peano numbers) (structural, for binary trees) (tCPA tactic, revisited) induction hypotheses induction hypothesis (strengthening the) induction principle (over Peano numbers, 1st order) (over Peano numbers, 2nd order) (over Peano numbers, 3rd order) (over Peano numbers, 4th order) (over Peano numbers, 6th order) (over Peano numbers, course of values) (over Peano numbers, strong) (over Peano numbers, tailored) (over Peano numbers, weak) (over Peano numbers, which one to choose) Inductive (Gallina keyword)

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

L

lambda-dropped programs (revisited) lambda-dropped proofs lambda-lifted programs (revisited) lambda-lifted proofs lazy lists 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 (nested) (revisited) (with a flat proof) 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

nil (the empty list)

P

Pascal's rule Pascal's triangle 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) repeat (tCPA tactic) 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) ring (tCPA tactic) routine proof

S

Search (tCPA command, revisited) semi-colon (tCPA keyword) simpl (tCPA tactic) soundness (of a function) (of a program) (of a representation) (of an addition function) (of an equality predicate) (of an equality predicate, the remaining case) specification (ambiguous) (satisfying a) (vacuous) split (tCPA tactic, revisited)

streams subtracting natural numbers (the problem with) summation by parts (for int-valued functions) (for nat-valued functions) summations (over integers) (over natural numbers) (that may start above zero) (that start at one) (that start at zero) syntactic sugar

T

tail calls tCPA (the Coq Proof Assistant) tCPA command (Check) (Compute) (Search) (Show Proof) tCPA constructor (conj) TCPA in essence

tCPA keyword (... at ...) (... in ...) (Proof) (Qed) (_ semicolon _) (clear) (eqn) tCPA lemma (f_equal) tCPA tactic (apply) (assert) (case) (clear) (compute) (contradiction) (destruct) (discriminate) (do) (ex_intro) (exact) (exists) (induction) (injection) (intro) (intros) (reflexivity) (reflexivity, revisited) (remember) (repeat) (revert) (rewrite) (ring) (simpl) (split) (symmetry) (unfold) Theorem (tCPA keyword, revisited)

U

unfold (tCPA tactic, revisited) uniformity and unity

unit-test functions universal quantifier (forall)

W

WYSIWYG