coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] termination when branching with fmaps

From: Lorenzo Gheri <lor.gheri AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] termination when branching with fmaps
Date: Sat, 20 Feb 2021 19:33:18 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lor.gheri AT gmail.com; spf=Pass smtp.mailfrom=lor.gheri AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f170.google.com
Ironport-phdr: 9a23:hPdAfhWs/dGfNCqax2+Ih9zfbRvV8LGtZVwlr6E/grcLSJyIuqrYbBeFt8tkgFKBZ4jH8fUM07OQ7/mxHzNQqsfd+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiyoAnLtMQbgoRuJ6I+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuB2upxJ9zIDUbo+bN+dwcL3Bct4BX2VNQtxcWjZdDo+gbYYCCfcKM+ZCr4n6olsDtR2wBQ62BOzxzD9Jh3j21rA73eQhDw7Gxg0gFM8JvXTQq9X1Lr0eUe+1zKbW1zXDbuhb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmTe+ii3MrpgByrzav28oihInHi4wVx13a6Sh0w4k7K9KmRUN5f9KoDpRdui6aOoZoTM0vQG9mtTsmxrAGuZC1cjQHxZI6zBDRbPyHdpKH4hPlVOuJLjd4hW5leLKihxmp60Sv1ur8Vsyy3V1XrSRFisHBum4R2xHX8MSKSftw8l281TuO1g3f8PxILEIomafdNpUv2KQ/loAJvkTGBiL2mFv5jKuRdkg8/+in8eXnYrH/qp+dM494lxjyMqozlsG9Heg0KAcOX2+c+eSz0L3s41f1T6lNjv0ziqXZsZbaKtoHpqOhHQNZzoIu5wy8AjqmytgUgHgKIVNfdB6ajYXlJ0nCIPXiAve+h1Ssni1rx/fDPrD5BpXNKWLDnK3ufbZ99UFc0gszwMtQ55JREL4BIfbzVlXtu9zfCx81Kxa0zPr/CNVhyoMeXnqCDbOeMKPLqFOH+uYvI/SXa4IOozb8K/0l5+b0gnMjmF8de7Op3ZoNZ3yiEPRmORbRXX25idAYVGwOowAWTerwiVTEXyQASWy1WvcY4Ss2DpChRajDS5qsyOiF2z39EZ1bfGFuBVWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEn36V3KjoF/J++RwRU28JLu0N8vub/WnBA2sD1wVoGTij7VCW5zmWwMSnk926Ut+RUhmGfG6rBxhrljLfIW/+lAC15oOpvVzug8ANf3CFqYL4W5DW2+S9DjOgkfC9c4wtsAeUF4QozwgRXK3i7sCLgQxeWG

Hi All again,

thank you very much! Also for the pointers to the examples in finfun.v

Best,

Lorenzo

On Fri, 19 Feb 2021 at 17:07, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi,

> Finite maps are based on finite functions which allow such nested
definitions,
> You can find an example in the doc:

There is actually an example about tree in the header

https://github.com/math-comp/math-comp/blob/17dd3091e7f809c1385b0c0be43d1f8de4fa6be0/mathcomp/ssreflect/finfun.v#L24

the depth function is simply:

Inductive tree : Type := node n of tree ^ n.
Fixpoint depth (t : tree) : nat :=
match t with node n br => (\max_(i <- codom (depth \o br)) i).+1
end.

--
Laurent

[Coq-Club] termination when branching with fmaps, Lorenzo Gheri, 02/18/2021
- Re: [Coq-Club] termination when branching with fmaps, Li-yao Xia, 02/18/2021
  - Re: [Coq-Club] termination when branching with fmaps, Lorenzo Gheri, 02/19/2021
    - Re: [Coq-Club] termination when branching with fmaps, Matthieu Sozeau, 02/19/2021
      - Re: [Coq-Club] termination when branching with fmaps, Laurent Thery, 02/19/2021
        
        Re: [Coq-Club] termination when branching with fmaps, Lorenzo Gheri, 02/20/2021
    - Re: [Coq-Club] termination when branching with fmaps, Marcel Ullrich, 02/19/2021