The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

I am unsure as to whether this is what you want, but if you revert a, m and Heqt before performing the induction, you will strengthen your induction hypothesis.

The context at the inductive step becomes:

 

  H : t --> ti
  H0 : ti ==> t'
  IHeval_trans : forall (a : Address) (m : Memory),
                 ti = (a, m) -> ti ==> (S a', m')
  a : Address
  m : Memory
  Heqt : t = (a, m)
  ============================
   t ==> (S a', m')

 

Is this satisfactory? Supposedly, the premise in the induction hypothesis is somewhat bogus and easily satisfied...

 

- Valentin

On Fri, Jul 19, 2013 at 10:31 AM, <marco.patrignani AT cs.kuleuven.be> wrote:

Hello.

I just posted this question on cs.theory.stackexchange (here:
http://cstheory.stackexchange.com/questions/18407/induction-over-a-transitive-relation-in-coq)
and was suggested to ask for help here as well since there are many experts.
So here's the question.


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
(http://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.