6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Have you asked about this on the coq mailing list? It is full of experts. $\endgroup$ – Andrej Bauer Jul 18 '13 at 23:39
  • 1
    $\begingroup$ Nope, but thank you for your suggestion, I shall. $\endgroup$ – Squera Jul 19 '13 at 7:35
  • $\begingroup$ Can you post a condensed answer here, if you receive one? $\endgroup$ – Dave Clarke Jul 20 '13 at 15:11
4
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.