coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] merging functions over disjoint domains
Date: Wed, 27 Apr 2016 14:28:44 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f173.google.com
Ironport-phdr: 9a23:b54i5RH5vI3RDrFBGMrwLp1GYnF86YWxBRYc798ds5kLTJ75osSwAkXT6L1XgUPTWs2DsrQf27qQ4/qrBT1IyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6biodaPMk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET5uZ2sy/YjgsQTJZQqJ/HoVFGsMxElmGQ/AuTjwXpbqsib5/sN70S+WdZn/R7A1QjSv7OFiThbuhGEGNiI22G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZCSA==

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.

[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