by Aaron Bohannon and Yves Bertot, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic

# coq intro

the Coq system provides a language in which one handles formulas, verifies that they are well-formed, and proves them. formulas may contain functions and limited forms of computations are provided for these functions. formulas can be constructed by combining propositions with logical connectives, or other expressions with addition, multiplication, the pairing construct (,) , and so on. you can also construct a new function by using the keyword fun, which replaces the λ symbol of lambda calculus

the conditions for terms to be well-formed have two origins: first, the syntax must be respected (parentheses must be balanced, binary operators must have two arguments, etc); second, expressions must respect a type discipline

```    (* comments *)

(*
multiline
*)```

#### keywords

```_
as
at
cofix
else
end
exists
exists2
fix
for
forall
fun
if
IF
in
let
match
mod
Prop
return
Set
then
Type
using
where
with
```

tokens:

```!		%		&		&&		(		()		)
*		+		++		,		-		->		.
.(		..		/		/\		:		::		:<
:=		:>		;		<		<-		<->		<:
<=		<>		=		=>		=_D		>		>->
>=		?		?=		@		[		\/		]
^		{		|		|-		||		}		~
```

to start cli:

`\$> coqtop`

```   Check
Print
Eval
Compute
Let
Fail
Require Import
Open scope
Search
```

the first thing you need to know is how you can check whether a formula is well-formed. the command is called ` Check `. commands are always terminated by a period (.). to see the type of `x`, you can use `Check x.` you can also try to check badly formed formulas and the Coq system returns an informative error statement. the Check command not only checks that expressions are well-formed but it also gives the type o f expressions.

to see the definition of `x`, you can use `Print x.`

```Coq < Let x := 12.
Toplevel input, characters 0-12:
Warning: x is declared as a local definition [local-declaration,scope]
x is defined

Coq < Check x.
x
: nat

Coq < Print x.
x = 12
: nat

Coq < Eval simpl in x.
= x
: nat

Coq < Compute x + 3.
= 15
: nat
```

the notation A:B is used for two purposes:

• the first is to indicate that the type of the expression A is the expression B
• the second purpose is to express that A is a proof of B

`Set`, `Prop` and `Type`

• ` Prop ` is the universe of logical propositions
• ` Set ` is is the universe of program types or specifications
• ` Type ` is the type of ` Set ` and ` Prop `

```Coq < Check (3 , 3 = 5) : nat * Prop.
(3, 3 = 5) : nat * Prop
: nat * Prop

Coq < Check (fun x:nat => x = 3).
fun x : nat => x = 3
: nat -> Prop

Coq < Check (forall x:nat, x < 3 \/ (exists y:nat, x = y + 3)).
forall x : nat, x < 3 \/ (exists y : nat, x = y + 3)
: Prop

Coq < Check (let f := fun x => (x * 3, x) in f 3).
let f := fun x : nat => (x * 3, x) in f 3
: nat * nat
```

you can find the function hidden behind a notation by using the Locate command:

```Coq < Locate "_ <= _".
Notation            Scope
"n <= m" := le n m   : nat_scope
(default interpretation)

Coq < Eval compute in let f := fun x => (x * 3, x) in f 3.
= (9, 3)
: nat * nat
```

types in `Set` are data

Prop is parallel to Set in the hierarchy, but types in Prop can be thought of as logical propositions rather than data. the inhabitants of types in Prop can be thought of as proofs rather than programs

why Coq uses that division? not all functions of type A -> B are equal, but all proofs of a proposition P -> Q are. this idea is known as "proof irrelevance"

#### natural numbers

```    Require Import Nat.

Search nat.
...................................
```

```nat  : Set

O    : nat
S    : nat -> nat

succ: nat -> nat
pred: nat -> nat

plus : nat -> nat -> nat
mult : nat -> nat -> nat

max: nat -> nat -> nat
min: nat -> nat -> nat

even: nat -> bool
odd: nat -> bool

pow: nat -> nat -> nat
gcd: nat -> nat -> nat
```

```Coq < Eval compute in S O.
= 1
: nat

Coq < Eval compute in S (S O).
= 2
: nat

Coq < Eval compute in mult (S (S O)) (S (S O)).
= 4
: nat

Coq < Eval simpl in plus 4 5.
= 9
: nat

Coq < Require Import Nat. Compute modulo 12 5.
= 2
: nat
```

#### booleans (data)

```    Require Import Bool.

Search bool.
...................................
```

```bool  : Set

true  : bool
false : bool

andb  : bool -> bool -> bool
orb   : bool -> bool -> bool
implb : bool -> bool -> bool
xorb  : bool -> bool -> bool
negb  : bool -> bool
```

#### logical properties (not data)

```True  : Prop
False : Prop

not = fun A : Prop => A -> False : Prop -> Prop

Inductive or (A B : Prop) : Prop :=
or_introl : A -> A \/ B | or_intror : B -> A \/ B

Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B

I     : True
```

```Coq < Compute orb false true.
= true
: bool

> Compute not true.
>             ^^^^
Error:
The term "true" has type "bool" while it is expected to have type "Prop".
```

the expression “forall ident : type, term” denotes the product of the variable ident of type type , over the term term . Note that term is intended to be a type

If the variable ident occurs in term, the product is called dependent product

a dependent product `forall x : A , B` denotes either

• the universal quantification of the variable x of type A in the proposition B
• or the functional dependent product from A to B (usually written Πx:A . B)

non-dependent product types have a special notation: ``` A -> B ``` stands for “forall _ : A , B”

the non-dependent product is used both to denote

• the propositional implication and
• function types

the expression “term : type” enforces the type of term to be type

`value : forall A : Type, A -> option A`

```definitions ::= | Inductive   | Coinductive
| Fixpoint    | CoFixpoint
| Definition  | Defined
| Variant     | Varibables

form ::= |  True
|  False
|  ~ form	                     (not)
|  form /\ form	             (and)
|  form \/ form	             (or)
|  form -> form	             (primitive implication)
|  form <-> form	             (iff)
|  forall ident : type , form	     (primitive for all)
|  exists ident [: specif] , form   (ex)
|  term = term	                     (eq)

spec ::= |  spec * spec	                     (prod)
|  spec + spec	                     (sum)
|  spec + { spec }	             (sumor)
|  { spec } + { spec }	             (sumbool)
|  { ident : spec | form }	     (sig)
|  { ident : spec | form & form }   (sig2)
|  { ident : spec & spec }	     (sigT)
|  { ident : spec & spec & spec }   (sigT2)

term ::= ( term , term )	             (pair)
```

```tt : unit

list : Type -> Type

if _ then _ else _
```

```Coq < Compute if true then 12 else 13.
= 12
: nat

Coq < Compute if false then 12 else 13.
= 13
: nat
Coq < Compute if 2 then 12 else 13.
= 13
: nat

Coq < Compute if 0 then 12 else 13.
= 12
: nat
```

#### arithmetics

` Require Import Arith. Open scope nat_scope. `

```    Notation	     Interpretation
------------------------------------------
_ < _	          lt
x <= y	          le
_ > _	          gt
x >= y	          ge
x < y < z	          x < y /\ y < z
x < y <= z	          x < y /\ y <= z
x <= y < z	          x <= y /\ y < z
x <= y <= z	          x <= y /\ y <= z
_ + _	          plus
_ - _	          minus
_ * _	          mult
-------------------------------------------
```

` Require Import ZArith. Open scope Z_scope. `

```    Notation	Interpretation	Precedence	Associativity
--------------------------------------------------------------
_ < _	Z.lt
x <= y	Z.le
_ > _	Z.gt
x >= y	Z.ge

x < y < z	    x < y /\ y < z
x < y <= z	    x < y /\ y <= z
x <= y < z	    x <= y /\ y < z
x <= y <= z	    x <= y /\ y <= z

- _	        Z.opp

_ - _	Z.sub
_ * _	Z.mul
_ / _	Z.div
_ mod _	Z.modulo	40	         no

_ ^ _	Z.pow

_ ?= _	Z.compare	70	         no
-----------------------------------------------------------
```

the package ZArith provides two inductive data-types to represent integers. the first inductive type, named positive, follows a binary representation to model the positive integers (from 1 to infinity) and the type Z is described as a type with three constructors, one for positive numbers, one for negative numbers, and one for 0. the package also provides orders and basic operations: addition, subtraction, multiplication, division, square root. the type Z is not suited for structural recursion

we can tell the Coq system to forget about the specification notations for integers:

` Close Scope Z_scope.`

#### lists

` Require Import List. Open Scope list_scope. `

```Notation	Interpretation       Precedence	Associativity
-------------------------------------------------------------
length	        length
tail	        all but first element
app	        concatenation
rev	        reverse
nth	        accessing n-th element (with default)
map	        applying a function
flat_map	applying a function returning lists
fold_left	iterator (from head to tail)
fold_right	iterator (from tail to head)

_ ++ _	        app	              60	   right
_ :: _	        cons	              60	   right
--------------------------------------------------------------
```

```Coq <  Check 1::2::3::nil.
1 :: 2 :: 3 :: nil
: list nat

Coq < Eval compute in map (fun x => x + 3) (1::3::2::nil).
= 4 :: 6 :: 5 :: nil
: list nat
```

```\$> coqtop
Welcome to Coq 8.6 (April 2017)

Coq < Check (fun x : nat => x).
fun x : nat => x
: nat -> nat

Coq < Check (fun x : True => x).
fun x : True => x
: True -> True

Coq < Check I.
I
: True

Coq < Check (fun _ : False => I).
fun _ : False => I
: False -> True

Coq < Check (fun x : False => x).
fun x : False => x
: False -> False

Coq < Inductive unit : Set := tt.
unit is defined
unit_rect is defined
unit_ind is defined
unit_rec is defined

Coq < Check unit.
unit
: Set

Coq < Check tt.
tt
: unit
```
[unit] is the type with only one value - [tt], and [True] is the proposition that has one proof - I, and always holds. by replacing
```      Set     to     Prop
unit    to     True
tt      to     I```
you get the definition of [True] from the Coq stdlib

### propositions and proofs

the notation t:B is actually used for several purposes in the Coq system. one of the se purposes is to express that t is a proof for the logical formula B. to construct proofs of formulas, we can simply look for existing proofs. alternatively, we can construct new proofs and give them a name

one can find already existing proofs of facts by using the Search command. its argument should always be an identifier. the command SearchPattern takes a pattern as argument, where some of the arguments of a predicate can be replaced by incomplete expressions. the command SearchAbout makes it possible to find all theorems that are related to a given symbol

```assertion_keyword ::=
| Theorem    | Lemma
| Remark     | Fact
| Corollary  | Proposition
| Definition | Example
| Goal       | Axiom

proof ::=
| Proof . … Qed .
| Proof . … Defined .
| Proof . … Admitted .

```

the keyword `Lemma` is used to state a new proposition you intent to prove. `Theorem` and `Fact` are just synonyms for `Lemma`

the keyword `Proof`, immediately following the statement of the proposition, indicates the beginning of a proof script (can be omitted, but this is not recommendet)

once all of the goals are solved, you should use the keyword `Qed` to record the completed proof. if the proof is incomplete, you may tell Coq to accept the lemma on faith by using `Admitted` instead of `Qed`

examples:

```Coq < Theorem obvious : True.
1 subgoal

============================
True

obvious < Proof. apply I. Qed.
1 subgoal

============================
True

No more subgoals.

Proof.
(apply I).

Qed.
obvious is defined
```

```Coq < Theorem unit_singleton : forall x : unit, x = tt.
1 subgoal

============================
forall x : unit, x = tt

unit_singleton < induction x. (* destruct x. *) reflexivity. Qed.
1 subgoal

============================
tt = tt

No more subgoals.

(induction x).
reflexivity.

Qed.
unit_singleton is defined
```

```
Coq < Inductive Empty : Set := .
Empty is defined
Empty_rect is defined
Empty_ind is defined
Empty_rec is defined
```
[Empty] has no elements; the fact of having an element implies anything. [Empty] is equivalent of [False]. now:
```Coq < Theorem black_is_white : forall x : Empty, 2 + 2 = 5.
1 subgoal

============================
Empty -> 2 + 2 = 5

black_is_white < Proof. destruct 1. Qed.
1 subgoal

============================
Empty -> 2 + 2 = 5

No more subgoals.

Proof.
(destruct 1).

Qed.
black_is_white is defined
```
[destruct 1] instead of [destruct x] because unused quantified vars are referred by number

```Coq < Check Empty.
Empty
: Set

Coq < Definition e2u (e : Empty) : unit := match e with end.
e2u is defined
```
matching on a value whose type has no constructors you no need to provide any branches

another examples:

```Goal 1 = 1 -> 1 = 1.
intro. assumption. Qed.

Goal forall A B : Prop, A -> B -> A /\ B.
intros A B H1 H2. split. assumption. assumption. Qed.

Goal forall A B : Prop, A /\ B -> B.
intros A B H. decompose [and] H. assumption. Qed.

Goal forall A B : Prop, A -> A \/ B.
intros A B H. left. assumption. Qed.

Goal forall A B : Prop, B -> A \/ B.
intros A B H. right. assumption. Qed.

Goal exists x : nat, forall y, x + y = y.
exists 0. simpl. reflexivity. Qed.

Goal exists x : nat, forall y, y + x = y.
exists 0.  auto. Qed.

Lemma lemmaPlus0 : forall x, x + 0 = x. auto. Qed.
Goal 3 + 0 = 3. apply lemmaPlus0. Qed.

Goal forall x, 0 + x = x. reflexivity. Qed.

Require Import ZArith Ring Field. Open Local Scope Z_scope.

Lemma toto1 : 1 + 1 = 2. ring. Qed.
Lemma toto2 : 2 + 1 = 3. ring. Qed.
Hint Resolve toto1 toto2 : totobase.
Goal 2 + (1 + 1) = 4. auto with totobase. Qed.

Goal 1 = 1 -> 1 = 1 -> 1 = 1. intros H1 H2. exact H1. Qed.
Goal 1 = 1 -> 1 = 1 -> 1 = 1. intros H1 H2. exact H2. Qed.
```

#### emacs keybinding for ProofGeneral

 C-c C-b loads an emacs buffer into coqtop C-c C-c interrupts coqtop; useful if it hangs C-c C-r retracts a buffer C-c C-n one-step C-c C-u undo last step C-c C-. jump to the last evaluated point C-c C-s hide/show goals C-c C-l restore 3W-mode C-c C-a C -b tell me about ... C-c C-a C-c check ... C-c C-a C-p print ...

by default, the "." key is "electric" - it inserts a period _and_ causes the material up to the cursor to be sent to Coq. if you find this behavior annoying, it can be toggled by doing "C-c ."

#### tactics

a proposition and its proof are both represented as terms in the calculus of inductive constructions

proof terms are built interactively, using tactics to manipulate a proof state

a proof state consists of a set of goals (propositions or types for which you must produce an inhabitant), each with a context of hypotheses (inhabitants of propositions or types you are allowed to use)

a proof state begins initially with one goal (the statement of the lemma you are tying to prove) and no hypotheses

a goal can be solved, and thereby eliminated, when it exactly matches one of hypotheses in the context

a proof is completed when all goals are solved

tactics can be used for

• forward reasoning - modifying the hypotheses of a context while leaving the goal unchanged
• backward reasoning - replacing the current goal with one or more new goals in simpler contexts
• it would be ridiculously impractical to complete a proof using forward reasoning alone. however it is usually both possible and practical to complete a proof using backward reasoning alone. most people naturally use a significant amount of forward reasoning in their thinking process, so it may take you a while to become accustomed to getting by without it

a proof script is a sequence of tactic expressions, each concluding with a (.)

intros, apply, simpl, and reflexivity are examples of tactics

ring , field (you can divide in field but not in ring)

```Require Import ZArith. Open Scope Z_scope.

Theorem myplus : 2 + 3 = 3 + 2.
Proof. compute . reflexivity. Qed.

Theorem myplus2 : 2 + 3 = 3 + 2.
Proof. simpl . reflexivity. Qed.
```

induction will make it possible to perform a proof by induction on a natural number n. this decompose the proof in two parts: first we need to verify that the property to prove is satisfy when n is 0, second we need to prove the property for S p is a consequence of the same property for p (the hypothesis about the property for p is called the induction hypothesis, its name usually starts with IH). two goals are created, one for 0 and one for S p.

simpl will replace calls of a recursive function on a complex argument by the corresponding value

discriminate will be usable when one hypothesis asserts that 0 = S ... or true = false

injection will be usable when one hypothesis has the form S x = S y to deduce x = y

most theorems are universally quantified and the values of the quantified variables must be guessed when the theorems are used. the rewrite guesses the values of the quantified variables by finding patterns of the lhs in the goal’s conclusion and instanciating the variables accordingly

a common approach to proving difficult propositions is to assert inter mediary steps using a tactic called assert. given an argument of the form (H:P) , this tactic yields two goals, where the first one is to prove P, while the second one is to prove the same statement as before, but in a context where a hypothesis named H and with the statement P is added

#### defining new constants

you can define a new constant by using the keyword Definition :

` Definition example1 := fun x : nat => x * x + 2 * x + 1. `

an alternative, exactly equivalent, definition could be:

` Definition example1 (x : nat) := x * x + 2 * x + 1. `

after executing one of these commands, the function can be used in other commands

sometimes, you may want to forget a definition that you just made. this is done using the Reset command, giving as argument the name you just defined

#### parameterized constructors

datatype constructors can be parameterized. such constructors yield a different value for each argument sequence. consider the type byte:

```Inductive byte := Byte(b7 b6 b5 b4 b3 b2 b1 b0: bool).

Definition negate_byte(b: byte): byte :=
match b with Byte b7 b6 b5 b4 b3 b2 b1 b0 =>
Byte
(negate b7)
(negate b6)
(negate b5)
(negate b4)
(negate b3)
(negate b2)
(negate b1)
(negate b0)
end.```
the datatype byte has 256 values, all yielded by applying the single constructor Byte to different sequences of booleans

```Inductive sum (A B : Type) : Type :=  inl : A -> A + B | inr : B -> A + B

left  : forall A B : Prop, A -> {A} + {B}
right : forall A B : Prop, B -> {A} + {B}

Inductive prod (A B : Type) : Type :=  pair : A -> B -> A * B

pair : forall A B : Type, A -> B -> A * B
fst  : forall A B : Type, A * B  -> A
snd  : forall A B : Type, A * B  -> B
```

```Coq < Compute pair 1 2.
= (1, 2)
: nat * nat

Coq < Compute (1,2).
= (1, 2)
: nat * nat
```

```id : forall A : Type, A -> A

eq_refl : forall (A : Type) (x : A), eq A x x

andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
O_S : forall n : nat, 0 <> S n
n_Sn: forall n : nat, n <> S n

plus_n_O       : forall n : nat, n = n + 0
plus_O_n       : forall n : nat, 0 + n = n
plus_n_Sm      : forall n m : nat, S (n + m) = n + S m
plus_Sn_m      : forall n m : nat, S n + m = S (n + m)

f_equal2_plus  : forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2

mult_n_O       : forall n : nat, 0 = n * 0
mult_n_Sm      : forall n m : nat, n * m + n = n * S m

f_equal2_mult  : forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2

f_equal2_nat   : forall (A : Type) (f : nat -> nat -> A) (x1 y1 x2 y2 : nat),
x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
```

to compile source file into library use `coqc <file> ` cli command

#### extraction

in the Coq system, programs are usually represented by functions. simple programs can be executed in the Coq system itself, more complex Coq programs ca n be transformed into programs in more conventional languages and executed outsid e Coq

program extraction, which generates OCaml code from Coq developments. for instance:

` Extraction somefunction. `.

this command just print extracted version. you can compile with the OCaml compiler and obtain an executable program

this command just print, but you can get more ... first you say what language you want to extract into (Ocaml or Haskell):

``````
Extraction Language Ocaml.
``````
now you load up the Coq environment with some definitions, either directly or by importing them from other modules. then you tell Coq the name of a definition to extract and the name of a file to put the extracted code into:
``````
Extraction "implementation.ml" your_function_name.
``````
Coq generates a file "implementation.ml" containing an extracted version of your_function_name, together with everything that it recursively depends on.

```   Extraction
Module  <name> ... End ... <name>
Section <name> ... End ... <name>
```

### a simple language of exp over nats and bools

you define n-ary relations in Coq by giving a set of inference rules

### Inductive

```Inductive tm : Set :=
| tm_T   : tm               (* true *)
| tm_F   : tm               (* false *)
| tm_if  : tm -> tm -> tm -> tm
| tm_Z   : tm               (* zero *)
| tm_S   : tm -> tm         (* succ *)
| tm_P   : tm -> tm         (* pred *)
| tm_isZ : tm -> tm.
```

the `Inductive` keyword defines a new type with name `tm` and declare that `tm` lives in the sort ` Set `

now the environment contains the name of the newly defined type `tm`, along with the names of all of the constructors

the property of "being a value" is a unary relation over `tm`s. two relations: `bval` and `nval`. it is possible to view their type as a datatype; however, it is more natural to interpret it as a proposition, so it will be declared to live in Prop:

```Inductive bval : tm -> Prop :=
| b_T : bval tm_T
| b_F : bval tm_F .

Inductive nval : tm -> Prop :=
| n_Z : nval tm_Z
| n_S : forall t , nval t -> nval (tm_S t) .
```

the unary relations `bval` and `nval` are families of types indexed by elements of `tm`. you can build inhabitants of some (but not all) of the types in these families with the constructors:

the proposition `bval t | nval t` will be true if it is inhabited and false if it is not. Coq's logic is constructive and `P \/ not P` is provable for some `P` but not provable for others

the `Definition` keyword is used for defining non-recursive functions (including 0-ary functions, i.e., constants)

you can define a call-by-value operational semantics by giving a definition of the single-step evaluation of one term to another - as an inductively defined binary relation eval:

```Definition gval (t : tm) : Prop :=  bval t \/ nval t.

Inductive eval : tm -> tm -> Prop :=
| e_if    : forall t k t1 t2, eval t k -> eval (tm_if t t1 t2) (tm_if k t1 t2)
| e_ifT   : forall t1 t2,     eval (tm_if tm_T t1 t2) t1
| e_ifF   : forall t1 t2,     eval (tm_if tm_F t1 t2) t2
| e_S     : forall t k,       eval t k -> eval (tm_S t) (tm_S k)
| e_P     : forall t k,       eval t k -> eval (tm_P t) (tm_P k)
| e_predZ :                   eval (tm_P tm_Z) tm_Z
| e_predS : forall t,         nval t -> eval (tm_P (tm_S t)) t
| e_isZ   : forall t k,       eval t k -> eval (tm_isZ t) (tm_isZ k) .
| e_isZZ  :                   eval (tm_isZ tm_Z) tm_T
| e_isZS  : forall t,         nval t -> eval (tm_isZ (tm_S t)) tm_F
```

the multi-step evaluation is defined with the relation `eval_many`. this relation includes all of the pairs of terms that are connected by sequences of evaluation steps:

```Inductive eval_many : tm -> tm -> Prop :=
| m_refl : forall t,        eval_many t t
| m_step : forall t1 t2 t3, eval t1 t2 -> eval_many t2 t3 -> eval_many t1 t3.

Definition normal_form (t : tm) : Prop := ~ exists k , eval t k.
```

a term is a `normal_form` if there is no term to which it can step. note the concrete syntax for negation (~) and existential quantification exists in the definition

a big-step semantics:

```Inductive f_eval : tm -> tm -> Prop :=
| f_gval  : forall v          , gval v -> f_eval v v
| f_ifT   : forall t1 t2 t3 v , f_eval t1 tm_T -> f_eval t2 v -> f_eval (tm_if t1 t2 t3) v
| f_ifF   : forall t1 t2 t3 v , f_eval t1 tm_F -> f_eval t3 v -> f_eval (tm_if t1 t2 t3) v
| f_succ  : forall t v        , nval v -> f_eval t v -> f_eval (tm_S t) (tm_S v)
| f_predZ : forall t          , f_eval t tm_Z -> f_eval (tm_P t) tm_Z
| f_predS : forall t v        , nval v -> f_eval t (tm_S v) -> f_eval (tm_P t) v
| f_isZZ  : forall t          , f_eval t tm_Z -> f_eval (tm_isZ t) tm_T
| f_isZS  : forall t v        , nval v -> f_eval t (tm_S v) -> f_eval (tm_isZ t) tm_F .
```

### Variant

```Variant bool_option : Set :=
| some_bool : bool -> bool_option
| no_bool : bool_option.

Variant nat_option : Set :=
| some_nat : nat -> nat_option
| no_nat : nat_option.
```

the Variant keyword is identical to the Inductive keyword, except that it disallows recursive definition of types (in particular lists cannot be defined with the Variant keyword).

### Fixpoint

to recursively do something use the keyword Fixpoint instead of Definition

```Fixpoint tm_to_nat (t : tm) {struct t} : nat_option :=
match t with
| tm_Z => some_nat O
| tm_S t1 =>
match tm_to_nat t1 with
| some_nat n => some_nat (S n)
| no_nat => no_nat
end
| _ => no_nat
end.

Fixpoint nat_to_tm (n : nat) {struct n} : tm :=
match n with
| O => tm_Z
| S m => tm_S (nat_to_tm m)
end.

Definition tm_to_bool (t : tm) : bool_option :=
match t with
| tm_T => some_bool true
| tm_F => some_bool false
| _ => no_bool
end.

Definition bool_to_tm (b : bool) : tm :=
match b with
| true => tm_T
| false => tm_F
end.
```

the type system will only allow us to write functions that terminate. the annotation ` {struct t} ` here informs the type-checker that termination is guaranteed because the function is being defined by structural recursion on t

### Universal Quantification

the tactic intros x1 ... xn moves antecedents and universally quantified variables from the goal into the context

``````Lemma e_S_P_S :
forall t ,
nval t -> eval (tm_S (tm_P (tm_S t))) (tm_S t) .
Proof.```

============================
forall t : tm, nval t -> eval (tm_S (tm_P (tm_S t))) (tm_S t)

`intros.`

t : tm
H : nval t
============================
eval (tm_S (tm_P (tm_S t))) (tm_S t)
```

if the conclusion (the part following the rightmost arrow) `e` of a constructor, hypothesis, or lemma matches our current goal, then apply e will replace the goal with a new goal for each premise/antecedent of `e`. if `e` has no premises, then the current goal is solved

by `e_S`, in order to prove our conclusion, it suffices to prove that `eval (tm_P (tm_S t)) t`

````apply  e_S.`

t : tm
H : nval t
============================
eval (tm_P (tm_S t)) t
```

that, in turn, can be shown by `e_predS`, if we are able to show that `nval t`

````apply e_predS.`

t : tm
H : nval t
============================
nval t

`apply H.`

No more subgoals.

Qed.
```

consider the rule `m_step`:

```    eval t1 t2    eval_many t2 t3
-----------------------------  (m_step)
eval_many t1 t3
```

if we have a goal such as `eval_many e1 e2`, we should be able to use `apply m_step` in order to replace it with the goals `eval e1 t2` and `eval_many t2 e2`. but what exactly is `t2` here? how is it chosen?

it stands to reason the conclusion is justified if we can come up with any `k` for which the premises can be justified

for the type of `m_step`, all three variables `t1`, `t2`, and `t3` are universally quantified. the tactic `apply m_step` will use pattern matching between our goal and the conclusion of `m_step` to find the only possible instantiation of `t1` and `t3`. however, `apply m_step` will raise an error since it does not know how it should instantiate `t2`

in this case, the apply tactic takes a `with` clause that allows us to provide this instantiation

``````Lemma m_S_P_S :
forall t ,
nval t -> eval_many (tm_S (tm_P (tm_S t))) (tm_S t).
Proof.```

============================
forall t : tm,
nval t -> eval_many (tm_S (tm_P (tm_S t))) (tm_S t)
```

the proof tree:

```    s    =  tm_S
p    =  tm_P
lem  =  e_S_P_S

nval t
-----------------------  (lem)     ---------------------  (m_refl)
eval (s (p (s t))) (s t)           eval_many (s t) (s t)
------------------------------------------------------------------   (m_step)
eval_many (s (p (s t))) (s t)
```

````intros t H0.`

t : tm
H0 : nval t
============================
eval_many (tm_S (tm_P (tm_S t))) (tm_S t)
```

by `m_step`, to show our conclusion, it suffices to find some `k` for which `eval (tm_S (tm_P (tm_S t))) k` and `eval k (tm_S t)`. let us choose `k` to be `tm_S t`:

````apply m_step with (t2 := tm_S t).`

t : tm
H0 : nval t
============================
eval (tm_S (tm_P (tm_S t))) (tm_S t)

eval_many (tm_S t) (tm_S t)
```
by the lemma `e_S_P_S`, to show `eval (tm_S (tm_P (tm_S t))) (tm_S t)`, it suffices to show `nval t`.
````apply e_S_P_S.`

t : tm
H0 : nval t
============================
nval t

eval_many (tm_S t) (tm_S t)

`apply H0.`

t : tm
H0 : nval t
============================
eval_many (tm_S t) (tm_S t)
```
by the rule `m_refl`, we also may conclude `eval (tm_S t) (tm_S t)`:
```` apply m_refl.`

No more subgoals.

Qed.
```

proofs of universally quantified propositions are functions that take the witness of the quantifier as an argument. proofs of implications are functions that take one proof as an argument and return another proof. observe the types of the following terms:

``````Check (e_S_P_S).
Check (e_S_P_S tm_Z).
Check (n_Z).
Check (e_S_P_S tm_Z n_Z).
``````

any tactic like `apply` that takes the name of a constructor or lemma as an argument can just as easily be given a more complicated expression as an argument. thus, we may use function application to construct proof objects on the fly. observe how this technique can be used to rewrite the proof of the previous lemma:

``````Lemma m_S_P_S_alt :
forall t,
nval t -> eval_many (tm_S (tm_P (tm_S t))) (tm_S t).
Proof.
intros t H0.```

t : tm
H0 : nval t
============================
eval_many (tm_S (tm_P (tm_S t))) (tm_S t)
```
apply (m_step
(tm_S (tm_P (tm_S t)))
(tm_S t)
(tm_S t)
).```

t : tm
H0 : nval t
============================
eval (tm_S (tm_P (tm_S t))) (tm_S t)

eval_many (tm_S t) (tm_S t)

```
apply (e_S_P_S t H0).```

t : tm
H0 : nval t
============================
eval_many (tm_S t) (tm_S t)

```
apply (m_refl (tm_S t)).```

No more subgoals.

Qed.
```

sometimes it is useful to be able to replace a defined name in a proof with its definition. this sort of replacement can be done the tactic unfold

```Definition strongly_diverges t :=
forall u, eval_many t u -> ~ normal_form u.
```

```Lemma unfold_example : forall t k,
strongly_diverges t -> eval t k -> strongly_diverges k.
Proof.

============================
forall t k : tm,
strongly_diverges t -> eval t k -> strongly_diverges k

`intros t k Hd He.`

t, k : tm
Hd : strongly_diverges t
He : eval t k
============================
strongly_diverges k

`unfold strongly_diverges.`

t, k : tm
Hd : strongly_diverges t
He : eval t k
============================
forall u : tm, eval_many k u -> ~ normal_form u

`intros u Hm.`

t, k : tm
Hd : strongly_diverges t
He : eval t k
u : tm
Hm : eval_many k u
============================
~ normal_form u

`unfold strongly_diverges in Hd.`

t, k : tm
Hd : forall u : tm,
eval_many t u -> ~ normal_form u
He : eval t k
u : tm
Hm : eval_many k u
============================
~ normal_form u

`apply Hd.`

t, k : tm
Hd : forall u : tm,
eval_many t u -> ~ normal_form u
He : eval t k
u : tm
Hm : eval_many k u
============================
eval_many t u

`apply m_step with (t2 := k).`

t, k : tm
Hd : forall u : tm,
eval_many t u -> ~ normal_form u
He : eval t k
u : tm
Hm : eval_many k u
============================
eval t k

eval_many k u

`apply He.`

t, k : tm
Hd : forall u : tm,
eval_many t u -> ~ normal_form u
He : eval t k
u : tm
Hm : eval_many k u
============================
eval_many k u

`apply Hm.`

No more subgoals.

Qed.
```

### conjunction and disjunction

if `H` is the name of a conjunctive hypothesis, then `destruct H as p` will replace the hypothesis `H` with its components using the names in the pattern `p`

```Lemma m_two_conj : forall t0 t1 t2,
eval t0 t1 /\ eval t1 t2 -> eval_many t0 t2.
Proof.

============================
forall t0 t1 t2 : tm,
eval t0 t1 /\ eval t1 t2 -> eval_many t0 t2

`intros t0 t1 t2 H.`

t0, t1, t2 : tm
H : eval t0 t1 /\ eval t1 t2
============================
eval_many t0 t2

`destruct H as [ He1 He2 ].`

t0, t1, t2 : tm
He1 : eval t0 t1
He2 : eval t1 t2
============================
eval_many t0 t2

`apply m_two with (t2 := t1).`

t0, t1, t2 : tm
He1 : eval t0 t1
He2 : eval t1 t2
============================
eval t0 t1

eval t1 t2

`apply He1.`

t0, t1, t2 : tm
He1 : eval t0 t1
He2 : eval t1 t2
============================
eval t1 t2

`apply He2.`

No more subgoals.
(dependent evars: (printing disabled) )

Qed.
```

patterns may be nested to break apart nested structures. note that infix conjunction is right-associative, which is significant when trying to write nested patterns.

```Lemma m_three_conj : forall t0 t1 t2 t3,
eval t0 t1 /\ eval t1 t2 /\ eval t2 t3 -> eval_many t0 t3.
Proof.

============================
forall t0 t1 t2 t3 : tm,
eval t0 t1 /\ eval t1 t2 /\ eval t2 t3 ->
eval_many t0 t3

`intros t0 t1 t2 t3 H.`

t0, t1, t2, t3 : tm
H : eval t0 t1 /\ eval t1 t2 /\ eval t2 t3
============================
eval_many t0 t3

`destruct H as [ He1 [ He2 He3 ] ].`

t0, t1, t2, t3 : tm
He1 : eval t0 t1
He2 : eval t1 t2
He3 : eval t2 t3
============================
eval_many t0 t3

`apply m_step with (t2 := t1).`

t0, t1, t2, t3 : tm
He1 : eval t0 t1
He2 : eval t1 t2
He3 : eval t2 t3
============================
eval t0 t1

eval_many t1 t3

`apply He1.`

t0, t1, t2, t3 : tm
He1 : eval t0 t1
He2 : eval t1 t2
He3 : eval t2 t3
============================
eval_many t1 t3

`apply m_two with (t2 := t2).`

t0, t1, t2, t3 : tm
He1 : eval t0 t1
He2 : eval t1 t2
He3 : eval t2 t3
============================
eval t1 t2

eval t2 t3

`apply He2.`

t0, t1, t2, t3 : tm
He1 : eval t0 t1
He2 : eval t1 t2
He3 : eval t2 t3
============================
eval t2 t3

`apply He3.`

No more subgoals.
(dependent evars: (printing disabled) )

Qed.
```

if your goal is a conjunction, use split to break it apart into two separate subgoals:

```Lemma m_three : forall t0 t1 t2 t3,
eval t0 t1 -> eval t1 t2 -> eval t2 t3 -> eval_many t t3.
Proof.
`intros t t1 t2 t3 He1 He2 He3.`
`apply m_three_conj with (t1 := t1) (t2 := t2).`
`split. apply He1.`
`split. apply He2. apply He3.`
Qed.
```

```Lemma m_if_iszero_conj : forall v t1 t2 t3 t4,
nval v /\ eval t1 t2 /\ eval t3 t4 ->
eval_many (tm_if (tm_isZ tm_Z) t1 t3) t2 /\ eval_many (tm_if (tm_isZ (tm_S v)) t1 t3) t4.
Proof.
```

if the goal is a disjunction, we can use the left or right tactics to solve it by proving the left or right side of the conclusion

```Lemma true_and_S_zero_values :
value tm_T /\ value (tm_S tm_Z).
Proof.
`unfold value. split.`
`left. apply b_T.`
`right. apply n_S. apply n_Z.`
Qed.```

If we have a disjunction in the context, we can use `destruct` to reason by cases on the hypothesis. Note the syntax of the associated pattern.

```Lemma e_if_true_or_false : forall t1 t2,
eval t1 tm_T \/ eval t1 tm_F ->
eval_many (tm_if t1 t2 t2) t2.
Proof.
`intros t1 t2 H. destruct H as [ He1 | He2 ].`
`apply m_two with (t2 := tm_if tm_T t2 t2).`
`apply e_if. apply He1.`
`apply e_ifT.`
`apply m_two with (t2 := tm_if tm_F t2 t2).`
`apply e_if. apply He2.`
`apply e_ifF.`
Qed.```

```Lemma two_values : forall t u,
value t /\ value u ->
bvalue t \/
bvalue u \/
(nval t /\ nval u).
Proof.
We know `value t` and `value u`,
which means either `bvalue t` or `nval t`,
and either `bvalue u` or `nval u`.
Consider the case in which `bvalue t` holds.
Then one of the disjuncts of our conclusion is proved.
Next, consider the case in which `nval t` holds.
Now consider the subcase where `bvalue u` holds. ...

`destruct` can be used on propositions with implications. this will have the effect of performing `destruct` on the conclusion of the implication, while leaving the hypotheses of the implication as additional subgoals

```Lemma destruct_example : forall bv t t1 t1',
bvalue bv ->
(value bv -> eval t t1 /\ eval t1 t1') ->
eval_many t t1'.
Proof.
`intros bv t t1 t1' Hbv H. destruct H as [ H1 H2 ].`
Show 2.
`unfold value. left. apply Hbv.`
`apply m_two with (t2 := t1).`
`apply H1.`
`apply H2.`
Qed.```

After applying a tactic that introduces multiple subgoals, it is sometimes useful to see not only the subgoals themselves but also their hypotheses. Adding the command `Show n.` to your proof script to cause Coq to display the nth subgoal in full.

### cases and induction

It is possible to supply `destruct` with a pattern on an inductively defined datatype or proposition. However, the patterns become increasingly complex; so it is often more practical to omit the pattern (thereby letting Coq choose the names of the terms and hypotheses in each case), in spite of the fact that this adds an element of fragility to the proof script (since the proof script will mention names that were system-generated).

```Lemma e_isZ_nval : forall v,
nval v ->
eval (tm_isZ v) tm_T \/
eval (tm_isZ v) tm_F.
Proof.
`intros v Hn. destruct Hn.`
`left. apply e_isZZ.`
`right. apply e_isZS. apply Hn.`
Qed.```

You can use `induction` to reason by induction on an inductively defined datatype or proposition. This is the same as `destruct`, except that it also introduces an induction hypothesis in the inductive cases.

```Lemma m_iszero : forall t u,
eval_many t u ->
eval_many (tm_isZ t) (tm_isZ u).
Proof.
`intros t u Hm. induction Hm.`
`apply m_refl.`
`apply m_step with (t1 := tm_isZ t1).`
`apply e_isZ. apply H.`
`apply IHHm.`
Qed.```

```Lemma m_trans : forall t t1 u,
eval_many t t1 ->
eval_many t1 u ->
eval_many t u.
Proof.
We proceed by induction on the derivation of `eval_many t t1`.
Case `m_refl`:
Since `t` and `t1` must be the same, our conclusion holds by assumption.
Case `m_step`:
Now let's rename the `t1` from the lemma statement to `u0` (as Coq likely will)
and observe that there must be some `t1` (from above the line of the `m_step` rule)
such that `eval t t1` and `eval_many t1 u0`.
Our conclusion follows from from an application of `m_step` with our new `t1`
and our induction hypothesis, which allows us to piece together `eval_many t1 u0`
and `eval_many u0 u` to get `eval_many t1 u`.

It is possible to use `destruct` not just on hypotheses but on any lemma we have proved. If we have a lemma

```      lemma1 : P /\ Q
```
then we can use the tactic
`      destruct lemma1 as [ H1 H2 ]. `

to continue our proof with `H1 : P` and `H2 : Q` in our context. This works even if the lemma has antecedents (they become new subgoals); however it fail if the lemma has a universal quantifier, such as this:

`      lemma2 : forall x, P(x) /\ Q(x) `

However, remember that we can build a proof of `P(e) /\ Q(e)` (which can be destructed) using the Coq expression `lemma2 e`. So we need to phrase our tactic as

```      destruct (lemma2 e) as [ H1 H2 ].
```
An example of this technique is below.

```Lemma m_iszero_nval : forall t v,
nval v ->
eval_many t v ->
eval_many (tm_isZ t) tm_T \/
eval_many (tm_isZ t) tm_F.
Proof.
`intros t v Hnv Hm.`
`destruct (e_isZ_nval v) as [ H1 | H2 ].`
`apply Hnv.`
`left. apply m_trans with (t1 := tm_isZ v).`
`apply m_iszero. apply Hm.`
`apply m_one. apply H1.`
`right. apply m_trans with (t1 := tm_isZ v).`
`apply m_iszero. apply Hm.`
`apply m_one. apply H2.`
Qed.```

Prove the following lemma. Hint: You may be interested in some previously proved lemmas, such as `m_one` and `m_trans`.

```Lemma eval_rtc_many : forall t u,
eval_rtc t u -> eval_many t u.
```

Prove the following lemma.

```Lemma eval_many_rtc : forall t u,
eval_many t u -> eval_rtc t u.
```

Prove the following lemma.

```Lemma f_eval_to_value : forall t v,
f_eval t v -> value v.
```

### Existential Quantification

• `exists`
• `destruct` (for existential propositions)
Use `exists` to give the witness for an existential quantifier in your goal.
```Lemma if_bvalue : forall t1 t2 t3,
bvalue t1 ->
exists u, eval (tm_if t1 t2 t3) u.
Proof.
`intros t1 t2 t3 Hb. destruct Hb.`
`exists t2. apply e_ifT.`
`exists t3. apply e_ifF.`
Qed.```
You may use `destruct` to break open an existential hypothesis.
```Lemma m_two_exists : forall t u,
(exists w, eval t w /\ eval w u) ->
eval_many t u.
Proof.
`intros t u H.`
`destruct H as [ w He ].`
`destruct He as [ He1 He2 ].`
`apply m_two with (t2 := w).`
`apply He1.`
`apply He2.`
Qed.```
Tip: We can combine patterns that destruct existentials with patterns that destruct other logical connectives.

Here is the same proof with just one use of `destruct`.

```Lemma m_two_exists' : forall t u,
(exists w, eval t w /\ eval w u) ->
eval_many t u.
Proof.
`intros t u H. destruct H as [ w [ He1 He2 ] ].`
`apply m_two with (t2 := w).`
`apply He1.`
`apply He2.`
Qed.```
Tip: We give patterns to the `intros` tactic to destruct hypotheses as we introduce them.

Here is the same proof again without any uses of `destruct`.

```Lemma m_two_exists'' : forall t u,
(exists w, eval t w /\ eval w u) ->
eval_many t u.
Proof.
`intros t u [ w [ He1 He2 ] ].`
`apply m_two with (t2 := w).`
`apply He1.`
`apply He2.`
Qed.```

```Lemma value_can_expand : forall v,
value v ->
exists u, eval u v.
Tip: You should find the lemma `m_iszero` useful. Use `Check m_iszero.` if you've forgotten its statement.
```Lemma exists_iszero_nvalue : forall t,
(exists nv, nvalue nv /\ eval_many t nv) ->
exists bv, eval_many (tm_isZ t) bv.
Proof.
There exists some `nv` such that `nvalue nv`.  Consider
the case where `nv` is `tm_Z`.  Then choose `bv` to
be `tm_T`.  By `m_trans`, we can show that
`eval_many (tm_isZ t) tm_T` by showing
`eval_many (tm_isZ t) (tm_isZ tm_Z)` and
`eval_many (tm_isZ tm_Z) tm_T`.  The former
follows from `m_iszero` and our assumption.  The latter
follows from `m_one` and the rule `e_isZZ`.  On the
other hand, in the case where `nv` is built from
`tm_succ`, we choose `bv` to be `tm_F` and the proof

### negation

• `unfold not`
• `destruct` (for negation)

The standard library defines an uninhabited type `False` and defines `not P` to stand for `P -> False`. Furthermore, Coq defines the notation `~ P` to stand for `not P`. (Such notations only affect parsing and printing -- Coq views ```not P``` and `~ P` as being syntactically equal.)

The most basic way to work with negated statements is to unfold `not` and treat `False` just as any other proposition.

(Note how multiple definitions can be unfolded with one use of `unfold`. Also, as noted earlier, many uses of `unfold` are not strictly necessary. You can try deleting the uses from the proof below to check that the proof script still works.)

```Lemma normal_form_succ : forall t,
normal_form (tm_S t) ->
normal_form t.
Proof.
`intros t Hnf.`
`unfold normal_form. unfold not.`
`unfold normal_form, not in Hnf.`
`intros [ t' H' ]. apply Hnf.`
`exists (tm_S t'). apply e_succ. apply H'.`
Qed.```
```Lemma normal_form_to_forall : forall t,
normal_form t ->
forall u, ~ eval t u.
```Lemma normal_form_from_forall : forall t,
(forall u, ~ eval t u) ->
normal_form t.
If you happen to have `False` as a hypothesis, you may use `destruct` on that hypothesis to solve your goal.
```Lemma False_hypothesis : forall v,
False ->
value v.
Proof.
intros v H. destruct H.
Qed.```

Recalling that `destruct` can be used on propositions with antecedents and that negation is simply an abbreviation for an implication, using `destruct` on a negated hypothesis has the derived behavior of replacing our goal with the proposition that was negated in our context.

Tip: We actually don't even need to do the unfolding below because `destruct` would have done it for us.

```Lemma destruct_negation_example : forall t v,
value v ->
eval t tm_Z ->
(value v -> normal_form t) ->
eval tm_T tm_F.
Proof.
`intros t v Hnv He Hnf.`
`unfold normal_form, not in Hnf.`
`destruct Hnf.`
`apply Hnv.`
`exists tm_Z. apply He.`
Qed.```
This one may be a bit tricky. Start by using `destruct` on one of your hypotheses.
```Lemma negation_exercise : forall v1 v2,
~ (value v1 \/ value v2) ->
~ (~ bvalue v1 /\ ~ bvalue v2) ->
eval tm_T tm_F.

### equality

• `reflexivity`
• `subst`
• `rewrite`
• `inversion` (on equalities)

If you have an equality in your context, there are several ways to substitute one side of the equality for the other in your goal or in other hypotheses.

If one side of the equality is a variable `x`, then the tactic `subst x` will replace all occurrences of `x` in the context and goal with the other side of the quality and will remove `x` from your context.

Use `reflexivity` to solve a goal of the form `e = e`.

```Lemma equality_example_1 : forall t1 t2 t3 u1 u2,
t1 = tm_isZ u1 ->
t2 = tm_S u2 ->
t3 = tm_S t2 ->
tm_if t1 t2 t3 =
tm_if (tm_isZ u1) (tm_S u2) (tm_S (tm_S u2)).
Proof.
intros t1 t2 t3 u1 u2 Heq1 Heq2 Heq3.
subst t1. subst t2. subst t3. reflexivity.
Qed.```

If neither side of the equality in your context is a variable (or if you don't want to discard the hypothesis), you can use the `rewrite` tactic to perform a substitution. The arrow after `rewrite` indicates the direction of the substitution. As demonstrated, you may perform rewriting in the goal or in a hypothesis.

```Lemma equality_example_2a : forall t u v,
tm_S t = tm_S u ->
eval (tm_S u) v ->
eval (tm_S t) v.
Proof.
intros t u v Heq He. rewrite -> Heq. apply He.
Qed.```
Lemma equality_example_2b : forall t u v, tm_S t = tm_S u -> eval (tm_S u) v -> eval (tm_S t) v. Proof. `intros t u v Heq He.` `rewrite <- Heq in He.` `apply He.` Qed. We also note that, analogously with `destruct`, we may use `rewrite` even with a hypothesis (or lemma) that has antecedents.
```Lemma equality_example_2c : forall t u v,
nvalue v ->
(nvalue v -> tm_S t = tm_S u) ->
eval (tm_S u) v ->
eval (tm_S t) v.
Proof.
`intros t u v Hnv Heq He. rewrite <- Heq in He.`
`apply He.`
`apply Hnv.`
Qed.```
If you need to derive additional equalities implied by an equality in your context (e.g., by the principle of constructor injectivity), you may use `inversion`. `inversion` is a powerful tactic that uses unification to introduce more equalities into your context. (You will observe that it also performs some substitutions in your goal.)
```Lemma equality_example_3 : forall t u,
tm_S t = tm_S u ->
t = u.
Proof.
`intros t u Heq. inversion Heq. reflexivity.`
Qed.```
```Lemma equality_exercise : forall t1 t2 t3 u1 u2 u3 u4,
tm_if t1 t2 t3 = tm_if u1 u2 u2 ->
tm_if t1 t2 t3 = tm_if u3 u3 u4 ->
t1 = u4.
`inversion` will also solve a goal when unification fails on a hypothesis. (Internally, Coq can construct a proof of `False` from contradictory equalities.)
```Lemma equality_example_4 :
tm_Z = tm_T ->
eval tm_T tm_F.
Proof.
intros Heq. inversion Heq.
Qed.```
Note: `e1 <> e2` is a notation for `~ e1 = e2`, i.e., the two are treated as syntactically equal.

Note: This is fairly trivial to prove if we have a size function on terms and some automation. With just the tools we have described so far, it requires just a little bit of work.

Hint: The proof requires induction on `t`. (This is the first example of induction on datatypes, but it is even more straightforward than induction on propositions.) In each case, unfold the negation, pull the equality into the context, and use `inversion` to eliminate contradictory equalities.

```Lemma succ_not_circular : forall t,
t <> tm_S t.

### inversion

• `inversion` (on propositions)
The `inversion` tactic also allows you to reason by inversion on an inductively defined proposition as in paper proofs: we try to match some proposition with the conclusion of each inference rule and only consider the cases (possibly none) where there is a successful unification. In those cases, we may use the premises of the inference rule in our reasoning.

Since `inversion` may generate many equalities between variables, it is useful to know that using `subst` without an argument will perform all possible substitutions for variables. It is a little difficult to predict which variables will be eliminated and which will be kept by this tactic, but this is a typical sort of trade-off when using powerful tactics.

(The use of `subst` in this proof is superfluous, but you can observe that it simplifies the context.)

```Lemma value_S_nvalue : forall t,
value (tm_S t) ->
nvalue t.
Proof.
`intros t H.`
`unfold value in H.`
`destruct H as [ H1 | H2 ].`

`inversion H1.`

`inversion H2. subst. apply H0.`
Qed.```
```Lemma inversion_exercise : forall t,
normal_form t ->
eval_many (tm_P t) tm_Z ->
nvalue t.
Proof.
By inversion on the `eval_many` relation, then conclusion
`eval_many (tm_P t) tm_Z` must have been derived by
the rule `m_step`, which means there is some `t'` for
which `eval (tm_P t) t'` and `eval_many t' tm_Z`.
Now, by inversion on the `eval` relation, there are only
three ways that `eval (tm_P t) t'` could have been
derived:
By `e_predZ`, with `t` and `t'` both being equal to `tm_Z`.
Our conclusion follows from `n_Z`.
By `e_predS`, with `t` being `tm_S t0` where we have
`nvalue t0`.
In this case, our conclusion is provable with `n_S`.
By `e_pred`, with `t` taking an evaluation step.
Thiscontradicts our assumption that `t` is a normal form (which can be shown
by using `destruct` on that assumption).

Tip: Nested patterns will be useful here.

```Lemma contradictory_equalities_exercise :
(exists t, exists u, exists v,
value t /\
t = tm_S u /\
u = tm_P v) ->
eval tm_T tm_F.
```Lemma eval_fact_exercise : forall t1 t2,
eval (tm_isZ (tm_P t1)) t2 ->
eval t2 tm_F ->
exists u, t1 = tm_S u.
```Lemma normal_form_if : forall t1 t2 t3,
normal_form (tm_if t1 t2 t3) ->
t1 <> tm_T /\ t1 <> tm_F /\ normal_form t1.

• `generalize dependent`
• `assert`
• `;`
• `clear`

Sometimes we need to have a tactic that moves hypotheses from our context back into our goal. Often this is because we want to perform induction in the middle of a proof and will not get a sufficiently general induction hypothesis without a goal of the correct form. (To be specific, if we need to have an induction hypothesis with a `forall` quantifier in front, then we must make sure our goal has a `forall` quantifier in front at the time we invoke the `induction` tactic.) Observe how ```generalize dependent``` achieves this in the proof below, moving the variable `t` and all dependent hypotheses back into the goal. You may want to remove the use of ```generalize dependent``` to convince yourself that it is performing an essential role here.

```Lemma value_is_normal_form : forall v,
value v ->
normal_form v.
Proof.
`intros v [ Hb | Hn ] [ t He ].`
`destruct Hb.`
`inversion He.`
`inversion He.`
`generalize dependent t. induction Hn.`
`intros t He. inversion He.`
`intros u He. inversion He. subst. destruct (IHHn t').`
`apply H0.`
Qed.```
Coq has many operations (called "tacticals") to combine smaller tactics into larger ones.

If `t1` and `t2` are tactics, then `t1; t2` is a tactic that executes `t1`, and then executes `t2` on subgoals left by or newly generated by `t1`. This can help to eliminate repetitious use of tactics. Two idiomatic uses are performing `subst` after `inversion` and performing `intros` after `induction`. More opportunities to use this tactical can usually be discovered after writing a proof. (It is worth noting that some uses of this tactical can make proofs less readable or more difficult to maintain. Alternatively, some uses can make proofs more readable or easier to maintain. It is always good to think about your priorities when writing a proof script.)

Revise the proof for `value_is_normal_form` to include uses of the `;` tactical.

Sometimes it is helpful to be able to use forward reasoning in a proof. One form of forward reasoning can be done with the tactic `assert`. `assert` adds a new hypothesis to the context but asks us to first justify it.

```Lemma nvalue_is_normal_form : forall v,
nvalue v ->
normal_form v.
Proof.
`intros v Hnv.`
`assert (value v) as Hv. right. apply Hnv.`
`apply value_is_normal_form. apply Hv.`
Qed.```
`assert` can also be supplied with a tactic that proves the assertion. We rewrite the above proof using this form.
```Lemma nvalue_is_normal_form' : forall v,
nvalue v ->
normal_form v.
Proof.
`intros v Hnv.`
`assert (value v) as Hv by (right; apply Hnv).`
`apply value_is_normal_form. apply Hv.`
Qed.```
The proof below introduces two new, simple tactics. First, the tactic `replace e1 with e2` performs a substitution in the goal and then requires that you prove `e2 = e1` as a new subgoal. This often allows us to avoid more cumbersome forms of forward reasoning. Second, the `clear` tactic discards a hypothesis from the context. Of course, this tactic is never needed, but it can be nice to use when there are complicated, irrelevant hypotheses in the context.
```Lemma single_step_to_multi_step_determinacy :
(forall t u1 u2, eval t u1 -> eval t u2 -> u1 = u2) ->
forall t v1 v2,
eval_many t v1 -> normal_form v1 ->
eval_many t v2 -> normal_form v2 ->
v1 = v2.
Proof.
`intros H t v1 v2 Hm1 Hnf1 Hm2 Hnf2. induction Hm1.`
`clear H. destruct Hm2.`
`reflexivity.`
`destruct Hnf1. exists t'. apply H.`
`destruct Hm2.`
`destruct Hnf2. exists t'. apply H0.`
`apply IHHm1; clear IHHm1.`
`apply Hnf1.`
`replace t' with t'0.`
`apply Hm2.`
`apply H with (t := t).`
`apply H1.`
`apply H0.`
Qed.```
This proof is lengthy and thus somewhat challenging. All of the techniques from this section will be useful; some will be essential. In particular, you will need to use `generalize dependent` at the beginning of the proof. You will find `assert` helpful in the cases where your assumptions are contradictory but none of them are in a negative form. In that situation, you can assert a negative statement that follows from your hypotheses (recall that `normal_form` is a negative statement). Finally, you will want to use the above lemma `nvalue_is_normal_form`. Good luck!
```Theorem eval_deterministic : forall t t' t'',
eval t t' ->
eval t t'' ->
t' = t''.
Prove the following lemmas. The last is quite long, and you may wish to wait until you know more about automation.
```Lemma f_eval_from_value : forall v w,
value v ->
f_eval v w ->
v = w.

Lemma eval_f_eval : forall t t' v,
eval t t' ->
f_eval t' v ->
f_eval t v.

Lemma f_eval_complete : forall t v,
value v ->
eval_many t v ->
f_eval t v.
```

### automation

• `eapply`, `esplit`
• `auto`, `eauto`
You can use `eapply e` instead of `apply e with (x := e1)`. This will generate subgoals containing unification variables that will get unified during subsequent uses of `apply`.
```Lemma m_if : forall t1 u1 t2 t3,
eval_many t1 u1 ->
eval_many (tm_if t1 t2 t3) (tm_if u1 t2 t3).
Proof.
`intros t1 u1 t2 t3 Hm. induction Hm.`
`apply m_refl.`
`eapply m_step.`
`apply e_if. apply H.`
`apply IHHm.`
Qed.```
You can use `esplit` to turn an existentially quantified variable in your goal into a unification variable.
```Lemma exists_P_zero :
exists u, eval (tm_P tm_Z) u.
Proof.
esplit. apply e_predZ.
Qed.```
The `auto` tactic solves goals that are solvable by any combination of
• `intros`
• `apply` (used on some local hypothesis)
• `split`, `left`, `right`
• `reflexivity`
If `auto` cannot solve the goal, it will leave the proof state completely unchanged (without generating any errors).

The lemma below is a proposition that has been contrived for the sake of demonstrating the scope of the `auto` tactic and does not say anything of practical interest. So instead of thinking about what it means, you should think about the operations that `auto` had to perform to solve the goal.

Note: It is important to remember that `auto` does not destruct hypotheses! There are more advanced forms of automation available that do destruct hypotheses in some specific ways.

```Lemma auto_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
(forall u, eval t t' -> eval t' u -> eval_many t u) ->
eval t' t \/ t = t /\ eval_many t t''.
Proof.
`auto.`
Qed.```
The `eauto` tactic solves goals that are solvable by some combination of
• `intros`
• `eapply` (used on some local hypothesis)
• `split`, `left`, `right`
• `esplit`
• `reflexivity`
This lemma has two significantly differences from the previous one, both of which render `auto` useless.
```Lemma eauto_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
(forall u, eval t u -> eval u t'' -> eval_many t t'') ->
eval t' t \/ (exists u, t = u) /\ eval_many t t''.
Proof.
`eauto.`
Qed.```
You can enhance `auto` (or `eauto`) by appending ```using x_1, ..., x_n```, where each `x_i` is the name of some constructor or lemma. Then `auto` will attempt to apply those constructors or lemmas in addition to the assumptions in the local context.
```Lemma eauto_using_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
eval t' t \/ t = t /\ eval_many t t''.
Proof.
eauto using m_step, m_one.
Qed.```
Go back and rewrite your proofs for `m_one`, `m_two`, and `m_iftrue_step`. You should be able to make them very succinct given what you know now.

See how short you can make these proofs.

Note: This is an exercise. We are not making the claim that shorter proofs are necessarily better!

Hint: Remember that we can connect tactics in sequence with `;`. However, as you can imagine, figuring out the best thing to write after a `;` usually involves some trial and error.

```Lemma pred_not_circular : forall t,
t <> tm_P t.
```Lemma m_succ : forall t u,
eval_many t u ->
eval_many (tm_S t) (tm_S u).
```Lemma m_pred : forall t u,
eval_many t u ->
eval_many (tm_P t) (tm_P u).
Go back and rewrite your proofs for `m_trans` and `two_values`. Pulling together several tricks you've learned, you should be able to prove `two_values` in one (short) line.

Sometimes there are lemmas or constructors that are so frequently needed by `auto` that we don't want to have to add them to our `using` clause each time. Coq allows us to request that certain propositions that always be considered by `auto` and `eauto`.

The following command adds four lemmas to the default search procedure of `auto`. Hint Resolve m_if m_succ m_pred m_iszero.

Constructors of inductively defined propositions are some of the most frequently needed by `auto`. Instead of writing

```    Hint Resolve b_T b_F.
```
we may simply write
```    Hint Constructors bvalue.
```
Let's add all our constructors to `auto`.

Hint Constructors bvalue nvalue eval eval_many.

By default `auto` will never try to unfold definitions to see if a lemma or constructor can be applied. With the `Hint Unfold` command, we can instruct `auto` to try unfold definitions in the goal as it is working.

Hint Unfold value normal_form.

There are a few more variants on the `Hint` command that can be used to further customize `auto`. You can learn about them in the Coq reference manual.

### Functions and Conversion

• `Fixpoint/struct`
• `match ... end`
• `if ... then ... else ...`
• `simpl`
• `remember`
We can define simple (non-recursive) functions from one datatype to another using the `Definition` keyword. The `match` construct allows us to do case analysis on a datatype. The `match` expression has a first-match semantics and allows nested patterns; however, Coq's type checker demands that pattern-matching be exhaustive.

Coq also has an `if/then/else` expression. It can be used, not just with the type `bool` but, in fact, with any datatype having exactly two constructors (the first constructor corresponding to the `then` branch and the second to the `else` branch). Thus, we can define a function `is_bool` as below.

```Definition is_bool (t : tm) : bool :=
if tm_to_bool t then true else false.```
Write a function `interp : tm -> tm` that returns the normal form of its argument according to the small-step semantics given by `eval`.

Hint: You will want to use `tm_to_nat` (or another auxiliary function) to prevent stuck terms from stepping in the cases `e_predS` and `e_isZS`.

The tactic `simpl` (recursively) reduces the application of a function defined by pattern-matching to an argument with a constructor at its head. You can supply `simpl` with a particular expression if you want to prevent it from simplifying elsewhere.

```Lemma bool_tm_bool : forall b,
tm_to_bool (bool_to_tm b) = some_bool b.
Proof.
`intros b. destruct b.`
`simpl (bool_to_tm true). simpl. reflexivity.`
`reflexivity.`
Qed.```
We can also apply the tactic `simpl` in our hypotheses.
```Lemma tm_bool_tm :forall t b,
tm_to_bool t = some_bool b ->
bool_to_tm b = t.
Proof.
`intros t b Heq. destruct t.`
`simpl in Heq. inversion Heq.`
`simpl. reflexivity.`
`inversion Heq. reflexivity.`
`simpl in Heq. inversion Heq.`
`inversion Heq.`
`inversion Heq.`
`inversion Heq.`
`inversion Heq.`
Qed.```
```Lemma tm_to_bool_dom_includes_bvalue : forall bv,
bvalue bv -> exists b, tm_to_bool bv = some_bool b.
```Lemma tm_to_bool_dom_only_bvalue : forall bv b,
tm_to_bool bv = some_bool b -> bvalue bv.

Not all uses of `simpl` are optional. Sometimes they are necessary so that we can use the `rewrite` tactic. Observe, also, how using `rewrite` can automatically trigger a reduction if it creates a redex.

```Lemma nat_tm_nat : forall n,
tm_to_nat (nat_to_tm n) = some_nat n.
Proof.
`intros n. induction n.`
`reflexivity.`
`bsimpl. rewrite -> IHn.`
`reflexivity.`
Qed.```
Here's an example where it is necessary to use `simpl` on a hypothesis. To trigger a reduction of a `match` expression in a hypothesis, we use the `destruct` tactic on the expression being matched.
```Lemma tm_nat_tm : forall t n,
tm_to_nat t = some_nat n ->
nat_to_tm n = t.
Proof.
`intros t. induction t; intros n Heq.`
`inversion Heq.`
`inversion Heq.`
`inversion Heq.`
`inversion Heq. reflexivity.`
`simpl in Heq. destruct (tm_to_nat t).`
`inversion Heq. simpl. rewrite -> IHt.`
`reflexivity.`
`reflexivity.`
`inversion Heq.`
`inversion Heq.`
`inversion Heq.`
Qed.```
```Lemma tm_to_nat_dom_includes_nvalue : forall v,
nvalue v -> exists n, tm_to_nat v = some_nat n.
```Lemma tm_to_nat_dom_only_nvalue : forall v n,
tm_to_nat v = some_nat n -> nvalue v.
Using the tactic `destruct` (or `induction`) on a complex expression (i.e., one that is not simply a variable) may not leave you with enough information for you to finish the proof. The tactic `remember` can help in these cases. Its usage is demonstrated below. If you are curious, try to finish the proof without `remember` to see what goes wrong.
```Lemma remember_example : forall v,
eval_many
(tm_P (tm_S v))
(match tm_to_nat v with
| some_nat _ => v
| no_nat => tm_P (tm_S v)
end).
Proof.
`intros v. remember (tm_to_nat v) as x. destruct x.`
`apply m_one. apply e_predS.`
`eapply tm_to_nat_dom_only_nvalue.`
`rewrite <- Heqx. reflexivity.`
`apply m_refl.`
Qed.```
Prove the following lemmas involving the function `interp` from a previous exercise:
```Lemma interp_reduces : forall t,
eval_many t (interp t).

Lemma interp_fully_reduces : forall t,
normal_form (interp t).
```