The Coq mailing list

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

Change with patterns seem like a very good idea. I have not used patterns very much yet.

I should also look into the Equations package.

Thanks all!

On Thu, May 28, 2020 at 9:15 AM Yannick Forster <yannick AT yforster.de> wrote:

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