Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq tatic help

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq tatic help


Chronological Thread 
  • From: Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] coq tatic help
  • Date: Sun, 17 Mar 2019 13:01:19 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s8mawutt AT stud.uni-saarland.de; spf=None smtp.mailfrom=s8mawutt AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
  • Autocrypt: addr=s8mawutt AT stud.uni-saarland.de; prefer-encrypt=mutual; keydata= mQINBFWVkZsBEADmp2Mq5XZcOg38F91SMR5uF8cqC7LaODrnF+xh3TNKgbK301sPwcSKA4gr +TKV73e4VQoWihiWaYfPJYHsudXrp644dqYvWuxNWlkh4S2HIOmcopuTEd063TL5hRvhkg0V ZOMq000ucKo0yBsUux7+TdZdDAX3WP1whF7jY8OTe5xnEO3yv4xydAZhbT/gMO/IW6BVE2xO eElXEwC8Tnssar8cM0wZcnxgKXq4dhjDO6sSkeaf81a6FPlpy+VuCIHFYoFIAquX6T6V+Zbi UXJyDSUSUVVmechLA8vXmiRgOTyVMdTejXQb5niLGjb/Upvy9uSlO7eR0aSkCs3vqeXIppmS PDTKVwPso/PmJHEJnZLrbXKqqh589pbDAdYfJvP3Sg0fncL5bzxV0gdSqWH0t0e7c9AMiHs5 5bxEHBXuVtNs1srF52gT0KlE84R2UOmZ9Kst7P3XgJtIGzuS5uSHqFmtknh9tj+/G/Kg3qDz njxM6xTGExNPHQuskwbvYDqA6/5Hslqis6D6EpMPGhRuUhPuE5Eb+PsxpV26UccZt51FqIIc Mwv+3AUPbF7v7s7rAE1BkbmClUGuYUGfqfndGT4V6fLpQH5F9kRdxmIm9FcMURUDvX4CBKZz gmwIZ4jgZ2jZ1VTy+MWIXRpgJIt5aim4liycyDoPk+fyYfdmQwARAQABtDFNYXhpbWlsaWFu IFd1dHRrZSA8czhtYXd1dHRAc3R1ZC51bmktc2FhcmxhbmQuZGU+iQIwBBMBCgAaBAsJCAcC FQoCFgECGQAFglcSYFwCngECmwEACgkQ7Ve7Ztu9/N6Nng/9Efrx3z5menrcwHILe2WX/i2i 8zFu8a3dqFZj0kgj8AumdUwbvOYv0mMBEG7c+6YNsQEw21mjKQGEw7GSOlN++K0xiZnlzULc DZlVxrH0Eg7fr/NNpQiJeCxFzxjMqMtitIbUh9BIFEnVOLsySLUoMRB77+/g8Lf0fJ5bTxfw 8xXg7has6p/J8Zc3Y19128o3BrBhDVYbYub+NeqwmHUdIbiPn+QsuhDpmvYniw5gsFm+KP7t YRpExeVT7ZuHFPiCQfHVbj0s4TzXMRFBrruOefreC2kg6e1YNpPRQolUYkc8kwIdPYF5oBC3 oRlgRiYMs+nGOyQcrPWz78PyycsuCrvOg0oDja41aNtL3PiZtqZf0Ih0GSNP6X0++I+ZIyR8 TZQyguRWb0z0anq1LhH/vRnXefH4zListwKwJViQsKPGXANu6qZpvwn65iH98+dT5uwKhHhl h3qTNx43WGOo57ETrsF8vpl++IotCFqihwUK6yV30xxZaOTa+p00QYzE34ZoRRgKdtclD0b1 aQciJ/k+BYjxy/vl8ZgiSpOLlI1jSncX6AKeq4KpmvbV96QdVrErlUsQULPRHiePi3hot9yS BRg7J5Z3mzLMt/rdfJIb8/bkxZGbqXl6LoxAvE1Io+fvFMOTSer47Los3MJO+smC/SstQczS BKOT0Cf+Ase5Ag0EVZWRmwEQALwwnvtVw/zFec+MNKgBwKt1MIG6EMBKc+OTIYM2tN4jcWla AbEcIZGkBSeoPJeTi4m3GQXhifGZK29VoDIUQjYYDWNtp6U8y0hLRnqSVY/YvcTDnK929n5r qMqO0wYf1fzhmPshIyD1jj96tqu0ppX7zE++VQ/VJgVIA8IGcNXUN21A/+rJKCJFAvBp+6u2 gNaUDfnqvPfTGtkq7A/D40Lo6y0KVu20R3W76iFWl6FEQzOe28VBnOjU/NbyzAzVUSgYCSfk YxhDiKfJRJvQd+VKUCAa+BSNoEPvDMKakvhApWUOncnNUbfXiH04fYSViu2NH2Ls3HLm+6xa Aaf9eUIU75A02xXUa6m+AccJQzCEJySeYJFVhJLSgZEbGwDZVdrRALolgYiIrwOHTitC2PLR ej8HeywQrn3PUGBwiYdOa19KTHZykbO0s0SHb6bvm3vgpAPPdZp+QWPOXx3aZz6dw4D867li sGVKMcKBcX9QCekVL7CW6lvvevUP5tBBYCshMvSTaN0BymBBwYrz8UB4RYJ4cUs5apd1mMfD 5Vm8EZf1DT15Q+K9+HsRQr3y/+AtHm0gd0DpXGfBH4H+54vyB9Aj3DVbyPMeFYv9UhyKALEo mprFM0tr0+SPh275xXlIxUvoC+3PlFM0swoLSmi2Tu9edjU6GuyL91w/9WTjABEBAAGJBD4E GAEIAAkFglWVkZsCmwICKQkQ7Ve7Ztu9/N7BXaAEGQEIAAYFAlWVkZsACgkQIA5mg0qOKkAo DhAAnms7o654V2uZWBsiiR2oEykGs/sIzxYcKrOi2RnkL6RAwhJgBr+WVpjQ2IS9IQ5Bxy8G OWhzyit2XvFYTWxGamrmyXol7IynGcl2U3WpmSQEPJx/QeyQ5lWLYzjn5bbdzNdY0mhUnRZ+ ke2tcttmvLsUKn2J/8lSyqBF4i4Yaj4p4LQ8n/K/eW9lIY+J/gVGDcrlZqOozXV9aClYDtgx L/c6/TPuDi0vgkhIaojwsSu38YmhmbYP03ntiLTrLbjnJXr0pYIlMRqUmNvPsphOR8cVGFnZ 50dVoWHSSJhoIESpu8Qz1qwvA9uNTDhe/nnr092diP78FWo4SENiKjrXA2fOjk0YoZA1uSL0 RbcRKAttPC88iBWUyBwYrhMBFKzJeDG+lvBID8gED205Jy7Mk8v7R9NqHpjJXST1avVMF7TX CH8OK7rgI9ATGLqJ31WoYZkCSFkYKYRbyarZnVKxMsQ1zhpjoEfuQlWaq2NgwS2cijWmKAmF V4Qv3FA5zAoEdzB9HCbT2DafITEUqjf111+WjNcfJvtfQcO7hghhMwFtW9Or9KqVKpEDraku uHUr6nVnBNYCliY80m/X5DXOZsKzehxfHht4t+CydGE2xRzIwzpos2ZebhkjWmghGS7G1JHA DgEk7zBKyVxJm/nwwNGk5MdY9sckx8XMiaA5lV2oDw/+K7mXo2qbEPnghGjN2bAqYbZd/Wdh 5SUwa5YvnfqWcSY7G8OA5pexnIV/5RRIdcc+RtrxADmfTYGVIvSfAS4uwALIgEd5LYdYBIaj xWLCyNghoQowLqZbIQQ4eOWd2xCF6srcTsIou2kJ97iiFtXgX3PthKn+fhdFYWktEDabDhgY SdqJVvs+Sk3lO41aJu5MSIsqWq+G0ZGumTtO/yR9x5RzA/qKn56S6Da8WjRF6iq/oyemifyC 74HXmmi6gd8HCWD+eEXNWVAVL/FlfYhL420olMcBgP+cMGJTpmWK5jCyaxHH4RFYg8AAdzn0 /Lc/Xr47IZBntCaLy3V1LSKvDSZackKOreBmxQrd2Qn5/seLYFWWl/rPvqib6hmoE17SjBI2 szi/t37JGXTl0ZkhSUp6FSC4YmoFrKJgxuX0q7CONZzdZ9G7mNOkUdg3QAaN6/EZQceGC/Dv i28jB57Y50OoOAcyJnSkS95lPobHcGbBDDIQVvcEBwhSir/coGXHk8tqMXCdhxDo9Tq1cSvA NeRYuJdrTdJM2FMll7QEtBcto0DNCNEecvZ+D/uqOU+InyJHpD4qDpQR8bqNJ3Fmehd54LYi ZK2G5/gRwF+8vnaeoy9fSs/CAw3icKPTcSSmy9bOk3I0fgAyb63xLF/sGHAOq5gkPg+9o79d HcbtD425Ag0EVZWRmwEQAKYFa3Y6d5D34YkaNBYvjU3mUlaS2uq7khoVxhnPiad496PzpxpF 76rwpAbh7+V+aqxFDldmydjV3REPgJKk5hnhJ2ndltaoy0CtzFOjUV2KkzzvG2YXADSKCqvL rtVx3wfAxOVxjPOlFzG57mvZd3MUlxOGJPvNbFJJY98OzjQGeCukITMO4mivublSlJy8hNkw bMgkAfBkuITNXllrLfTxch6wikunYlDrtI2X1/h6ygXn/m8dYWzDGv80PyzVHWNMz7JS5UuD 7PkkazkqLzH9HQ+xj2x7KOWIHs9BQp99OrZfUMcD54EfoM0JUG5kq0Xs099Z4UEFA2Pl+8mn n7z7NNZ1JSN0xjUuxhMu5deIkKEj8XGwB+6OXYEhF3mdh5T29C4LHDpp3fpa9LU+8Dlpq0HJ lwBx5ngXOfAmZrKAJhiy8kT3AfNskiVWxgYga2Kk2ku8vV4DkMai7kzK45t0/cDwdgugeck8 3x/7yR9XIrBwlt8N4bdJ3URbOtnuGuYjM5RTtqpadjVLLr+ZdhKPdM7qtPfnHotjRq+ban1T dA/zlCOW+s4g955kvafY29qnhx54y+DQJUwELAZCTA0fT/eHs0n6M/gILepMleBR7STA+Xqn I5aWlWn3Pp6nI8t3bz0T6sFEocD++YJNEr/J7yduvcNaI84j03iRMfPjABEBAAGJAh8EGAEI AAkFglWVkZsCmwwACgkQ7Ve7Ztu9/N4GJA//f21oF6/XClyTnbsNSBKLvbtb9CjKx+9c6B6k 1qHePSylFf+BsrKFMEdtyn40bfVnQqQ1GzNFFbzGiFkUlwM1BZMR0ogl6ahtJL3M4Tf7RkV6 FUhkov5HwYIXDjx9WdboLPPz4NQkomgcWyc0vAndtL1vYFizVLkxIdWonnv11M4MoQybCjv9 lm+UwmoqLkSvrWn3F6RMPwsc4HWDRHiBYNkCxYGlfVfQax1u3ENH7KfEnZAEEoxSBkaha1Tv /06wHjQ9w+7ZwueiB48MCQleDM4xP+Geom/VIhExdySrAtGZEP7DjCpcXTYL6491G1gDdStp zSU0odKKxp3xUgB7gFuegBsM4dXm02Q6tzr+oVLkCeTGWld3/DfyIVVi3f2w+g+JEE8W71Gx uIw4IwuxXr0sGo1gHnH8CD5ky0/dGYfW644oZ6DQRzDqp+7sJNGoSOmEbJ5k7IgkPlwb41jN Ez1miq/AIleDjVgM6ZP1g4eVAWgjATFqfv9y/WR1t1BvrcogGKdVLfRr6kDYwP2GzzCGz2Ki VtlPaPv52UYPa9zX6IT5hEOq4GSAVo2IHwtukyG10l7sanq7J6s5CumNukDzuJxJ+EgNYIxa EtdujUPJxlRQcFwqjbLEt2LQBJivwzRhRmQfQz5tt3c797Tsto875TRgvFHu+ezStimb9ew=
  • Ironport-phdr: 9a23:7S3P2RY9e6NpdMxzNekHTXX/LSx+4OfEezUN459isYplN5qZoMuzbnLW6fgltlLVR4KTs6sC17OO9fi5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCehbb9oMBm6sBjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbZqaNPZiZK7Tes8WSGRDU8tXSidPApm8b4wKD+cZOuhXtYb8p1oLrRu/AQmsBfngyjlVjXD2wK06z/ghEQLY0wc9GN8Oq3fZrNDvO6YcTOC10LXIwC7Yb/NKxDfy9ZLEcg0nofGNRL5watDexlM1FwPBlFqQr5HqMymI2esTqmWW6fdrW+G3i2M/tg18rDeiyt0oh4TInI4YyErI+Tt5zYotONG1RkF2bcSgHZZRrS2XNoV7Ttk8T210uCs3zKANt4ShcygQ0psnwgbSa/yZfIiM5RLuTPqRIS15hHJ5f7K/gQy+8VKhy+HmS8m01ldKojNektbWrH8NzRjT5dKBSvRg5EuuxCiA2xjS6uFCP080ibLWJ4Mvz7M/jJYetUXOEjX0lUnskqObdl0o+u2y5OTmZrXmqIWcN4hxigzmKaQjmcm/Dv42MwgTQ2ib5f+x1Kb//U3kXbpGlOA2kq/YsJzDPsQUvLS2AxVR0ok57RawEi2q38kGknUfNlJKZAqHj5T1O1HJOP33EfC/g021nDh3w/DGI6buD47WLnnDlbfhZaxy51RdyAo119Bf5ohbBqsPIPLpCQfNs4nTCQZ8OAipyc7mDs9838UQQzGhGKicZYbboV6N5+YuKu/EW5IJpDXwY6w+t/vnkmIlhXcGYbSlm4YRaTWjF/18J0yfbTzgj4FSQi8xogMiQbmy2xW5WjlJaiPqBvNu1nQAEIujSLz7aMWoib2F0j28G8cMNHtaF1zKDHHpMp6NUu0IYSSeZMNswGRdCeqRDrQ53BTrjzfUjqJ9J7COqDYEqJ6lyd50ovbanAs2/Dp4SciQgTnUEjNE21gQTjpz55hR5ExwzlDZjvpkmf1EEtoV/eEPTwE7cIXVxvZ+Atb+HA7MLI+E
  • Openpgp: preference=signencrypt

`omega` doesn't unfold definitions.
You need to unfold `ea_in_range` first.

```
Lemma test2:
forall a, ea_in_range a -> a+3<6.
Proof.
unfold ea_in_range.
intros.
omega.
Qed.
```


On 17/03/2019 12:27, 朱立平 wrote:
> Since omega works in the following proof.
> Require Import ZArith.
>
> /Lemma test1:/
> /  forall a, a<3 -> a+3<6./
> /Proof./
> /intros./
> /omega./
> /Qed./
>
> I wonder why error occurs at this:
> /Definition ea_in_range (ea:nat) : Prop := ea < 3./
>
> /Lemma test2:/
> /  forall a, ea_in_range a -> a+3<6./
> /Proof./
> /intros./
> /omega.  /
> Error: Omega can't solve this system
>
> Best Regards,
> Julian
>
>
>  
>

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page