Stream: Coq users

Topic: Beginner Coq question about equiv


view this post on Zulip David Sillman (Sep 28 2023 at 00:50):

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!

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 04:02):

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.

view this post on Zulip David Sillman (Sep 28 2023 at 15:10):

@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.

view this post on Zulip Yann Leray (Sep 28 2023 at 15:24):

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

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 16:54):

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