The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Sorry, did a non-list send by accident.  Resending...

On Wed, 27 May 2020 16:25:29 -0500
Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

> No, it did not.
> 
> Is there a tactic which says "do one step of reduction"?  

I have developed beta1 and zeta1 tactics that do one step of those
reductions, but none that would help here.  

Are you sure hnf doesn't work?  I tried it, and it seemed to work for
me:

Inductive Formula {A : Type} : Type :=
| FAtomic : (A -> bool) -> Formula
| FAnd : Formula -> Formula -> Formula
| FOr : Formula -> Formula -> Formula.

Fixpoint eval {A : Type} (f : @Formula A) (x : A) : bool :=
  match f with
  | FAtomic f => f x
  | FAnd f g => (eval f x) && (eval g x)
  | FOr f g => (eval f x) || (eval g x)
  end.

Section Test.
  Variable A : Type.
  Variable x : A.
  Variable f g h: @Formula A.

  Goal True.
    pose (eval (FAnd (FOr f g) h) x) as e.
    hnf in e.
    
    
The above produces:

1 subgoal (ID 23)
  A : Type
  x : A
  f, g, h : Formula
  e := if eval (FOr f g) x then eval h x else false : bool
  ============================
  True


> 
> On Wed 27 May, 2020, 16:14 jonikelee AT gmail.com, <jonikelee AT gmail.com>
> wrote:
>   
> > Does the hnf tactic work?
> >
> >
> > On Wed, 27 May 2020 10:55:26 -0500
> > Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:
> >    
> > > I have something like:
> > >
> > > Inductive Formula {A : Type} : Type :=
> > > | FAtomic : (A -> bool) -> Formula
> > > | FAnd : Formula -> Formula -> Formula
> > > | FOr : Formula -> Formula -> Formula
> > > .
> > >
> > > and something like
> > >
> > > Fixpoint eval {A : Type} (f : @Formula A) (x : A) : bool :=
> > > match f with
> > > | FAtomic f => f x
> > > | FAnd f g => (eval f x) && (eval g x)
> > > | FOr f g => (eval f x) || (eval g x)
> > > end.
> > >
> > > Now, let's say I have a proof and I have an expression e = (FAnd
> > > (FOr f g) h), and I am trying to simplify (eval e x). If I simply
> > > suggest `simpl.`, Coq simplifies it all the way down. How can I
> > > control simpl so that only the first FAnd is simplified but the
> > > FOr is not?
> > >
> > > Currently, I am using "replace ... with ... " but this requires
> > > me to type out all the details, which is very painful. The actual
> > > formula and eval that I have are more complex than this.
> > >
> > > Another option seems to be `remember (FOr f g) as z.` and then
> > > doing `simpl.`, but this is also not very nice since I have to
> > > copy large chunks of the expression to my proof.    
> >
> >