Coq学习——《SoftwareFoundation》Volume1.7IndProp
IndProp
We have seen several ways of writing propositions (conjunction, disjunction, and existential quantification) In this chapter, we bring yet another new tool in to the mix: inductive definitions.
Uses an inductive definition of “evenness” as a running example.
In past chapters, we have two ways to say [n] is even:
 [evenb n = true]
 [exists k, n = double k]
Yet another possibility is to say that [n] is even if we can establish its evenness from the following rules:
 Rule [ev_0]: The number [0] is even.
 Rule [ev_SS]: If [n] is even, then [S (S n)] is even.
Inductive Definition of Evenness
1 

Different from previous uses of [Inductive]. Neither a [Type] (like [nat]) nor a function yielding a [Type] (like [list]).
We define a function from [nat] to [Prop]. That is, a property of numbers!
In contrast, recall the definition of [list]:
1 

Notice the “parameter” on the left of the colon and “index” (or “annotation”) on the right.
Inversion on Evidence
destruct [ev n] directly.
1 

When the goal relates to [n] but we destruct H with S(n) or S(S(n)), we can two ways to prove.
 with the help of [ev_inversion] theorem proven before.
 use [remember] tactic.
Note how both proofs produce two subgoals, which correspond to the two ways of proving [ev]. The first subgoal is a contradiction that is discharged with [discriminate]. The second subgoal makes use of [injection] and [rewrite]. Coq provides a handy tactic called [inversion] that factors out that common pattern.
The [inversion] tactic can detect:
 that the first case ([n = 0]) does not apply and
2 .that the [n’] that appears in the [ev_SS] case must be the same as [n].
It has an “[as]” variant similar to [destruct], allowing us to assign names rather than have Coq choose them.
1 

The [inversion] tactic does quite a bit of work. destruct, injection …
When [inversion H]. Generate subgoals which [H] has been replaced by exact contexts. Then [inversion] will throw those selfcontradictionory subgoals away. Details follows:
Here’s how [inversion] works in general. Suppose the name [H] refers to an assumption [P] in the current context, where [P] has been defined by an [Inductive] declaration. Then, for each of the constructors of [P], [inversion H] generates a subgoal in which [H] has been replaced by the exact, specific conditions under which this constructor could have been used to prove [P]. Some of these subgoals will be selfcontradictory; [inversion] throws these away. The ones that are left represent the cases that must be proved to establish the original goal. For those, [inversion] adds all equations into the proof context that must hold of the arguments given to [P] (e.g., [S (S n’) = n] in the proof of [evSS_ev]).
Induction on Evidence
Just as induction on data, when we inversion construct evidence and get stuck like prove another instance of the same theorem we set out to prove, we can consider use induction on evidence.
This time we can get a useful hypothesis related to the other instance of n.
1 

Inductive Relations
A oneargument proposition can be thought of as a property. A twoargument proposition can be thought of as a relation.
1 

本博客所有文章除特别声明外，均采用 CC BYSA 4.0 协议 ，转载请注明出处！