# GADTs vs Inductive Datatypes

Consider the following definition of Nat-indexed Vector GADT in OCaml and Haskell: OCaml:

Haskell:

Observe that quantified type variables in the type of constructors are generalized by the type-constructor signature. Infact, this is not always true. For example, consider the GADT for higher-order abstract syntax:

The type scheme of *App* contains a type variable (*a*) that is not
generalized by the type-constructor signature.

This type is treated as existential type when an expression of type
`Exp b`

is destructed and matched agains `App`

.

Therefore, the correct observation is this: All type variables generalized by the signature of type constructor are also generalized in type schemes of its value constructors.

Here is the nat-indexed vector inductive datatype in Coq:

The above definition should be read as following: `vec`

is a `Type`

indexed by a `Type`

and a `nat`

. Here are the only ways to construct
values of `Vec X N`

, where X could be any `Type`

and N could be any
`nat`

:

- For any
`Type`

*A*,`vnil A`

is a value of`Vec A O`

- For any
`Type`

*A*and for any`nat`

*n*,`vcons A n`

accepts a value of type*A*, a value of type`vec A n`

, and generates a value of type`Vec A (S n)`

Notice that it looks quite similar to Haskell definition, with type
variables explicated. An empty list in explicitly typed haskell is
`VNil Int`

, whereas in Coq, it is `vnil int`

. However, unlike Haskell,
where there is term-type-kind hierarcy, Coq has full dependent types
with infinite hierarchy of universes. One consequence of this is that we
will frequently see arrows mapping members of one universe to members
of a different universe. For example, if we `Print vec.`

, this is what
we see:

Evidently, `vec`

maps a member of Type(59) universe and member of Set
universe to a type universe at higher level. Compare this to the type
of `Vec`

type-constructor in haskell `* -> * -> *`

, which simply says
that when *a* is a type, and *n* is a type (i.e., *a* and *n* have
kind `*`

), then `Vec a n`

is a type (i.e., it has kind `*`

).

In the inductive definition of `vec`

, observe that both constructors
construct values of type `vec A _`

. Therefore, we can as well
generalize *A* at the type of type-constructor (here, this is a mere
syntactic convenience):

The above definition should be read as following: `vec`

is a `Type`

indexed by a `Type`

*A* and a `nat`

. Here are the only ways to construct
values of `Vec A N`

, where N could be any `nat`

…

Another consequence of having full dependent types in Coq is that the
type of inductive type-constructors can be dependent as well. For eg,
here is the inductive definition of `sig`

datatype:

`sig T P`

is the type of values of type *T* that satisfy proposition
*P*. `sig`

is a function on type, and propositions on *that* type.
Observe that the type of second argument to type-constructor `sig`

depends on the value of its first argument.

How did we arrive at that type definition? Let us say we want to
define a refinement type for values of `nat`

satisfying a predicate
*P*. Effectively, we would like to index `nat`

with a predicate *P*
over natural numbers. Since *P* is a predicate, `P : nat -> Prop`

. We
define a new `Type`

*natST* (read “nat, such that”) that is indexed by
`P : nat -> Prop`

:

What should be its constructors? There has to be only one constructor
that, given a nat (*n*), and a proof that it satisfies the predicate
(i.e., proof of `P n`

), returns evidence for `natST P`

. In other
words, we have an evidence for `natST P`

if and only if we have a nat,
and the evidence that it satisfies the predicate. Destructing a ```
natST
P
```

value would produce a nat and a proof that it satisfies *P*.

Type `natST`

helps us easily write type for division operation:

# Implicit Arguments

Following is to set the implicit arguments option in Coq.

When the mode for automatic declaration of implicit arguments is on,
the default is to automatically set implicit only the strict implicit
arguments (eg: tyarg of `Cons`

is strict implicit, whereas that of
`Nil`

is contextual implicit).

By default, Coq does not automatically set implicit the contextual implicit arguments. To tell Coq to infer also contextual implicit argument, use command

Setting contextual implcit too may not infer ty annot for Nil. Why? How does coq know whether we want to partially applied Nil or fully apply it? Setting Maximal Implicit works, but that would prevent us from writing certain partial function applications. Therefore, we explciity set implicit args for Nil:

# Notation, Associativity, and Precedence

The level is for precedence. Assume for instance that we want conjunction to bind more than disjunction. This is expressed by assigning a precedence level to each notation, knowing that a lower level binds more than a higher level. Hence the level for disjunction must be higher than the level for conjunction. 100 is the highest level. There is a special 200 level higher than 100.

Since connectives are the less tight articulation points of a text, it is reasonable to choose levels not so far from the higher level which is 100, for example 85 for disjunction and 80 for conjunction

# The Omega Tactic

Omega is a decision procedure for linear arithmetic (also known as Presburger arithmetic). It can be used to discharge any silly goals on nats and integers like:

Omega can deal with nats. It converts nats to integers. Following operations on nat are recognized by omega:

- Predicates, such as =, le, lt, gt, ge
- Functions, such as +, minus, mult, pred, S, O

Omega needs to be imported:

# apply and eapply tactics

`apply H`

tries to unify the current goal with conclusion of H. If it
succeeds, it generates a sub-goal for each assumption (argument) of H.
For instance, in the following context:

using `apply Union_introl`

, where

unifies U with A, B with s1, C with (Union A s2 s3), and x with x to generate following sub-goal:

which is already an assumption.

The tactic `eapply`

does the same, except that instead of failing due
to inability to instantiate variables, it replaces them with
existentials. When you have existential in you context, destruct it to
skolemize. The ?6201 style variables in goal when you use eapply are
actually existential variables.

# The Auto Tactic

The auto tactic solves goals that are solvable by any combination of

- intros, and
- apply.

By default, auto only does `apply`

on local hypotheses. To add to the
global hint database of auto:

One can optionally declare a hint database using the command ```
Create
HintDb
```

.

To see hints applicable in the current context, and list of all hints, respectively:

Using auto tactic with database of hints named sets:

You can extened hint DB for one application of auto with `using`

keyword. To extend with `Union_introl`

:

To extend with all constructors of `Union`

:

More avatars of auto:

`trivial`

tactic - non recursive auto. depth =0.`autounfold`

and`autorewrite`

to use`Hint Unfold`

and`Hint Rewrite`

hints in the hint database.

## Auto Examples

Completely manual proof for theorem union_is_associative:

Proof with auto:

Even simpler auto proof:

SF automation chapter (sfauto)says this on `auto`

:

Note that proof search tactics never perform any rewriting step (tactics rewrite, subst), nor any case analysis on an arbitrary data structure or predicate (tactics destruct and inversion), nor any proof by induction (tactic induction). So, proof search is really intended to automate the final steps from the various branches of a proof. It is not able to discover the overall structure of a proof.

# The Solve Tactical

Solve tactical takes a list of tactics, and tries them left to right, stopping when a tactic is successful. If none of the tactics are successful, the solve fails.

The difference between `try solve [e1 | e2]' and `

try e1; try e2` is
the short-cut behaviour of solve.

# The Intuition Tactical

`Intuition t`

applies propositional decision procedure to simplify the
goal, and then applies tactic `t`

on the resultant.

`intuition fail`

succeeds if the goal is a propositional tautology. Fails otherwise. This is equivalent to`tauto`

tactic.- Simply using
`intuition`

is equivalent to using`intuition auto with \*`

.

# Notes:

- To instantiate a universally quantified hypothesis H on variable n,
just do (H n). Eg:
`destruct (H n).`

- When there is ambiguity about which term
`rewrite`

rewrites when there are multiple rewritable terms in the goal, assert the required hypothesis as a separate assertion, and prove it (using apply). - It is futile to define strong lemmas with conjunction in consequent.
Not only that applying them is difficult, but also that
`auto`

only tries such lemmas when current goal is a conjunction at top level. Instead, define two separate lemmas.

# References:

- Universes chapter in CPDT.