Basics.v

Coq, interactive theorem prover, functional programming, Gallina, type, expression, Compute command, type definition syntax, type constructors, enumerated types, function definition syntax, infix notation, pattern matching, booleans, conditionals, parametrized types, tuple types, examples (proof), proof syntax, reflexivity tactic, simpl tactic, assertion syntax, modules, module syntax, natural numbers, nat type, expression evaluation syntax, arrow types, same type parameters idiom, recursive function definition syntax, infix notation options, algebraic data types, propositions, proof by simplification, universal quantifier, proof goals, intro tactic, assumptions, proof context, proposition keywords: {theorem, lemma, fact, example, remark}, proof by rewriting, tactics, rewrite tactic, admitted command, check command, abort command, proof by case analysis, destruct tactic, rewrite with theorem, eqn annotation, intro pattern, bullets, subgoals, notation scope, precedence, associativity, fixpoints, structural recursion, termination requirement, multiple cases sugaring, nested case sugaring, unfolding

Shows how to use simpl and reflexivity.

Same as above.

Shows how to define a fixpoint function.

Introducing the intros tactic, for variables and hypotheses.

Shows to use/invoke theorems in proofs using rewrite.

Shows how to use destruct for case analysis. This was a bit tricky before I realized how to step one tactic at a time. You destruct two times. When encountering a contradiction, use it to rewrite.

The problem was to write a recursive function that terminates on all inputs but gets rejected by Coq’s unsophisticated automatic analysis of decreasing arguments.

Answer:

Fixpoint summation (i : nat) (n : nat) : nat :=
  if i =? n
  then n
  else i + (summation (i+1) n).

Wow, it’s actually interesting how Coq is unable to analyze this simple function as decreasing! They should borrow Why3’s variant keyword - n - i is strictly decreasing. In Why3, you’d have to include this variant keyword or else Why3 would complain about the function not being proved as terminating.

Straightforward.

Suppose a course has a grading policy based on late days.

A student’s letter grade is lowered if they submit too many HW assignments late.

We have a letter datatype, modeling the grade. We have a modifier type, which modifies a letter grade. For example, we can have a Natural A, which is a plain grade of A. There’s also Plus A, Minus A.

A grade is then just a letter and a modifier. We also create a enumerated type comparison.

Inductive letter : Type :=
  | A | B | C | D | F.
Inductive modifier : Type :=
  | Plus | Natural | Minus.
Inductive grade : Type :=
  Grade (l:letter) (m:modifier).
Inductive comparison : Type :=
  | Eq         (* "equal" *)
  | Lt         (* "less than" *)
  | Gt.        (* "greater than" *)

This is a straightforward comparison function for letter grades. What’s notable though, is the syntactic sugar for two cases at once:

(** As another shorthand, we can also match one of several
    possibilites by using [|] in the pattern.  For example the pattern
    [C , (A | B)] stands for two cases: [C, A] and [C, B]. *)

Definition letter_comparison (l1 l2 : letter) : comparison :=
  match l1, l2 with
  | A, A => Eq
  | A, _ => Gt
  | B, A => Lt
  | B, B => Eq
  | B, _ => Gt
  | C, (A | B) => Lt
  | C, C => Eq
  | C, _ => Gt
  | D, (A | B | C) => Lt
  | D, D => Eq
  | D, _ => Gt
  | F, (A | B | C | D) => Lt
  | F, F => Eq
  end.

And we also have a modifier comparison.

Definition modifier_comparison (m1 m2 : modifier) : comparison :=
  match m1, m2 with
  | Plus, Plus => Eq
  | Plus, _ => Gt
  | Natural, Plus => Lt
  | Natural, Natural => Eq
  | Natural, _ => Gt
  | Minus, (Plus | Natural) => Lt
  | Minus, Minus => Eq
  end.

We define lower_letter - a function that lowers a letter grade. It’s just simple pattern matching.

Definition lower_letter (l : letter) : letter :=
  match l with
  | A => B
  | B => C
  | C => D
  | D => F
  | F => F  (* Can't go lower than [F]! *)
  end.

Destructing a letter gives you five possible options.

We define a comparison function for grades. The resulting ordering is called “lexicographic ordering”.

A hint is given - match g1 and g2 simultaneously but don’t “enumerate all the cases” – do case analysis on letter​_comparison call.

Interesting things: reflexivity should quickly prove a “unit test” of a function. Nested match expression – the inner one doesn’t end with a dot. It seems periods close a full term.

This was the most fun proof so far! There was a lot of strategic destructs, simplifications, and rewrites. We also used previous theorems.

This “unfolding” technique is quite important.

(** Sometimes it is useful to be able to "unfold" a definition to be
    able to make progress on a proof.  Soon, we will see how to do this
    in a much simpler way automatically, but for now, it is easy to prove
    that a use of any definition like [apply_late_policy] is equal to its
    right hand side just by using reflexivity.

    This result is useful because it allows us to use [rewrite] to
    expose the internals of the definition. *)
Theorem apply_late_policy_unfold :
  forall (late_days : nat) (g : grade),
    (apply_late_policy late_days g)
    =
    (if late_days <? 9 then g  else
       if late_days <? 17 then lower_grade g
       else if late_days <? 21 then lower_grade (lower_grade g)
            else lower_grade (lower_grade (lower_grade g))).
Proof.
  intros. reflexivity.
Qed.

Same thing as above.

We are given this background:

(** **** Exercise: 3 stars, standard (binary)

    We can generalize our unary representation of natural numbers to
    the more efficient binary representation by treating a binary
    number as a sequence of constructors [B0] and [B1] (representing 0s
    and 1s), terminated by a [Z]. For comparison, in the unary
    representation, a number is a sequence of [S] constructors terminated
    by an [O].

    For example:

        decimal               binary                          unary
           0                       Z                              O
           1                    B1 Z                            S O
           2                B0 (B1 Z)                        S (S O)
           3                B1 (B1 Z)                     S (S (S O))
           4            B0 (B0 (B1 Z))                 S (S (S (S O)))
           5            B1 (B0 (B1 Z))              S (S (S (S (S O))))
           6            B0 (B1 (B1 Z))           S (S (S (S (S (S O)))))
           7            B1 (B1 (B1 Z))        S (S (S (S (S (S (S O))))))
           8        B0 (B0 (B0 (B1 Z)))    S (S (S (S (S (S (S (S O)))))))

    Note that the low-order bit is on the left and the high-order bit
    is on the right -- the opposite of the way binary numbers are
    usually written.  This choice makes them easier to manipulate. *)

The task was to define an increment function incr and a conversion function bin_to_nat.

For bin_to_nat, I had to define pow and use a helper function bin_to_nat'.

When doing the factorial exercise, I defined factorial as such:

Fixpoint factorial (n:nat) : nat :=
  match n with
  | 0 => 1
  | S n => if (n > 0) then n * factorial(n-1) else 1
  end.

I needed the conditional so that it terminates for negative inputs. Well, I didn’t need to do this, because 1) n is a natural number, not an integer 2) n > 0 always because 0 is already matched.

Anyway, with this conditional, I get the error:

Error: The term "n0 > 0" has type "Prop" which is not a (co-)inductive type.

Why is this happening? I am assuming that Prop is the proposition type, are propositions different from booleans? Why is the comparison typed as a Prop instead of a boolean?

SOLVED:

Yes, I read later in the chapter that propositions are different from booleans. For example, 1 = 0 is a logical claim, a proposition you can prove, but 1 =? 0 (? is boolean equality) is an expression that evaluates to a boolean. So, n0 > 0 is type Prop - we need to use a less than operator that is in the boolean world.

Apparently, there is a difference between the patterns a, b and (a, b)!

These don’t work:

match leb n m, eqb n m with
  | true, false => true
  | _ => false
end.

The compiler will complain that it expects two patterns for the second case.

match (leb n m, eqb n m) with
  | true, false => true
  | _ => false
end.

Here, the compiler will complain that it expects one pattern for the first case.

However, these work:

match leb n m, eqb n m with
  | true, false => true
  | _, _ => false
end.

match (leb n m, eqb n m) with
  | (true, false) => true
  | _ => false
end.

Why is there a difference, or what is the difference?

ANSWERED:

Here’s the relevant passage.

(** This is simply a convenient abbreviation for nested pattern
    matching.  For example, the match expression on the left below is
    just shorthand for the lower-level "expanded version" shown on the
    right: **)

match l1, l2 with
| A, A => Eq
| A, _ => Gt
end

match l1 with
| A => match l2 with
       | A => Eq
       | _ => Gt
       end
end

This means that one (tuples) is an actual type/pattern, while the comma-on-its-own pattern is syntactic sugar for nested matches.

There’s still a small question: What does it matter? Apparently in Why3 / automated theorem prover, the code structure matters, because the prover can get confused…

Does it matter that we use a tuple or nested matches? Maybe it has to do something with simpl behavior.

Apparently rewrite -> is rewriting from “left to right” while rewrite <- is rewriting from “right to left”.

What is the difference? When does it matter and what’s an example of when it matters?

ANSWERED:

You can try it out on proofs.

I want to see what the current goal looks like, at an intermediate proof step. I don’t know how to do that.

ANSWERED:

It’s pretty simple. Use the arrows to step through each line. The screen on the right shows you the current goal.

Oh, and the UI is atrociously bright, so I’ve switched to ProofGeneral in emacs. It also allows me to have my notes on a buffer to the side.

For ProofGeneral, the keybindings C-c C-n, C-c C-u, C-c C-RET are what matters most.

Coq demands that at least one argument in a Fixpoint definition of a function be strictly decreasing. This ensures that all functions terminate. How does Coq do this? And why does the author say that Coq’s way of doing this is unsophisticated, and that it is “sometimes necessary to write functions in slightly unnatural ways?”

ANSWERED:

OK, I’ve defined a function summation that Coq doesn’t detect as terminating. This is because the argument i is increasing and the other argument n is constant. We know it terminates because n-i strictly decreases and reaches 0. This seems annoying – can’t we avoid having to design code such that every argument must be decreasing?

A notation (infix operator) has precedence, associativity, and a notation scope. What’s a notation scope? This isn’t too important (it’s just for infix operators in Coq!), but the chapter talks about it but never clarifies or defines what a notation scope is.

The chapter explains how tactics are used. And I got a lot of practice with tactics. But what is actually happening when I use a tactic? Can someone explain the parts of an interactive theorem prover?

The underlined buffer thingy is atrocious.

For bin_to_nat, I had to define pow and use a helper function bin_to_nat'.

Definition bin_to_nat (m : bin) : nat :=
  bin_to_nat' m O.

The wording of the question makes me feel like it can be done only one Fixpoint bin_to_nat. I don’t know if that’s possible. I don’t think so, personally.

I am gonna do this template for notes in the future:

• Summary
• Section 1 (actual notes)
• …
• Optional sections
• Exercises
• Questions
• Reflections
• Further knowledge

Adapted from https://en.wikipedia.org/wiki/Coq_(software)

Coq is a interactive theorem prover released in 1989. Coq works within the theory of the calculus of inductive constructions (what?). Coq is not an automated theorem prover.

Coq has a specification language (what?) called Gallina. Programs in Gallina abide by the weak normalization (what?) property, implying that they always terminate. This avoids the halting problem.

The development of Coq has been supported since 1984 by French Institute for Research in Computer Science and Automation (INRIA), initiated by Thierry Coquand and Gérard Huet.

The Association for Computing Machinery awarded Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013 ACM Software System Award for Coq.

Coq is rooster in French, and comes from the French tradition of naming research development tools after animals. It is also a reference to Coquand’s name and CoC (Calculus of Constructions). However, the Coq community has voted to change the name to “The Rocq Prover” in coming months.

Gallina means hen in Latin, Spanish, Italian and Catalan.

Coq was used by Georges Gonthier of Microsoft Research and Benjamin Wenrer of INRIA to create a surveyable proof (what?) of the four color theorem in 2002.

Notable applications include CompCert, a optimizing compiler for almost all of the C programming language which is programmed and proven correct in Coq, Feit-Thompson Theorem (some substantial group theory thing), and the Fundamental group of the circle.

In 2024, Coq proved the value of the 5-state Busy beaver. The value of the 5-state winning busy beaver was discovered by Heiner Marxen and Jürgen Buntrock back in 1989.

A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.

Adapted from https://www.seas.upenn.edu/~cis5000/current/lectures/cis5000-lec01.pdf, slide 20.

CompCert is by Xavier Leroy at INRIA. The project was started on 2010.

A 2011 PLDI paper studied bugs in C compilers. They generaqted random test cases, put them in source programs, and then compiled it with GCC, LLVM, and 8 other C compilers. There were 325 bugs in total (LLVM: 202, GCC: 79).

CompCert had <10 bugs then (this was when CompCert was still unverified).

After CompCert was verified, they concluded that:

The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.

Back to Top