Preface

About Software Foundation.

• Topics in the series: basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics and so on.
• All for reliable sofware.
• Principal 100% formalized and machine-checked.
• Read inside or alongside an interactive session with Coq.

The Software Foundations series is focused on the mathematical techniques for specifying and resasoning about properties of software and tools for helping validate these properties comparing to other ways which contributes to reliable software so that design philosophies for libraries programming languages design.

Overview

Logic Foundation lays ground work for the other books with basic ideas of funtional programming, constructive logic and the Coq proof assistant.

This volume weaves together three conceptual threads:

1. Basic tools from logic for making and justifying precise claims about programs;
   • Unusual effectiveness of logic in CS
   • Inductive proof - ubitous in all of CS
2. The use of proof assistants to construct rigorous logical arguments;
   • CS contributes to logic ("The flow of ideas between logic and computer science has not been unidirectional")
   • tools of automated theorem provers and hybrid proof assistants.
   • We use Coq in the SF series as it has been a critical enabler for a huge variety of work.
3. functional programming, both as a method of programming that simplifies reasoning about programs and as a bridge between programming and logic.
   • Roots go back to Church's lambda-calculus, which was invented in the 1930s.
   • Basic tenet is that Computation should be pure as much as possible
     • Free from side effects
     • Only effect of exwcution
   • Benefits the understanding and reasonng about the programs.
   • Often much easier to parallelize and pysically distribute.

Reading notes:

Logic Foundation

cunstructors是构造元素，constructor expressions是构造表示，用来描述 constructor 到零个或者多个 constructor 或 constructor expressions 的映射。

Inductive 定义包含了一组 constructor expressions 并赋予名字。

关于自然数的定义，只是表示，你可以使用任何任何其他名字（理解之前的rgb拆开的原因，这样控制 primary 生成的链有限）。

1
2
3

Inductive nat : Type :=
  | O
  | S (n : nat).

A critical point here is that what we've done so far is just to define a representation of numbers: a way of writing them down.The names [O] and [S] are arbitrary, and at this point they have no special meaning -- they are just two different marks that we can use to write down numbers (together with a rule that says any [nat] will be written as some string of [S] marks followed by an [O]). If we like, we can write essentially the same definition this way

Tests

All passed except 3 advanced questions.