Ramdom notes on Recursion Function, Curry-Howard isomorphism, etc..

(1) Reasoning about structural recursive functions naturally relies on a proof by induction on the principle argument of these functions and thus follows the structure of pattern matching constructs present in these functions

(2) According to the Curry-Howard isomorphism, the fact that a type is empty or not can carry logical information: The type represents a false or true formula.

(3) Natural numbers provide a simple recursion structure that often plays a role in problems of data size or combinatorics. Integers provide a clear algebraic structure, the ring structure, and are based on a binary encoding that supports efficient implementations of the most basic operations. Real numbers are given by a set of axioms. The definitional approach does not make it possible to obtain a type of real numbers with the usual notion of equality. For these three kind of numbers, a total order is also provided.

(4) The Coq system also provides a language called Ltac to define new tactics. Thanks to this language, we can write tactics with arguments without needing to master the internal structure of the proof engine. The Ltac engine is original in the control structures it provides; however, it provides no data structures. All this makes this programming language quite exotic. Ltac is quite recent and its syntax and semantics are probably unstable. Still, we can program very concise proof search algorithms, sometimes with functions whose termination is not ensured.