Exercise Zulip-01 in Coq

ExZulip01.v

(** Exercise Zulip-01

"Prove, by induction on boolean terms, that one step of
evaluation in this lambda calculus reduces the term size."

<https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Tactic.20for.20destructing.20specific.20pattern.20match.20in.20Goal/near/394101120>

*)

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

Notation T := TmTrue.
Notation F := TmFalse.
Notation "~ A" := (TmNot A).
Notation "F ? G : H" := (TmIf (F) (G) (H)) (at level 100, G at level 99).

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.

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.

Require Import Coq.Arith.PeanoNat.

Lemma term_size_eval_not_le : forall (t : term),
  term_size (eval1 (~ t)) <=
  term_size (~ (eval1 t)).
Proof.
  intros.
  destruct t; simpl.
  - apply le_S. apply le_n.
  - apply le_S. apply le_n.
  - apply le_n.
  - apply le_n.
Qed.

Lemma term_size_eval_if_not_le : forall (t1 t2 t3 : term),
  term_size (eval1 (~ t1 ? t2 : t3)) <=
  term_size (~ (eval1 t1 ? t2 : t3)).
Proof.
  intros.
  destruct t1; simpl.
  - apply le_S. apply le_n.
  - apply le_S. apply le_n.
  - apply le_n.
  - apply le_n.
Qed.

Theorem eval1_dec_size : forall (t : term),
  term_size (eval1 t) <= term_size t.
Proof.
  intros.
  induction t.
  - simpl. apply le_n.
  - simpl. apply le_n.
  - apply Nat.le_trans with (term_size (~ eval1 t)).
    + apply term_size_eval_not_le.
    + simpl.
      rewrite <- Nat.succ_le_mono.
      apply IHt.
  - destruct t1.
    + simpl.
      repeat apply le_S.
      apply Nat.le_add_r.
    + simpl.
      repeat apply le_S.
      apply Nat.le_add_l.
    + simpl.
      rewrite <- Nat.succ_le_mono.
      repeat rewrite <- Nat.add_succ_l.
      repeat apply Nat.add_le_mono_r.
      simpl in IHt1. apply IHt1.
    + simpl.
      rewrite <- Nat.succ_le_mono.
      repeat rewrite <- Nat.add_succ_l.
      repeat apply Nat.add_le_mono_r.
      simpl in IHt1. apply IHt1.
Qed.