I'm working on implementing a simple Boolean Algebra Lambda Calculus in Coq, inspired by the early chapters of Types and Programming Languages by @Benjamin Pierce . This lambda calculus has terms composed of T/F values, the unary not operator and if-statement. I've implemented the terms of this calculus as a Type:

```
Inductive term : Type :=
| TmTrue : term
| TmFalse : term
| TmNot : term -> term
| TmIf : term -> term -> term -> term.
```

I've also defined the nat "term size" recursively on this type:

```
Fixpoint term_size (t: term) : nat :=
match t with
| T => 1
| F => 1
| ~ t' => 1 + (term_size t')
| t' ? t'' : t''' => 1 + (term_size t') + (term_size t'') + (term_size t''')
end.
```

And a very simple evaluator for handling a single step of evaluation on the term type:

```
Fixpoint eval1 (t: term) : term :=
match t with
| ~ T => F
| ~ F => T
| ~ t' => ~ eval1 t'
| T ? t' : t'' => t'
| F ? t' : t'' => t''
| t' ? t'' : t''' => (eval1 t') ? t'' : t'''
| _ => t
end.
```

I'm now trying to prove what I thought would be a simple result - that evaluating a term once will not increase its term size, which I've tried formulating two different ways:

```
Theorem eval1_dec_size : forall (t: term),
term_size (eval1 t) <=? term_size t = true. (* using Nat.leb *)
Theorem eval1_dec_size : forall (t: term),
term_size (eval1 t) <= term_size t. (* using Nat.le *)
```

But I'm getting stuck. My primary approach has been induction on t:

```
Theorem eval1_dec_size : forall (t: term),
term_size (eval1 t) <= term_size t.
Proof.
intros.
induction t.
- simpl. reflexivity.
- simpl. reflexivity.
- (* ... *)
```

As soon as I hit one of the recursive cases from the type, I get stuck with the fact that I need/want to prove that `eval( ~ t) = ~ (eval t)`

, or more generally that `eval t = t' -> t = t'`

.

In other words, to prove the result, it seems that I need to stretch Coq's definition of equivalence ("equiv") to allow me to assert that terms are equiv if one is the result of evaluating the other. Does this approach to the theorem make sense? If not, is there a different way I can try to formulate the theorem which makes it easier to prove? Thanks in advance!

I don't understand your issue issue. In the case of `TmNot`

for example, after `simpl`

, your goal should be something like `IH: size (eval1 t') <= size t' |- size (~ eval1 t') <= size (~ t')`

. This is trivial by definition of `size`

, and does not require any kind of equivalence on `eval1`

. Other recursive calls should be just as trivial.

@Guillaume Melquiond I agree that, after `simpl`

, that my goal should look something like `term_size (~ (eval1 t)) <= term_size (~ t)`

, but that's built on the assumption that we know `eval1 (~ t)`

is identical to `~ (eval1 t)`

by the pattern matching in its definition. But instead, it seems to require me to do another layer of pattern matching (induction?), as this is my actual goal after `simpl`

:

```
term_size match t with
| T => F
| F => T
| _ => ~ eval1 t
end <= S (term_size t)
```

Is `simpl`

not the correct tactic? Do I need to introduce a Lemma so I can use `rewrite`

to make a targeted simplification? Thanks.

Your goal here is `term_size (eval1 (~ t)) <= term_size (~ t)`

, but with the fixpoint definitions of `eval1`

and `term_size`

unfolded once for the constructor `TmNot`

You can prove by using the induction hypothesis that `term_size (~ (eval1 t)) <= term_size (~ t)`

, so you need to relate the sizes of `eval1 (~ t)`

and `~ (eval1 t)`

. I think it would be better to put it as an auxiliary lemma

David Sillman said:

it seems to require me to do another layer of pattern matching (induction?)

Indeed, because of the syntactic sugar, I had not noticed that there was a nested pattern-matching in your definition of `eval1`

, sorry. You can just do `destruct t`

at this point to progress; no need for a full induction. That will unfortunately create a bunch of meaningless cases. So, if you do not want to pollute your proof, you can move them to an auxiliary lemma (or an `assert`

), as suggested by Yann.

Last updated: Jun 22 2024 at 15:01 UTC