coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] avoid recursive expansion with simpl or cbv

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: michael.soegtrop AT intel.com
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] avoid recursive expansion with simpl or cbv
Date: Mon, 21 Oct 2013 14:24:43 +0200

On 10/21/2013 01:48 PM,
michael.soegtrop AT intel.com
wrote:

Fixpoint even (n:nat) : Prop :=
match n with
| 0 => True
| 1 => False
| S (S p) => even p
end.

Eval simpl in even(4).

One possible trick is to artificially reduce the number of constructors so to stop the expansion.

Goal even(4).
assert (exists n, 2 = n) by (exists 2; auto).
case H; intros n H1; rewrite H1.
simpl; rewrite <-H1.

[Coq-Club] avoid recursive expansion with simpl or cbv, michael.soegtrop, 10/21/2013
- Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Laurent Théry, 10/21/2013
  - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Arnaud Spiwack, 10/21/2013
    - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Nuno Gaspar, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Laurent Théry, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Robbert Krebbers, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Gert Smolka, 10/21/2013
        
        RE: [Coq-Club] avoid recursive expansion with simpl or cbv, Soegtrop, Michael, 10/21/2013
    - RE: [Coq-Club] avoid recursive expansion with simpl or cbv, Soegtrop, Michael, 10/21/2013