# Mixing Ltac and Gallina for Fun and Profit

*mixing together*Ltac and Gallina.

- With match goal with it can inspect its context
- With match type of _ with it can pattern matches on types

## Revisions

This revisions table has been automatically generated
from the
`git`

history of this website repository, and the
change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here.

2021-03-28 | 2021 Spring redesign | 495f9db |

2020-08-28 | Heavy reworking of the Ltac series | a7e4531 |

2020-07-31 | Make the two articles about Ltac refer to each other | c2bb9b0 |

2020-07-31 | “For Fun and Benefit” was not an idiomatic expression | c0364ff |

2020-07-26 | Initial publication | a254d35 |

## A Tale of Two Worlds, and Some Bridges §

Definition is_some {α} (x : option α) : bool :=

match x with Some _ => true | None => false end.

Lemma is_some_None {α} (x : option α)

: x = None -> is_some x <> true.

Proof. intros H. rewrite H. discriminate. Qed.

Definition from_option {α}

(x : option α) (some : is_some x = true)

: α :=

match x as y return x = y -> α with

| Some x => fun _ => x

| None => fun equ => False_rect α (is_some_None x equ some)

end eq_refl.

In from_option, we construct two proofs without using tactics:
We can use another approach. We can decide to implement from_option
with a proof script.

- False_rect α (is_some_None x equ some) to exclude the absurd case
- eq_refl in conjunction with a dependent pattern matching (if you are not familiar with this trick: the main idea is to allow Coq to “remember” that x = None in the second branch)

Definition from_option' {α}

(x : option α) (some : is_some x = true)

: α.

Proof.

case_eq x.

+ intros y _.

exact y.

+ intros equ.

rewrite equ in some.

now apply is_some_None in some.

Defined.

There is a third approach we can consider: mixing Gallina terms, and
tactics. This is possible thanks to the ltac:() feature.

Definition from_option'' {α}

(x : option α) (some : is_some x = true)

: α :=

match x as y return x = y -> α with

| Some x => fun _ => x

| None => fun equ => ltac:(rewrite equ in some;

now apply is_some_None in some)

end eq_refl.

When Coq encounters ltac:(), it treats it as a hole. It sets up a
corresponding goal, and tries to solve it with the supplied tactic.
Conversly, there exists ways to construct terms in Gallina when writing a
proof script. Certains tactics takes such terms as arguments. Besides, Ltac
provides constr:() and uconstr:() which work similarly to ltac:().
The difference between constr:() and uconstr:() is that Coq will try to
assign a type to the argument of constr:(), but will leave the argument of
uconstr:() untyped.
For instance, consider the following tactic definition.

Both x the argument of wrap_id and f the anonymous identity function
are not typed. It is only when they are composed together as an argument of
exact (which expects a typed argument, more precisely of the type of the
goal) that Coq actually tries to typecheck it.
As a consequence, wrap_id generates a specialized identity function for
each specific context.

The generated anonymous identity function is fun x : nat => x.

The generated anonymous identity function is fun x : list α => x. Besides,
we do not need to give more type information about nil. If wrap_id were
to be expecting a typed term, we would have to replace nil by (@nil
α).
Proofs and computational programs are encoded in Coq as terms, but there is
a fundamental difference between them, and it is highlighted by one of the
axiom provided by the Coq standard library: proof irrelevance.
Proof irrelevance states that two proofs of the same theorem (i.e., two
proof terms which share the same type) are essentially equivalent, and can
be substituted without threatening the trustworthiness of the system. From a
formal methods point of view, it makes sense. Even if we value “beautiful
proofs,” we mostly want correct proofs.
The same reasoning does
Using tactics such as auto to generate terms which do not live inside
Prop is risky, to say the least. For instance,

## Beware the Automation Elephant in the Room §

*not*apply to computational programs. Two functions of type nat -> nat -> nat are unlikely to be equivalent. For instance, add, mul or sub share the same type, but computes totally different results.
This works, but it is certainly not what you would expect:
That being said, if we keep that in mind, and assert the correctness of the
generated programs (either by providing a proof, or by extensively testing
it), there is no particular reason not to use Ltac to generate terms when it
makes sens.
Dependently-typed programming can help here. If we decorate the return type
of a function with the expected properties of the result wrt. the function’s
arguments, we can ensure the function is correct, and conversly prevent
tactics such as auto to generate “incorrect” terms. Interested readers may
refer to the dedicated
series on this very website.

add = fun _ y : nat => y : nat -> nat -> nat