The Coq mailing list

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

Only the method with remember worked.

Sadly, the one with the simpl and the pattern did not make any difference. Neither did the one with the iota.

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)