coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equations 1.2beta is out!

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Equations 1.2beta is out!
Date: Wed, 6 Feb 2019 16:18:33 +0100
Autocrypt: addr=thery AT sophia.inria.fr; prefer-encrypt=mutual; keydata= mQENBE3a3V8BCADTeORKU7I7UmBBcs4VhSCq1IgKD8vdmdrGAlF3IJSFng7Fk8+MgS2gWYcS Ukf5t+rjNM3Z6brfYXc1naZlf2JPGHvAGiz8+TkXL+/ZA6+gAoIKy/iKyD+hCD8m92WH3rPH vCX6EJ44FEI7gUJ37GlTjvuP0I55vaFcwEg8nDgkALaCJvrSHtePuPKR1Q+9q2dgR7fTObal HYGMAsgT6k6n2ofe4Q6VFRLJhruU02qAfV5zgIoa3xgrTwSr4RRDILHttAw7EN6aLG6JycJ7 sPsPsiQzrd/tFsNbiHYeojJCkU2pDSQ3pBtXAJL/z2pMWTeTXvA60l9w0sDO7M3mkC3vABEB AAG0J0xhdXJlbnQgVGjDqXJ5IDxMYXVyZW50LlRoZXJ5QGlucmlhLmZyPokBOAQTAQIAIgUC TdrdXwIbAwYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQHHaWvRTi0tpIgggAnSUYcU2N uchXkGGwmPuLmvSUMiLkyFPs9GF2YF1ONOuJtpnQMcpsseCkcmIjESz0h5OpknpyraUXvbh0 ZdFqaLC2E+GyV8/YQi71wSsTPgWP450u0XUt0ysjwkKW6aIxIhSzrtgNp4E6w5KzXVJxA/yM V5RNFHg/5uifgfv4b7xaGHV8L93NbSvedk1O7yje5Hqgfab0t6J5Kf0M3sG+pB3gEkDVK9B7 +0fhe7/5u1Nj5HoLWid8UNZfFzJzb18Xe2ckzNye0KdDtQFac8qGUzhLbEYt3ScYjRYTq9/d V4Cin39j7Oo64Nk71iiLBISyuk0Q9D+Jq7nwwcQr/R8s1rkBDQRN2t1fAQgA7H6aX6BfdO/X Vlf4EGEoyFQ5u/JDe+giIHWSS34YWDWVUYyp320CrAYAkh9lQ1Nvh1tsmgiUh5xnY7wY0tOi wJSm94XlYAmHrddmWVNXRn09GvZJhfI2LdVBg3oxPfc8+bV+Hz83z/5BMPLOogxB22QMPJ6e iD2EsUMPNsuCVQ8WNo6ZmueuuYe7vEUXLYdRXNumJJgekEuG/q1BD4xgfzWpWfUODm6WygWZ oov50DomcDcAHW03bgnHlqnYu20Qg00GqgR3FKlORTvnOxD5TMCXe+eLUxkQfvnjbIPhtrnJ hgJMKVkRBEoaQ/XA4FdvxloInYPbqxNZ72yd09BbewARAQABiQEfBBgBAgAJBQJN2t1fAhsM AAoJEBx2lr0U4tLaWNQH/2/fIaF9ngbKPBJbDxYa7glJuCfamJgy3R8mJ//VYsS4RbdroSX3 29EgWlTx2reu1b4C5n5k7l4KpLgsRIc3bLUasGv15nf8BqmKIMulidzsxJv86S2imY/0870Q NOiO9SElHE7/2q4J1m2ew77SegiqGVWHl6Zs+4ROfOILTy24o26BQMAZhPX7jEs04Atv6yjw OUIPbzFO+XRuKqkBwHn9S8+GQelT0Gh84Dc5D2jIF0+kWY7uHqe2O+2LPfgO2CYhqmVfr/Ym mZv2xUyhJ7gui2hYaggncQ96cM2KhnKlgMw8nStY0GTqVXLEjPYblz8mqtF8aBPRSk/DjjrF QeI=
Openpgp: preference=signencrypt

Hi,

Removing Opaque and cbv could be better for beginner:

Fact Div_Mod x y :
x = S y * Div x (S y) + Mod x (S y).
Proof.
induction x as [x IH] using lt_wf_ind.
simp Div Mod in *.
destruct (le_lt_dec _ _) as [H|H]; simp Div Mod.
- assert (x - S y < x) as IH1%IH by lia.
simp Div Mod in IH1.
lia.
- lia.
Qed.

Re: [Coq-Club] Equations 1.2beta is out!, Gert Smolka, 02/06/2019
- Re: [Coq-Club] Equations 1.2beta is out!, Laurent Thery, 02/06/2019
- Re: [Coq-Club] Equations 1.2beta is out!, Laurent Thery, 02/06/2019
  - Re: [Coq-Club] Equations 1.2beta is out!, Pierre Courtieu, 02/06/2019
    - Re: [Coq-Club] Equations 1.2beta is out!, Jason -Zhong Sheng- Hu, 02/06/2019
      - Re: [Coq-Club] Equations 1.2beta is out!, Matthieu Sozeau, 02/07/2019
        
        Re: [Coq-Club] Equations 1.2beta is out!, Pierre Courtieu, 02/11/2019
        
        Re: [Coq-Club] Equations 1.2beta is out!, Matthieu Sozeau, 02/11/2019