<p>It is not clear to me how induction helps with the lemma you are trying to prove, so I'll take an alternative approach.</p>

<p>Firstly, I prove two helper lemmas that break apart and put back together <code>==&gt;</code>  with <code>--&gt;</code> at the tail, rather than at the start. Based on these lemmas, I can manipulate the result using your definition of <code>eval</code> to get the desired result. My impression is that the core lemma relies too heavily on the somewhat odd definition of <code>eval</code>, which possibly allowed me to side-step any inductive argument you had in mind.</p>

<p>So, although the lemma you are interested in does not require induction over the transitive relation, the two helper lemmas do.</p>

<p>Note: <em>proofs have not been optimised or beautified.</em></p>

<p>The first lemma inverts instances of <code>t ==&gt; ti</code> so that the single step reduction occurs at the end, rather than at the beginning. The proof relies on induction and was undemanding.</p>

<pre><code>Lemma end_inversion :
  forall (t ti : State),
    t ==&gt; ti -&gt; 
    t = ti \/ 
      exists t', t ==&gt; t' /\ t' --&gt; ti.
Proof.
  intros.
  induction H.

  left; auto.

  destruct IHeval_trans; right.

  exists t.
  subst.
  split; [apply refl | auto].

  destruct H1 as [x [H1 H2]].
  exists x.
  split; auto.
  apply trans with (ti := ti); auto.
Qed.
</code></pre>

<p>The second lemma plugs a single step reduction onto the end of a transitive reduction to again get a transitive reduction. The proof is by straightforward induction. </p>

<pre><code>Lemma end_eval : 
  forall (t ti t' : State), 
    t ==&gt; t' -&gt; 
    t' --&gt; ti -&gt; 
    t ==&gt; ti.
Proof.
  intros.
  induction H.
  apply trans with (ti := ti); [auto | apply refl].
  apply trans with (ti := ti0); auto.
Qed.
</code></pre>

<p>And now your lemma. The proof relies on <code>end_inversion</code> to break up <code>==&gt;</code>, does some manipulation of the result, and puts things back together using <code>end_eval</code>. No induction is required.</p>

<pre><code>Lemma some_lemma :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==&gt; (a', m') -&gt;
    (a, m) ==&gt; (S a', m').
Proof.
  intros a a' m m' H.
  apply end_inversion in H.
  destruct H.
  inversion H; subst.
  apply end_eval with (t' := (a', m')).
    apply refl.
    apply eval_step; auto.
  destruct H as [x [H0 H1]].
  apply end_eval with (t := (a, m)) (t' := x); auto.
  inversion H1; subst.
  apply eval_step; auto.
Qed.
</code></pre>

CC BY-SA 3.0
2013-07-21T10:51:36.083Z
2013-07-21T16:06:08.217Z
2013-07-21T16:06:08.217Z
Dave Clarke
<p>I have the current problem when using induction with Coq:</p>

<p>I have states ST, which are pairs (A,B), where A are Addresses (nat) and B are Memories (A parameter)</p>

<pre><code>Open Scope type_scope.

Definition Address := nat.
Parameter Memory : Set.

Definition State := ( Address *  Memory ).
</code></pre>

<p>and a reflexive and transitive relation between states:
    ST ==> ST',
which builds on a relation that performs the 'single step' between states:
    ST --> ST'</p>

<pre><code>Reserved Notation "S '--&gt;' S'" (at level 50, left associativity).
Inductive eval : State -&gt; State -&gt; Prop :=
| eval_step : forall (a a' : nat) (m m' : Memory),
  a' &gt; a -&gt;
  (a, m) --&gt; (a', m')

where "S '--&gt;' S'" := (eval S S') : type_scope.

Reserved Notation "S '==&gt;' S'" (at level 50, left associativity).
Inductive eval_trans : State -&gt; State -&gt; Prop :=
| refl : forall (t : State),
  t ==&gt; t

| trans : forall (t t' ti : State),
  t --&gt; ti -&gt;
  ti ==&gt; t'-&gt;
  t ==&gt; t'

where "S '==&gt;' S'" := (eval_trans S S') : type_scope.
</code></pre>

<p>When performing induction on an hypothesis of the form 
    ST ==> ST',
I should get two cases to prove.</p>

<p>When I introduce the various parts of a state among the hypotheses and then induce over a ST==>ST' hypothesis,
CoQ forgets the biding between a state and its component.
E.g. if ST is A,B and I have A,B among the hypotheses, induction here will forget the binding between ST and A,B.
This is a known problem (<a href="https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction">https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction</a>), that can be circumvented with a "remember A,B as ST". </p>

<p>However, in the transitive case, the "remember" does some wrong things, as the single step becomes
    ST --> ST'
    ST' ==> ST''
(and an inductive hypothesis of the form, if ST' = A,B , having already ST = A,B, then ST ==> ST')
The single step is performed between the same state, which should not be the case.</p>

<p>If I drop the "remember", the transitive case works fine, as expected,
    ST --> ST'
    ST' ==> ST''
but, alas, the state ST is a generic state and not A,B.</p>

<pre><code>Lemma some_lemma :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==&gt; (a', m') -&gt;
    (a, m) ==&gt; (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) ==&gt; (a', m') -&gt;
    (a, m) ==&gt; (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 ==&gt;,
but ti is the state t reaches after 1 step (H)*)
Admitted.
</code></pre>

<p>Any help is greatly appreciated.
I have created this example by shortening the case I am working on, I believe all the important details to be present.</p>

<p>thank you, and sorry in case I have missed some answer being out there in the net, but I couldn't find anything useful.</p>

CC BY-SA 3.0
2013-07-18T23:39:16.173Z
Have you asked about this on the coq mailing list? It is full of experts.
Andrej Bauer
CC BY-SA 3.0
2013-07-19T07:35:00.797Z
Nope, but thank you for your suggestion, I shall.
Squera
CC BY-SA 3.0
2013-07-20T15:11:20.910Z
Can you post a condensed answer here, if you receive one?
Dave Clarke
<coq>
Induction over a transitive relation in Coq
Squera
# Induction over a transitive relation in Coq

(Asked by: username_0 on 2013-07-18)

I have the current problem when using induction with Coq:
I have states ST, which are pairs (A,B), where A are Addresses (nat) and B are Memories (A parameter)
Open Scope type_scope.

Definition Address := nat.
Parameter Memory : Set.

Definition State := ( Address *  Memory ).

and a reflexive and transitive relation between states:
    ST ==> ST',
which builds on a relation that performs the 'single step' between states:
    ST --> ST'
Reserved Notation "S '-->' S'" (at level 50, left associativity).
Inductive eval : State -> State -> Prop :=
| eval_step : forall (a a' : nat) (m m' : Memory),
  a' > a ->
  (a, m) --> (a', m')

where "S '-->' S'" := (eval S S') : type_scope.

Reserved Notation "S '==>' S'" (at level 50, left associativity).
Inductive eval_trans : State -> State -> Prop :=
| refl : forall (t : State),
  t ==> t

| trans : forall (t t' ti : State),
  t --> ti ->
  ti ==> t'->
  t ==> t'

where "S '==>' S'" := (eval_trans S S') : type_scope.

When performing induction on an hypothesis of the form 
    ST ==> ST',
I should get two cases to prove.
When I introduce the various parts of a state among the hypotheses and then induce over a ST==>ST' hypothesis,
CoQ forgets the biding between a state and its component.
E.g. if ST is A,B and I have A,B among the hypotheses, induction here will forget the binding between ST and A,B.
This is a known problem (https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction), that can be circumvented with a "remember A,B as ST". 
However, in the transitive case, the "remember" does some wrong things, as the single step becomes
    ST --> ST'
    ST' ==> ST''
(and an inductive hypothesis of the form, if ST' = A,B , having already ST = A,B, then ST ==> ST')
The single step is performed between the same state, which should not be the case.
If I drop the "remember", the transitive case works fine, as expected,
    ST --> ST'
    ST' ==> ST''
but, alas, the state ST is a generic state and not A,B.
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.

Any help is greatly appreciated.
I have created this example by shortening the case I am working on, I believe all the important details to be present.
thank you, and sorry in case I have missed some answer being out there in the net, but I couldn't find anything useful.

**Tags:** coq

> **Comments:**
> **username_1**: Have you asked about this on the coq mailing list? It is full of experts.  
> **username_0**: Nope, but thank you for your suggestion, I shall.  
> **username_2**: Can you post a condensed answer here, if you receive one?  

---

## 1 answers

### Answer by username_2 on 2013-07-21. Score: 4

It is not clear to me how induction helps with the lemma you are trying to prove, so I'll take an alternative approach.
Firstly, I prove two helper lemmas that break apart and put back together ==>  with --> at the tail, rather than at the start. Based on these lemmas, I can manipulate the result using your definition of eval to get the desired result. My impression is that the core lemma relies too heavily on the somewhat odd definition of eval, which possibly allowed me to side-step any inductive argument you had in mind.
So, although the lemma you are interested in does not require induction over the transitive relation, the two helper lemmas do.
Note: proofs have not been optimised or beautified.
The first lemma inverts instances of t ==> ti so that the single step reduction occurs at the end, rather than at the beginning. The proof relies on induction and was undemanding.
Lemma end_inversion :
  forall (t ti : State),
    t ==> ti -> 
    t = ti \/ 
      exists t', t ==> t' /\ t' --> ti.
Proof.
  intros.
  induction H.

  left; auto.

  destruct IHeval_trans; right.

  exists t.
  subst.
  split; [apply refl | auto].

  destruct H1 as [x [H1 H2]].
  exists x.
  split; auto.
  apply trans with (ti := ti); auto.
Qed.

The second lemma plugs a single step reduction onto the end of a transitive reduction to again get a transitive reduction. The proof is by straightforward induction. 
Lemma end_eval : 
  forall (t ti t' : State), 
    t ==> t' -> 
    t' --> ti -> 
    t ==> ti.
Proof.
  intros.
  induction H.
  apply trans with (ti := ti); [auto | apply refl].
  apply trans with (ti := ti0); auto.
Qed.

And now your lemma. The proof relies on end_inversion to break up ==>, does some manipulation of the result, and puts things back together using end_eval. No induction is required.
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.
  apply end_inversion in H.
  destruct H.
  inversion H; subst.
  apply end_eval with (t' := (a', m')).
    apply refl.
    apply eval_step; auto.
  destruct H as [x [H0 H1]].
  apply end_eval with (t := (a, m)) (t' := x); auto.
  inversion H1; subst.
  apply eval_step; auto.
Qed.


---

