The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Is there a way to specify to simpl to stop simplifying after exactly one step?

Basically, I have something like f(f(x)) which simplifies to some _expression_ in f(x). I only wish to simply this once and NOT get rid of the inner f(x)

---

More details:

I have

Fixpoint eval2 {A: Type} (mon: Monitor A) (l : list A) : (bool * Monitor A) :=
  match l with
  | nil => (false, mon)
  | (x :: xs) => let (_, mon') := eval2 mon xs in
               (mNext mon' x)
  end.

In a certain proof, I have

E3 : eval2 (MonAnd mon1 mon2) (a0 :: l) = (bl, ml)

and

H3 : eval2 (MonAnd mon1 mon2) (a :: a0 :: l) = (true, x)

I wish to use E3 effectively after simplifying H3 by one step. However, when I try to use simpl in H3, I get

H3 : (let (_, mon') :=
          let (_, mon') := eval2 (MonAnd mon1 mon2) l in mNext mon' a0 in
        mNext mon' a) = (true, x)