<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.

```


---

