by Aaron Bohannon and Yves Bertot, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic
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 *)
_ 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
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
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"
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
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
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
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
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.
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
Set to Prop unit to True tt to Iyou get the definition of [True] from the Coq stdlib
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
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
Coq < Check Empty. Empty : Set Coq < Definition e2u (e : Empty) : unit := match e with end. e2u is defined
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.
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 ."
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
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
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
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.
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
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>
you define n-ary relations in Coq by giving a set of inference rules
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 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).
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}
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 tapply 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
eval k (tm_S t)
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)
e_S_P_S
, to show eval (tm_S (tm_P (tm_S t))) (tm_S t)
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)
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 kintros t k Hd He.
t, k : tm Hd : strongly_diverges t He : eval t k ============================ strongly_diverges kunfold strongly_diverges.
t, k : tm Hd : strongly_diverges t He : eval t k ============================ forall u : tm, eval_many k u -> ~ normal_form uintros u Hm.
t, k : tm Hd : strongly_diverges t He : eval t k u : tm Hm : eval_many k u ============================ ~ normal_form uunfold 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 uapply 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 uapply 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 uapply 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 uapply Hm.
No more subgoals. Qed.
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 t2intros t0 t1 t2 H.
t0, t1, t2 : tm H : eval t0 t1 /\ eval t1 t2 ============================ eval_many t0 t2destruct H as [ He1 He2 ].
t0, t1, t2 : tm He1 : eval t0 t1 He2 : eval t1 t2 ============================ eval_many t0 t2apply m_two with (t2 := t1).
t0, t1, t2 : tm He1 : eval t0 t1 He2 : eval t1 t2 ============================ eval t0 t1 eval t1 t2apply He1.
t0, t1, t2 : tm He1 : eval t0 t1 He2 : eval t1 t2 ============================ eval t1 t2apply 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 t3intros t0 t1 t2 t3 H.
t0, t1, t2, t3 : tm H : eval t0 t1 /\ eval t1 t2 /\ eval t2 t3 ============================ eval_many t0 t3destruct 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 t3apply 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 t3apply He1.
t0, t1, t2, t3 : tm He1 : eval t0 t1 He2 : eval t1 t2 He3 : eval t2 t3 ============================ eval_many t1 t3apply 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 t3apply He2.
t0, t1, t2, t3 : tm He1 : eval t0 t1 He2 : eval t1 t2 He3 : eval t2 t3 ============================ eval t2 t3apply 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 knowvalue t
andvalue u
, which means eitherbvalue t
ornval t
, and eitherbvalue u
ornval u
. Consider the case in whichbvalue t
holds. Then one of the disjuncts of our conclusion is proved. Next, consider the case in whichnval t
holds. Now consider the subcase wherebvalue 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.
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 ofeval_many t t1
. Casem_refl
: Sincet
andt1
must be the same, our conclusion holds by assumption. Casem_step
: Now let's rename thet1
from the lemma statement tou0
(as Coq likely will) and observe that there must be somet1
(from above the line of them_step
rule) such thateval t t1
andeval_many t1 u0
. Our conclusion follows from from an application ofm_step
with our newt1
and our induction hypothesis, which allows us to piece togethereval_many t1 u0
andeval_many u0 u
to geteval_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 /\ Qthen 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.
exists
destruct
(for existential propositions)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.
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.
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.
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.
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 somenv
such thatnvalue nv
. Consider the case wherenv
istm_Z
. Then choosebv
to betm_T
. Bym_trans
, we can show thateval_many (tm_isZ t) tm_T
by showingeval_many (tm_isZ t) (tm_isZ tm_Z)
andeval_many (tm_isZ tm_Z) tm_T
. The former follows fromm_iszero
and our assumption. The latter follows fromm_one
and the rulee_isZZ
. On the other hand, in the case wherenv
is built fromtm_succ
, we choosebv
to betm_F
and the proof follows similarly.Admitted.
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. Proof. Admitted.
Lemma normal_form_from_forall : forall t, (forall u, ~ eval t u) -> normal_form t. Proof. Admitted.
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.
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.
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.
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.
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.
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
(on propositions)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 theeval_many
relation, then conclusioneval_many (tm_P t) tm_Z
must have been derived by the rulem_step
, which means there is somet'
for whicheval (tm_P t) t'
andeval_many t' tm_Z
. Now, by inversion on theeval
relation, there are only three ways thateval (tm_P t) t'
could have been derived:
e_predZ
, with t
and t'
both being equal to tm_Z
.
Our conclusion follows from n_Z
.
e_predS
, with t
being tm_S t0
where we have
nvalue t0
.
In this case, our conclusion is provable with n_S
.
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.
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.
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.
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.
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.
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.
eapply
, esplit
auto
, eauto
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.
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.
auto
tactic solves goals that are solvable by any
combination of
intros
apply
(used on some local hypothesis)split
, left
, right
reflexivity
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.
eauto
tactic solves goals that are solvable by some
combination of
intros
eapply
(used on some local hypothesis)split
, left
, right
esplit
reflexivity
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.
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.
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.
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.
Fixpoint/struct
match ... end
if ... then ... else ...
simpl
remember
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.
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.
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.
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.
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.
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).