The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Wouldn't you want to [remember (a', m')] as well before inducting?  In 
general, [induction] only works when all arguments to the inductive type 
family are variables, and just one [remember] doesn't get you there.

I actually recommend ignoring [remember] and just restating your lemma 
in auxiliary form, where all the arguments to the inductive fact in 
question are variables, with equality hypotheses following to enforce 
shape.  Don't forget to put quantifiers over those sub-parts _after_ the 
hypothesis you induct on and not [intro] them first, so that they may 
change in the course of the induction.

Here's my solution:

Hint Constructors eval_trans.
Hint Extern 1 (_ --> _) => apply eval_step.

Lemma gt_S : forall n, S n > n.
  auto.
Qed.

Hint Resolve gt_S.

Lemma some_theorem' :
  forall S1 S2, S1 ==> S2
    -> forall (a a' : Address) (m m' : Memory),
      S1 = (a, m)
      -> S2 = (a', m')
      -> (a, m) ==> (S a', m').
  induction 1; intuition subst;
    try match goal with
          | [ H : (_, _) = (_, _) |- _ ] => injection H; clear H; 
intros; subst
        end;
    repeat match goal with
             | [ s : State |- _ ] => destruct s
           end; eauto.
Qed.

Theorem some_theorem :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') ->
    (a, m) ==> (S a', m').
  eauto using some_theorem'.
Qed.


On 07/19/2013 05:31 AM, 
marco.patrignani AT cs.kuleuven.be
 wrote:
> Lemma some_lemma :
>    forall (a a' : Address) (m m' : Memory),
>      (a, m) ==>  (a', m') ->
>      (a, m) ==>  (S a', m').
> Proof.
> intros a a' m m' H.
> induction H.
> (*base case*) admit.
> (*inductive case*) admit.
> (*in both cases I lost that t = (a,m), but the IH is right*)
> Admitted.
>
>
> Lemma some_lemma_v2 :
>    forall (a a' : Address) (m m' : Memory),
>      (a, m) ==>  (a', m') ->
>      (a, m) ==>  (S a', m').
> Proof.
> intros a a' m m' H.
> remember (a,m) as t.
> induction H.
> (*base case*) admit.
> (*inductive case*)
> (* I have that t = (a,m) and the IH sais that if ti =(a,m) then have some ==>,
> but ti is the state t reaches after 1 step (H)*)
> Admitted.
>