coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] merging functions over disjoint domains

From: Jonas Oberhauser <s9joober AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] merging functions over disjoint domains
Date: Wed, 27 Apr 2016 23:26:10 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s9joober AT gmail.com; spf=Pass smtp.mailfrom=s9joober AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
Ironport-phdr: 9a23:kcCtwx2+2Lxp6khnsmDT+DRfVm0co7zxezQtwd8ZsegVIvad9pjvdHbS+e9qxAeQG96Lu7QU0aGJ4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6CyZTtnL/js7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCmI4HIHGkIcnwBIChXe4QuyCoygsCz9vOdn8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

Am 27.04.2016 um 20:28 schrieb Abhishek Anand:

That makes sense. I used booleans before but found the automatization for rewriting was not so good. Is there a tactic that normalizes boolean expressions (by normalize I mean here to turn into a unique DNF or such)?

You can use the ring_simplify tactic to get a normal form as a ring _expression_. See Assia's recent post:

https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00059.html

Also, btauto may be useful.

Thanks, that helps : )
Have fun,
jonas

[Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/26/2016
- Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/26/2016
  - Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
    - Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/27/2016
      - Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
    - Re: [Coq-Club] merging functions over disjoint domains, Abhishek Anand, 04/27/2016
      - Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016