coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] unexpected lia failure

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] unexpected lia failure
Date: Sun, 19 Sep 2021 10:15:40 -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-ed1-f45.google.com
Ironport-hdrordr: A9a23:HpkWQ6MXFYYJI8BcTsyjsMiBIKoaSvp037BL7TEXdfUxSKalfq+V7ZcmPHPP6Ar5O0tApTnjAtjjfZq0z/ccirX5Vo3SOTUO1lHYSL2KLrGP/9QjIUDDHyJmupuIupIRNOHN
Ironport-phdr: A9a23:pP8MphFTTUgrMvRi+DXuIZ1Gf/1MhN3EVzX9CrIZgr5DOp6u447ldBSGo6k31BmYBM6GtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys55HfeQFFiCeybb5yLhi9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7alkVQXohT8IODA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGp+xYJAPD+oAJuZYr5fyp1gTphaiAwmjHuXvxSJVjXLxx6I1yOQhEQDd3AwgAd0Os27Yo8/zNKgIV+C60bPEzTTCb/NK1jfw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtIPqMS+P2OsXr2ib8/RvVfipi2M/tQx/oiaiy9ojh4fGm48Z1F7J+Tt6zYspK9C2SFB3bNGgHZZSqi2XNZZ7T8MiTWxquys3yKEKtYClcCUJy5kqyRjSYOGJfYiP5xLsTueRITFgiX15f7K/nRCy/lakyu34TMW7zktFrjdDn9LRtX4NzwTe5tabRvZ55Eus2jaC2xrN5u1YIk04j6XWJp4nz7UtjJQcq17DETXzmEjujK+ZaEEk+u+w5uTieLrmp5ucO5ZqhQ7jL6gig8K/DOs4PwQUUGib/uO81LLn/ULnWrlFkvo2kqzBvJDbI8QUuLK5DhdL3oo/7xuzFTSr3dQCkXUZMF5IewiLgofpNl3WJfD3F/a/g1CikDdxwPDGO6XsDY/WIXjDkbfhZrZ95FBfyAYp199f4YhbCrccL/7pW0/xtcDYDhAiPgy7xuboEtR91ocEVW2TBa+ZNbvesUWU6eI3P+mMeIgVtS7hJPgi/v7ilGM2mVsAfaayxpYXc3C5HvF+I0qDe3bsg9EBEX0LvgUkVuDqhkeCAnZvYCO5WLt57TUmAsryBoDaA4upnbap3SGhH5QQaHoQWX6WFnK9Xo+EWuwMZSHaC8lolDBMAbGrS4461Ryt8gb8wrxraOvV5iIwupfq1dwz7OrWw0JhvQdoBtiQhjneB1p/mXkFEmdeNEVXrkl0y1PF2q990aQw/TN76PZAUwN8PpnZnbUS4zHaXwvAepKERA/jTIn7Rz42Sd01zpkFZEMvQ72f

Require Import NArith.
Require Import Psatz.

Lemma liatest (n m:N) (p: N.lt N0 m): N.le N0 (N.modulo n m).
Fail lia.

Is this a bug or a feature?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] unexpected lia failure, Abhishek Anand, 09/19/2021
- Re: [Coq-Club] unexpected lia failure, Abhishek Anand, 09/19/2021
  - Re: [Coq-Club] unexpected lia failure, Laurent Thery, 09/19/2021
  - Re: [Coq-Club] unexpected lia failure, Frédéric Besson, 09/20/2021