Beginner Coq question about equiv · Coq users

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.

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 *)

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!

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.

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.

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

Guillaume Melquiond (Sep 28 2023 at 16:54):

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.

Stream: Coq users

Topic: Beginner Coq question about equiv

David Sillman (Sep 28 2023 at 00:50):

Guillaume Melquiond (Sep 28 2023 at 04:02):

David Sillman (Sep 28 2023 at 15:10):

Yann Leray (Sep 28 2023 at 15:24):

Guillaume Melquiond (Sep 28 2023 at 16:54):