The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Quoting Benjamin Pierce 
<bcpierce AT cis.upenn.edu>:

> Suppose we start a development like this...
>
> > Definition good (f : nat->(nat*nat)) :=
> >  forall a,
> >    let (x,y) := f a in
> >    x < y /\ a < x.
> >
> > Definition compose (f g : nat->(nat*nat)) :=
> >  fun a =>
> >    let (x,y) := f a in
> >    let (u,v) := g y in
> >    (x,v).
> >
> > Lemma compose_is_good :
> >  forall f g,
> >  good f -> good g -> good (compose f g).
> > Proof.
> >  (* ??? *)

(* Here are two ways of completing the proof.  The first proof is
   essentially what I came up with originally, but the second is
   shorter.  In both proofs, I used [omega] to reason about
   arithmetic. *)

Require Import Omega.

Lemma compose_is_good :
  forall f g,
  good f -> good g -> good (compose f g).
Proof.
  unfold good, compose.
  intros f g J1 J2 a.

  (* The main observation is that the "destructuring [let]s" here are
     each syntactic sugar for a [match], so we can simplify each one
     the same way we would simplify a [match]: by performing a case
     analysis on the term being analyzed.

     The [case_eq] tactic is similar to [destruct] and [case], except
     it records an equality that "remembers" the term being analyzed.
  *)

  case_eq (f a). intros n n' J3.
  case_eq (g n'). intros m m' J4.

  (* Now we make use of [J1] and [J2].  The equalities that [case_eq]
     gave us will be useful in simplifying those hypotheses. *)

  specialize (J1 a). rewrite J3 in J1.
  specialize (J2 n'). rewrite J4 in J2.
  omega.
Qed.

Lemma compose_is_good_shorter :
  forall f g,
  good f -> good g -> good (compose f g).
Proof.
  unfold good, compose.
  intros f g J1 J2 a.

  (* If we reorganize the proof, we can simply [destruct] all
     occurrences of [f _] and [g _] at once, instead of using
     [case_eq] and [rewrite]. *)

  specialize (J1 a). destruct (f a) as [x y].
  specialize (J2 y). destruct (g y) as [x' y'].
  omega.
Qed.

(*

Hope that helps,
Brian

*)