...whichcorrespondsto"proof by case analysis"inclassicalmath.Fornon-recursiveinductivetypes,thetwotacticswillalwayshaveidenticalbehavior.Oftencaseanalysisissufficient,eveninproofsaboutrecursivetypes,anditisnicetoavoidintroducingunneededinductionhypotheses.
%\noindent%...whichcorrespondsto"proof by case analysis"inclassicalmath.Fornon-recursiveinductivetypes,thetwotacticswillalwayshaveidenticalbehavior.Oftencaseanalysisissufficient,eveninproofsaboutrecursivetypes,anditisnicetoavoidintroducingunneededinductionhypotheses.
Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B
Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B
For conj: Arguments A, B are implicit
For conj: Arguments A, B are implicit
For and: Argument scopes are [type_scope type_scope]
For and: Argument scopes are [type_scope type_scope]
For conj: Argument scopes are [type_scope type_scope _ _]
For conj: Argument scopes are [type_scope type_scope _ _]
]]
]]
In addition to the definition of [and] itself, we get information on implicit arguments and parsing rules for [and] and its constructor [conj]. We will ignore the parsing information for now. The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments.
In addition to the definition of [and] itself, we get information on implicit arguments and parsing rules for [and] and its constructor [conj]. We will ignore the parsing information for now. The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments.
...
@@ -935,15 +922,14 @@ Section nat_tree_ind'.
...
@@ -935,15 +922,14 @@ Section nat_tree_ind'.
(** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.
(** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.
[[
[[
Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
match tr return (P tr) with
match tr with
| NLeaf' => NLeaf'_case
| NLeaf' => NLeaf'_case
| NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls)
| NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls)
end
end
with list_nat_tree_ind (ls : list nat_tree) : All P ls :=
with list_nat_tree_ind (ls : list nat_tree) : All P ls :=
Coq rejects this definition, saying "Recursivecalltonat_tree_ind'hasprincipalargumentequalto"tr"insteadofrest." The term "nestedinductivetype" hints at the solution to the problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
Coq rejects this definition, saying "Recursivecalltonat_tree_ind'hasprincipalargumentequalto"tr"insteadofrest." The term "nestedinductivetype" hints at the solution to the problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
match tr return (P tr) with
match tr with
| NLeaf' => NLeaf'_case
| NLeaf' => NLeaf'_case
| NNode' n ls => NNode'_case n ls
| NNode' n ls => NNode'_case n ls
((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
(** Notice that Coq was smart enough to expand the definition of [map] to verify that we are using proper nested recursion, even through a use of a higher-order function. *)
(** Notice that Coq was smart enough to expand the definition of [map] to verify that we are using proper nested recursion, even through a use of a higher-order function. *)
(** We know that the standard induction principle is insufficient for the task, so we need to provide a [using] clause for the [induction] tactic to specify our alternate principle. *)
(** We know that the standard induction principle is insufficient for the task, so we need to provide a [using] clause for the [induction] tactic to specify our alternate principle. *)
After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *)
After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *)
...
@@ -1062,24 +1049,25 @@ The advantage of using the hint is not very clear here, because the original pro
...
@@ -1062,24 +1049,25 @@ The advantage of using the hint is not very clear here, because the original pro
(** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *)
(** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *)
Theorem true_neq_false : true <> false.
Theorem true_neq_false : true <> false.
(* begin thide *)
(* begin thide *)
(** We begin with the tactic [red], which is short for "onestepofreduction," to unfold the definition of logical negation. *)
(** We begin with the tactic [red], which is short for "onestepofreduction," to unfold the definition of logical negation. *)
red.
red.
(** [[
(** [[
============================
============================
true = false -> False
true = false -> False
]]
]]
The negation is replaced with an implication of falsehood. We use the tactic [intro H] to change the assumption of the implication into a hypothesis named [H]. *)
The negation is replaced with an implication of falsehood. We use the tactic [intro H] to change the assumption of the implication into a hypothesis named [H]. *)
intro H.
intro H.
(** [[
(** [[
H : true = false
H : true = false
============================
============================
False
False
]]
]]
This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *)
This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *)
...
@@ -1090,30 +1078,30 @@ This is the point in the proof where we apply some creativity. We define a func
...
@@ -1090,30 +1078,30 @@ This is the point in the proof where we apply some creativity. We define a func
change (f false).
change (f false).
(** [[
(** [[
H : true = false
H : true = false
============================
============================
f false
f false
]]
]]
Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side. *)
Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side. *)
rewrite <- H.
rewrite <- H.
(** [[
(** [[
H : true = false
H : true = false
============================
============================
f true
f true
]]
]]
We are almost done. Just how close we are to done is revealed by computational simplification. *)
We are almost done. Just how close we are to done is revealed by computational simplification. *)
