The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

Expanding on Maximilian's second idea, if you define eval using the 
Equations package (http://mattam82.github.io/Coq-Equations/), the wanted 
equation is auto-generated for you:


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

Require Import Equations.Equations.

Equations eval {A : Type} (f : @Formula A) (x : A) : bool :=
  eval (FAtomic f) x := f x ;
  eval (FAnd f g) x := (eval f x) && (eval g x) ;
  eval (FOr f g) x := (eval f x) || (eval g x)
.

Goal forall f g h, eval (FAnd (FOr f g) h) true = false.
Proof.
  intros. rewrite eval_equation_2.
Abort.


Alternatively using the FunInd package 
(https://coq.inria.fr/refman/language/gallina-extensions.html#coq:cmd.function):

Require Import FunInd.

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

Goal forall f g h, eval (FAnd (FOr f g) h) true = false.
Proof.
  intros. rewrite eval_equation.
Abort.


Or completely without changing your definition using Functional Scheme 
(https://coq.inria.fr/refman/user-extensions/proof-schemes.html#functional-scheme):

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.

Require Import FunInd.
Functional Scheme eval_ind := Induction for eval Sort Prop.

Goal forall f g h, eval (FAnd (FOr f g) h) true = false.
Proof.
  intros. rewrite eval_equation.
Abort.


On 28/05/2020 15:54, Maximilian Wuttke wrote:
> Hi, I have two ideas.
>
> 1. You could use `change` with patterns, like `change eval (FAnd ?t1
> ?t2) with (eval ?t1 && eval ?t2)`. This way you wouldn't have to spell
> out t1 and t2. Also `change` supports `at`.
>
> 2. You could use rewriting. Have a rewriting lemma for every 'rule'.
> `setoid_rewrite lem at num` could be used to specify the position where
> to rewrite (I usually try out different values for `num`).
>
> On 28/05/2020 15:41, Agnishom Chattopadhyay wrote:
> > I realized that hnf was not working because what I had was something
> > like "(eval (FAnd (FOr f g) h) x) = ...." but it does seem to work when
> > I pull out the term and use hnf on it. Is there a way I can use hnf on
> > one branch of the equality?
> >
> > The issue with most strategies I can think of is that they are becoming
> > rather long-winded, and I am having to copy-paste large chunks of the
> > terms obscuring my proof text, especially for something which is a
> > rather simple algebraic manipulation
> >
> > On Wed, May 27, 2020 at 7:08 PM jonikelee AT gmail.com
> > <mailto:jonikelee AT gmail.com> <jonikelee AT gmail.com
> > <mailto:jonikelee AT gmail.com>> wrote:
> >
> >      On Wed, 27 May 2020 17:45:55 -0400
> >      "jonikelee AT gmail.com <mailto:jonikelee AT gmail.com>"
> >      <jonikelee AT gmail.com <mailto:jonikelee AT gmail.com>> wrote:
> >
> >      > 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
> >      <mailto: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:
> >
> >      It might not be working for you if the term is "e = (eval (FAnd
> >      (FOr f g) h) x)" - meaning that the head is equals, not eval.  You can
> >      use the set tactic to pull out the rhs of that equation, and use a match
> >      tactic to drive the set:
> >
> >      For instance, if your goal is "e = (eval (FAnd (FOr f g) h) x)", one can
> >      do something like:
> >      match goal with |- e = ?R => let t:=fresh in set (t:=R) in *; hnf in t;
> >      subst t end.
> >
> >      If the equation is intead the type of some hyp H, use "match type of H
> >      with e = ?R ..." instead.