The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The standard pattern I use for this is to define the fixpoint and the body separately:

Definition eval2_step {A: Type}

  (eval2 :  Monitor A -> list A -> bool * Monitor A)

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

Fixpoint eval2 {A: Type} (mon: Monitor A) (l : list A) : (bool * Monitor A) :=

  eval2_step eval2 mon l.

Then you can run `simpl eval2` and `simpl eval2_step` (or `cbn [eval2]` and `cbn [eval2_step]`) separately.

On Tue, Feb 25, 2020 at 3:48 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

I didn't test everything but i think there are a few ways to proceed. I do think that it's a good idea for Coq to implement a tactic, say, `eval_step`, which takes a list of reduction steps and perform them in sequence. in this case, I think it would be `eval_step [delta, iota]`. notice that delta reduction is only specified once, so it only unfold the outer `eval2` and iota evals the pattern matching and leave the inner `eval2` as is.

that said, you can probably simulate this action:

unfold eval2 in H3; cbn [iota] in H3.

in particular, `delta` is excluded from `cbn` so I hope `eval2` is not unfolded.

another way is to remember `a0 :: l` by doing

remember (a0 :: l) as l0 eqn:?.

I expect this replaces all `a0 :: l` with `l0`, which allows you to do `simpl in H3`.

another potential way is to specify the list to have two cons:

simpl (eval2 _ (_ :: _ :: _)) in H3.

i would be interested in knowing which one works. please let me know.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Sent: February 25, 2020 4:18 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] Simplifying a function (exactly) once?

 

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)