notes-computer-programming-programmingLanguageDesign-prosAndCons-coq

why does coq require 'reflexivity' in proofs? shouldn't this be assumed?

--

http://adam.chlipala.net/cpdt/html/Intro.html

--

Coq guarantees termination by a condition on the Fixpoint (function definition by structural recursion) operator which only allows structural recursion in function definitions when Coq can guarantee that one of the things being recursed on is decreasing as the recursion goes on.

http://coq.inria.fr/refman/Reference-Manual003.html#hevea_default51

http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab37

--

Coq has generator-based inductive abstract data types (ADTs), using 'Inductive'. It has function defns using 'Definition' and 'match', or structurally recursive function defns using 'Fixpoint'.

--

coq has proof tactics

--

the 'destruct' tactic tells coq to try breaking apart a variable by the cases of its ADT definition, and try and do a subproof for each of these cases.

---

syntax: allow multiple symbol names under one declaration. example from Coq:

" As a notational convenience, if two or more arguments have the same type, they can be written together. In the following definition, (n m : nat) means just the same as if we had written (n : nat) (m : nat).

Fixpoint mult (n m : nat) : nat := match n with

  end."

--

pattern matching on multiple expressions at once. example from Coq:

" You can match two expressions at once by putting a comma between them:

Fixpoint minus (n m:nat) : nat := match n, m with

  end."

--

use of _ for dummy variables

--

coq's 'notations' syntax

" We can make numerical expressions a little easier to read and write by introducing "notations" for addition, multiplication, and subtraction.

Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. "

"at level x" is precedence, "nat_scope" is which namespace the notation is declared in

" Notation "( x , y )" := (pair x y). "

" Notation "x :: l" := (cons x l) (at level 60, right associativity). Notation "[ ]" := nil. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

"

"For example, since we defined + as infix notation for the plus function at level 50, ... The + operator will bind tighter than ::, so 1 + 2 :: [3] will be parsed, as we'd expect, as (1 + 2) :: [3] rather than 1 + (2 :: [3]). "

"

The right associativity annotation tells Coq how to parenthesize expressions involving several uses of :: so that, for example, the next three declarations mean exactly the same thing:

Definition mylist1 := 1 :: (2 :: (3 :: nil)). Definition mylist2 := 1 :: 2 :: 3 :: nil. Definition mylist3 := [1;2;3]. "

" Notation "x ++ y" := (app x y) (right associativity, at level 60). "

--