## Inductively Defined Propositions

### The 3rd way to state Evenness…

Besides:

1
2
3

Theorem even_bool_prop : ∀n,
evenb n = true ↔ ∃k, n = double k.
(*bool*) (*prop*)

we can write an *Inductive definition* of the `even`

property!

### Inference rules

In CS, we often uses *inference rules*

1
2
3

ev n
---- ev_0 ------------ ev_SS
ev 0 ev (S (S n))

and *proof tree* (i.e. evidence), there could be multiple premieses to make it more tree-ish.

1
2
3
4
5
6

---- ev_0
ev 0
---- ev_SS
ev 2
---- ev_SS
ev 4

So we can literally translate them into a GADT:

### Inductive Definition of Evenness

1
2
3
4
5
6

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS : ∀n, even n → even (S (S n)).
Check even_SS.
(* ==> : forall n : nat, even n -> even (S (S n)) *)

There are two ways to understand the `even`

here:

### 1. A Property of `nat`

and two theorems (Intuitively)

the thing we are defining is not a

`Type`

, but rather a function`nat -> Prop`

— i.e., a property of numbers.

we have two ways to provide an evidence to show the `nat`

is `even`

, either or:

- it’s
`0`

, we can immediately conclude it’s`even`

. - for any
`n`

, if we can provide a evidence that`n`

is`even`

, then`S (S n)`

is`even`

as well.

We can think of the definition of

`even`

as defining a Coq property`even : nat → Prop`

, together with primitive theorems`ev_0 : even 0`

and`ev_SS : ∀ n, even n → even (S (S n))`

.

### 2. An “Indexed” GADT and two constructors (Technically)

In an Inductive definition, an argument to the type constructor on the left of the colon is called a “parameter”, whereas an argument on the right is called an “index”. – “Software Foundaton”

Considered a “parametrized” ADT such as the polymorphic list,

1
2
3
4
5

Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X).
Check list. (* ===> list : Type -> Type *)

where we defined type con `list : Type -> Type`

, by having a type var `X`

in the left of the `:`

.
the `X`

is called a *parameter* and would be *parametrized i.e. substituted, globally*, in constructors.

Here, we write `nat`

in the right of the `:`

w/o giving it a name (to refer and to substitute),
which allows the `nat`

taking different values in different constructors (as constraints).
it’s called an *index* and will form a family of type indexed by `nat`

(to type check?)

From this perspective, there is an alternative way to write this GADT:

1
2
3

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

we have two ways to construct the `even`

type (`Prop <: Type`

), either or:

`ev_0`

takes no argument, so simply instantiate`even`

with`nat`

0`ev_SS`

takes a`nat`

`n`

and a`H`

typed`even n`

,- the
*dependency*between two arguments thus established! - as long as the
*constraint on same*is fullfilled, we can build type`n`

`even`

with`S (S n)`

- the

The take way is that *dependent type (Pi-type)* allow us to constriant constructors with different values.

indexedway is more general. it formed a larger type, and is only used when extra power needed. every parametrized one can be represented as indexed one (it’s just that index happended to be the same)

### “Constructor Theorems”

Such “constructor theorems” have the same status as proven theorems. In particular, we can use Coq’s

`apply`

tactic with the rule names to prove`even`

for particular numbers…

1
2

Theorem ev_4 : even 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Proof States Transition:

1
2
3
4
5
6
7

even 4
------ apply ev_SS.
even 2
------ apply ev_SS.
even 0
------ apply ev_0.
Qed.

I believed what `apply`

do is trying to *backward reasoning*, i.e. matching the goal and leave the “evidence” need to be proved (to conclude the goal).

we can write it as normal function application syntax w/o using tactics like other Dependent-typed PL as well

1
2

Theorem ev_4' : even 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

## Using Evidence in Proofs

Besides

constructing evidencethat numbers are even, we can alsoreasonabout such evidence.

Introducing

`even`

with an`Inductive`

declaration tells Coq that these two constructors are theonlyways to build evidence that numbers are`even`

.

In other words, if someone gives us evidence

`E`

for the assertion`even n`

, then we know that`E`

must have one of two shapes

This suggests that it should be possible to analyze a hypothesis of the form

`even n`

muchas we do inductively defined data structures; in particular, it should be possible to argue byinductionandcase analysison such evidence.

This starts to get familiar as what we did for many calculi, ranging from Logics to PLT.
This is called the **Inversion property**.

### Inversion on Evidence

We can prove the inersion property by ourselves:

1
2
3
4
5
6
7
8
9

Theorem ev_inversion :
∀(n : nat), even n →
(n = 0) ∨ (∃n', n = S (S n') ∧ even n').
Proof.
intros n E.
destruct E as [ | n' E'].
- (* E = ev_0 : even 0 *) left. reflexivity.
- (* E = ev_SS n', E' : even (S (S n')) *) right. ∃n'. split. reflexivity. apply E'.
Qed.

But Coq provide the `inversion`

tactics that does more! (not always good tho, too automagical)

The inversion tactic does quite a bit of work. When applied to equalities, as a special case, it does the work of both

`discriminate`

and`injection`

. In addition, it carries out the`intros`

and`rewrite`

s

Here’s how inversion works in general. Suppose the name

`H`

refers to an assumption`P`

in the current context,where. Then, for each of the constructors of`P`

has been defined by an`Inductive`

declaration`P`

,`inversion H`

generates a subgoal in which`H`

has been replaced by theexact, specific conditions under which this constructor could have been used to prove. Some of these subgoals will be self-contradictory; 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`

`P`

(e.g.,`S (S n') = n`

in the proof of`evSS_ev`

). (`9-proof-object.md`

has a better explaination on`inversion`

)

`inversion`

is a specific use upon `destruct`

(both do case analysis on constructors), but many property need `induction`

!.
By `induction (even n)`

, we have cases and subgoals splitted, and induction hypothesis as well.

### Induction on Evidence

Similar to induction on inductively defined data such as `list`

:

To prove a property of (for any

`X`

)`list X`

holds, we can use`induction`

on`list X`

. To prove a property of`n`

holds for all numbers for which`even n`

holds, we can use`induction`

on`even n`

.

#### Notes on induction

*The principle of induction* is to prove `P(n-1) -> P(n)`

(多米诺) for some (well-founded partial order) set of `n`

.

Here, we are induction over “the set of numbers fullfilling the property `even`

”.
Noticed that we r proving things over this set, meaning we already have it (i.e. a proof, or a evidence) in premises, instead of proving the `even`

ness of the set.

#### Proof by Mathematical Induction is Deductive Reasoning

“Proof by induction,” despite the name, is deductive. The reason is that proof by induction does not simply involve “going from many specific cases to the general case.” Instead, in order for proof by induction to work, we need a deductive proof that each specific case implies the next specific case. Mathematical induction is not philosophical induction.

https://math.stackexchange.com/a/1960895/528269

Mathematical induction is an inference rule used in formal proofs. Proofs by mathematical induction are, in fact, examples of deductive reasoning. Equivalence with the well-ordering principle: The principle of mathematical induction is usually stated as an axiom of the natural numbers; see Peano axioms. However, it can be proved from the well-ordering principle. Indeed, suppose the following:

https://en.wikipedia.org/wiki/Mathematical_induction

#### Also, Structual Induction is one kind of Math. Induction

和标准的数学归纳法等价于良序原理一样，结构归纳法也等价于良序原理。

…A

well-foundedpartial orderis defined on the structures… …Formally speaking, this then satisfies the premises of anaxiom of well-founded induction…

https://en.wikipedia.org/wiki/Structural_induction

In terms of Well-ordering and Well-founded:

If the set of all structures of a certain kind admits a well-founded partial order, then every nonempty subset must have a minimal element. (This is the definition of “well-founded”.) 如果某种整个结构的集容纳一个良基偏序， 那么每个非空子集一定都含有最小元素。（其实这也是良基的定义

## Inductive Relations

Just as a single-argument proposition defines a *property*, 性质
a two-argument proposition defines a *relation*. 关系

1
2
3
4
5

Inductive le : nat → nat → Prop :=
| le_n n : le n n
| le_S n m (H : le n m) : le n (S m).
Notation "n ≤ m" := (le n m).

It says that there are two ways to

give evidencethat one number is less than or equal to another:

- either same number
- or give evidence that
`n ≤ m`

then we can have`n ≤ m + 1`

.

and we can use the same tactics as we did for properties.

## Slide Q&A - 1

- First
`destruct`

`even n`

into 2 cases, then`discriminate`

on each.

Another way…
rewriting `n=1`

on `even n`

. It won’t compute `Prop`

, but `destruct`

can do some `discriminate`

behind the scene.

## Slide Q&A - 2

`inversion`

and `rewrite plus_comm`

(for `n+2`

)

`destruct`

vs. `inversion`

vs. `induction`

.

`destruct`

,`inversion`

,`induction`

(on general thing)… similar/specialized version of each…

Trying to internalize this concept better: *When to use which?*

For any inductively defined proposition (`<: Type`

) in hypothesis:
meaning from type perspective, it’s already a “proper type” (`::*`

)

1

Inductive P = C1 : P1 | C2 : A2 -> P2 | ...

`destruct`

case analysis on inductive type

- simply give you each cases, i.e. each constructors.
- we can destruct on
`a =? b`

since`=?`

is inductively defined.

`induction`

use induction principle

- proving
`P`

holds for all base cases - proving
`P(n)`

holds w/`P(n-1)`

for all inductive cases (`destruct`

stucks in this case because of no induction hypothesis gained from induction principle)

`inversion`

invert the conclusion and give you all cases with premises of that case.

For GADT, i.e. “indexed” `Prop`

(property/relation), `P`

could have many shape
`inversion`

give you `Ax`

for shape `P`

assuming built with `Cx`

`inversion`

discards cases when shape `P != Px`

.
(`destruct`

stucks in this case because of no equation gained from inversion lemma)

## Case Study: Regular Expressions

### Definition

*Definition of RegExp in formal language can be found in FCT/CC materials*

1
2
3
4
5
6
7

Inductive reg_exp {T : Type} : Type :=
| EmptySet (* ∅ *)
| EmptyStr (* ε *)
| Char (t : T)
| App (r1 r2 : reg_exp) (* r1r2 *)
| Union (r1 r2 : reg_exp) (* r1 | r2 *)
| Star (r : reg_exp). (* r* *)

Note that this definition is

polymorphic. We depart slightly in thatwe do not require the type. (difference not significant here)`T`

to be finite

`reg_exp T`

describestringswith characters drawn from`T`

— that is,lists of elements of.`T`

### Matching

The matching is somewhat similar to *Parser Combinator* in Haskell…

e.g.
`EmptyStr`

matches `[]`

`Char x`

matches `[x]`

we definied it into an

`Inductive`

relation (can be displayed asinference-rule). somewhat type-level computing !

1
2
3
4
5
6
7
8
9
10

Inductive exp_match {T} : list T → reg_exp → Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar x : exp_match [x] (Char x)
| MApp s1 re1 s2 re2
(H1 : exp_match s1 re1)
(H2 : exp_match s2 re2) :
exp_match (s1 ++ s2) (App re1 re2)
(** etc. **)
Notation "s =~ re" := (exp_match s re) (at level 80). (* the Perl notation! *)

## Slide Q&A - 3

The lack of rule for `EmptySet`

(“negative rule”) give us what we want as PLT

`Union`

and `Star`

.

the informal rules for

`Union`

and`Star`

correspond totwo constructorseach.

1
2
3
4
5
6
7
8
9
10
11

| MUnionL s1 re1 re2
(H1 : exp_match s1 re1) :
exp_match s1 (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : exp_match s2 re2) :
exp_match s2 (Union re1 re2)
| MStar0 re : exp_match [] (Star re)
| MStarApp s1 s2 re
(H1 : exp_match s1 re)
(H2 : exp_match s2 (Star re)) :
exp_match (s1 ++ s2) (Star re).

Thinking about their *NFA*: they both have non-deterministic branches!
The recursive occurrences of `exp_match`

gives as *direct argument* (evidence) about which branches we goes.

we need some

sanity checksince Coq simply trust what we declared… that’s why there is even Quick Check for Coq.

### Direct Proof

In fact, `MApp`

is also non-deterministic about how does `re1`

and `re2`

collaborate…
So we have to be explicit:

1
2
3
4

Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
apply (MApp [1] _ [2]).
...

### Inversion on Evidence

This, if we want to prove via `destruct`

,
we have to write our own *inversion lemma* (like `ev_inversion`

for `even`

).
Otherwise we have no equation (which we should have) to say `contradiction`

.

1
2
3
4

Example reg_exp_ex3 : ~ ([1; 2] =~ Char 1).
Proof.
intros H. inversion H.
Qed.

### Manual Manipulation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Lemma MStar1 :
forall T s (re : @reg_exp T) ,
s =~ re ->
s =~ Star re.
Proof.
intros T s re H.
rewrite <- (app_nil_r _ s). (* extra "massaging" to convert [s] => [s ++ []] *)
apply (MStarApp s [] re). (* to the shape [MStarApp] expected thus can pattern match on *)
(* proving [MStarApp] requires [s1 s2 re H1 H2]. By giving [s [] re], we left two evidence *)
| MStarApp s1 s2 re
(H1 : exp_match s1 re)
(H2 : exp_match s2 (Star re)) :
exp_match (s1 ++ s2) (Star re).
- apply H. (* evidence H1 *)
- apply MStar0. (* evidence H2 *)
Qed. (* the fun fact is that we can really think the _proof_
as providing evidence by _partial application_. *)

### Induction on Evidence

By the recursive nature of

`exp_match`

, proofs will often require induction.

1
2
3
4
5
6
7
8
9
10

(** Recursively collecting all characters that occur in a regex **)
Fixpoint re_chars {T} (re : reg_exp) : list T :=
match re with
| EmptySet ⇒ []
| EmptyStr ⇒ []
| Char x ⇒ [x]
| App re1 re2 ⇒ re_chars re1 ++ re_chars re2
| Union re1 re2 ⇒ re_chars re1 ++ re_chars re2
| Star re ⇒ re_chars re
end.

The proof of `in_re_match`

went through by `inversion`

on relation `s =~ re`

. (which gives us all 7 cases.)
The interesting case is `MStarApp`

, where the proof tree has two *branches* (of premises):

1
2
3

s1 =~ re s2 =~ Star re
--------------------------- (MStarApp)
s1 ++ s2 =~ Star re

So by induction on the relation (rule), we got *two induction hypotheses*!
That’s what we need for the proof.

## The `remember`

tactic (Induction on Evidence of A Specific Case)

One interesting/confusing features is that `induction`

over a term that’s *insuffciently general*. e.g.

1
2
3
4
5
6

Lemma star_app: ∀T (s1 s2 : list T) (re : @reg_exp T),
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.

Here, we know the fact that both `s1`

and `s2`

are matching with the form `Star re`

.
But by `induction`

. it will give us *all 7 cases* to prove, but *5 of them are contradictory*!

That’s where we need `remember (Star re) as re'`

to get this bit of information back to `discriminate`

.

### Sidenotes: `inversion`

vs. `induction`

on evidence

We might attemp to use `inversion`

,
which is best suitted for have a specific conclusion of some rule and inverts back to get its premises.

But for *recursive cases* (e.g. `Star`

), we always need `induction`

.

`induction`

on a specific conclusion then `remember + contradiction`

is similar with how `inversion`

solves contradictionary cases. (They both `destruct`

the inductively defined things for sure)

## Exercise: 5 stars, advanced (pumping)

FCT/Wikipedia “proves” pumping lemma for regex in a non-constructive way.

Here we attempts to give a constructive proof.

## Case Study: Improving Reflection (互映)

we often need to relate boolean computations to statements in

`Prop`

1
2
3

Inductive reflect (P : Prop) : bool → Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ¬P) : reflect P false.

The *only* way to construct `ReflectT/F`

is by showing (a proof) of `P/¬P`

,
meaning invertion on `reflect P bool`

can give us back the evidence.

`iff_reflect`

give us `eqbP`

.

1
2
3
4

Lemma eqbP : ∀n m, reflect (n = m) (n =? m).
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

This gives us a small gain in convenience: we immediately give the `Prop`

from `bool`

, no need to `rewrite`

.

Proof Engineering Hacks…

### SSReflect - small-scale reflection

a Coq library used to prove 4-color theorem…! simplify small proof steps with boolean computations. (somewhat automation with decision procedures)

## Extended Exercise: A Verified Regular-Expression Matcher

we have defined a

match relationthat canprovea regex matches a string. but it does not give us aprogramthat canrunto determine a match automatically…

we hope to translate

inductive rules (for constructing evidence)torecursive fn. however, since`reg_exp`

is recursive, Coq won’t accept it always terminates

theoritically, the regex = DFA so it is decidable and halt. technically, it only halts on finite strings but not infinite strings. (and infinite strings are probably beyond the scope of halting problem?)

Heavily-optimized regex matcher = translating into

state machinee.g. NFA/DFA. Here we took aderivativeapproach which operates purely on string.

1
2

Require Export Coq.Strings.Ascii.
Definition string := list ascii.

Coq 标准库中的 ASCII 字符串也是归纳定义的，不过我们这里为了之前定义的 match relation 用 `list ascii`

.

to define regex matcher over

`list X`

i.e. polymorphic lists. we need to be able totest equalityfor each`X`

etc.

### Rules & Derivatives.

Check paper Regular-expression derivatives reexamined - JFP 09 as well.

`app`

and `star`

are the hardest ones.

#### Let’s take `app`

as an example

##### 1. 等价 helper

1
2

Lemma app_exists : ∀(s : string) re0 re1,
s =~ App re0 re1 ↔ ∃s0 s1, s = s0 ++ s1 ∧ s0 =~ re0 ∧ s1 =~ re1.

this *helper rules* is written for the sake of convenience:

- the
`<-`

is the definition of`MApp`

. - the
`->`

is the`inversion s =~ App re0 re1`

.

##### 2. `App`

对于 `a :: s`

的匹配性质

1
2
3
4

Lemma app_ne : ∀(a : ascii) s re0 re1,
a :: s =~ (App re0 re1) ↔
([ ] =~ re0 ∧ a :: s =~ re1) ∨
∃s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re0 ∧ s1 =~ re1.

the second rule is more interesting. It states the *property* of `app`

:

App re0 re1 匹配 a::s 当且仅当 (re0 匹配空字符串 且 a::s 匹配 re1) 或 (s=s0++s1，其中 a::s0 匹配 re0 且 s1 匹配 re1)。

这两条对后来的证明很有帮助，`app_exists`

反演出来的 existential 刚好用在 `app_ne`

中.

https://github.com/jiangsy/SoftwareFoundation/blob/47543ce8b004cd25d0e1769f7444d57f0e26594d/IndProp.v

##### 3. 定义 derivative 关系

the relation * re' is a derivative of re on a* is defind as follows:

1
2

Definition is_der re (a : ascii) re' :=
∀s, a :: s =~ re ↔ s =~ re'.

##### 4. 实现 derive

Now we can impl `derive`

by follwing `2`

, the property.
In paper we have:

1
2
3
4

∂ₐ(r · s) = ∂ₐr · s + ν(r) · ∂ₐs -- subscriprt "a" meaning "respective to a"
where
ν(r) = nullable(r) ? ε : ∅

In our Coq implementation, `nullable(r) == match_eps(r)`

,

Since we know that
`∀r, ∅ · r = ∅`

,
`∀r, ε · r = r`

,
we can be more straightforward by expanding out `v(r)`

:

1
2
3
4
5

Fixpoint derive (a : ascii) (re : @reg_exp ascii) : @reg_exp ascii :=
...
| App r1 r2 => if match_eps r1 (** nullable(r) ? **)
then Union (App (derive a r1) r2) (derive a r2) (** ∂ₐr · s + ∂ₐs **)
else App (derive a r1) r2 (** ∂ₐr · s **)