coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variable closure

From: Michel Levy <michel.levy1948 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Variable closure
Date: Sun, 12 May 2019 20:05:08 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michel.levy1948 AT gmail.com; spf=Pass smtp.mailfrom=michel.levy1948 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f45.google.com
Ironport-phdr: 9a23:VSYitRWeEe0h4lEPbfifnwL5T7bV8LGtZVwlr6E/grcLSJyIuqrYbBeOt8tkgFKBZ4jH8fUM07OQ7/m5Hz1aqs/Y4TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrM0bjZVtJqos1xfEpmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJi3YDUboGbOvlwcKzTctwVR3ZOU91LWCBdGI6xdZcDAuQDMOtesoLzp0EOrRy7BQS0A+3vyyNHhn/o0q0+zu8vFx/J3BIgHtkTt3nUqdT1O7sSUe+ryKnE1zHDYO1I2Tb99YTFdh8srPKXULJ/dMre00gvFwffglqMrozlOiqY2+IQuGaV6OpgUPigi28hqwxpvzivwMIshpPXiY0I11DJ8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN0uT3xytCs1yrAKoYC3czIWxJg6whPQdfKKfoiN7x/gT+mcLzl1iXd4dL2kiRu+7U2txfbzW8SwzVlHqzdJn9bSun0N0hHe6syKReFj8UqkxzmAyR3c5v9CLEspj6TUMYQhzaQ1lpcLsUTMACv2mELuga+TbEok++yo5/3pY7X8u5OQLoF0hw7+P6g0lcy/BuM4MgcKX2eF4+izyLrj/UjhTLVLiP05jLXZvYjEKcgHoqO1GQxY34Y55xqhETuqzc4UkHYHIV5dfRKIlYnpO1XAIPDiCve/hkyhkDJqx//aPr3uHJHNImLHkLj/Y7Z861NQxQ48wN1c/J9UBbQBL+jyWk/1rtDXEhg5Mwmsz+b9FNp9zp8eWX6IAqKBLKzStkaI6vszLOmIeY8aoy3wK+Ml5v7rlX82g0URfaiv3ZsNaXC3BO5qI0uDYSmkvtBUGmAT+wE6UebCiVuYUDcVaWzhcbg742QeCYmmAIOLYo2zkfTV2SawHpBSIGRLFEHVQCu4X4qBUvYILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgW6IRmBw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFGVw47MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYhskdoHYkI4BM/7yx6fgmylBLgak7HND5sxoPrR

With mace4 and the assumption

all x ((all y F(x,y)) -> G(x)) <-> all x all y (F(x,y) -> G(x)) .

mace4 produced the counter-model in 0 seconds

two elements 0, 1 in this countermodel with g(0)=0, g(1)=0, f(0,0)=1, f(0,1)=f(1,0)=f(1,1) = 0

With this model, all x all y (F(x,y) ->G(x)) has the value 0 and all x ((all y F(x,y))->G(x)) has the value 1.

This software is at the adress "https://www.cs.unm.edu/~mccune/mace4/"

Le 12/05/2019 à 17:17, richard Dapoigny a écrit :

forall x, ((forall y, F) -> G) <-> forall x y, (F -> G)

--
courriel : michel.levy1948 AT gmail.com
mobile : 0659134253

[Coq-Club] Variable closure, richard Dapoigny, 05/12/2019
- Re: [Coq-Club] Variable closure, Arthur Azevedo de Amorim, 05/12/2019
- Re: [Coq-Club] Variable closure, Jeremy Dawson, 05/12/2019
  - Re: [Coq-Club] Variable closure, richard Dapoigny, 05/12/2019
    - Re: [Coq-Club] Variable closure, Tadeusz Litak, 05/12/2019
      - Re: [Coq-Club] Variable closure, Kenji Maillard, 05/12/2019
- Re: [Coq-Club] Variable closure, Thorsten Altenkirch, 05/12/2019
- Re: [Coq-Club] Variable closure, Michel Levy, 05/12/2019