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.