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
       comments
    *)

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

but you cannot save/load except copy-pasting from/to your terminal

   Check
   Print
   About
   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:


Set, Prop and Type

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

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 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.add	 	
    _ - _	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
head	        first element (with default)
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


    ADT

    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 tms. 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.
    Admitted.
    

    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. ...
     Admitted.

    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.
     Admitted. 

    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

    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.
    Proof. Admitted.
    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
          follows similarly.Admitted.


    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.
    Proof. Admitted.
    Lemma normal_form_from_forall : forall t,
      (forall u, ~ eval t u) ->
      normal_form t.
    Proof. Admitted.
    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.
    Proof. Admitted. 


    equality

    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.
    Proof. Admitted.
    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.
    Proof. Admitted.


    inversion

    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). Admitted.
  • 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.
    Proof. Admitted. 
    Lemma eval_fact_exercise : forall t1 t2,
      eval (tm_isZ (tm_P t1)) t2 ->
      eval t2 tm_F ->
      exists u, t1 = tm_S u.
    Proof. Admitted.
    Lemma normal_form_if : forall t1 t2 t3,
      normal_form (tm_if t1 t2 t3) ->
      t1 <> tm_T /\ t1 <> tm_F /\ normal_form t1.
    Proof. Admitted.


    additional tactics

    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''.
    Proof. Admitted.
    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

    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 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 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.
    Proof. Admitted.
    Lemma m_succ : forall t u,
      eval_many t u ->
      eval_many (tm_S t) (tm_S u).
    Proof. Admitted.
    Lemma m_pred : forall t u,
      eval_many t u ->
      eval_many (tm_P t) (tm_P u).
    Proof. Admitted.
    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

    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.
    Proof. Admitted.
    Lemma tm_to_bool_dom_only_bvalue : forall bv b,
      tm_to_bool bv = some_bool b -> bvalue bv.
    Proof. Admitted.

    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.
    Proof. Admitted.
    Lemma tm_to_nat_dom_only_nvalue : forall v n,
      tm_to_nat v = some_nat n -> nvalue v.
    Proof. Admitted.
    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).