The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

In this case, proving a true transitivity lemma would be useful. 

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 eval_trans' : forall x y z, x ==> y -> y ==> z -> x ==> z.
  induction 1; auto; intros; eauto.
Qed.

Theorem some_thoemre' :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') -> (a, m) ==> (S a', m').
  intros; eapply eval_trans'; eauto 3.
Qed.




-- Duckki



On Friday, July 19, 2013 at 7:52 AM, Adam Chlipala wrote:

> Actually, here's an even simpler solution, based on the structure of 
> your theorem.
> 
> 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
> -> S1 ==> (S (fst S2), snd S2).
> induction 1; intuition subst;
> eauto; match goal with
> | [ t : State |- _ ] => destruct t; eauto
> end.
> Qed.
> 
> Theorem some_theorem :
> forall (a a' : Address) (m m' : Memory),
> (a, m) ==> (a', m') ->
> (a, m) ==> (S a', m').
> intros ? ? ? ? H; apply some_theorem' in H; auto.
> Qed.