Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A well-order on lists of natural numbers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A well-order on lists of natural numbers


Chronological Thread 
    < Chronological >      < Thread >
  • From: Michael Sÿfffff6gtrop <msoegtrop AT yahoo.de>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A well-order on lists of natural numbers
  • Date: Thu, 25 Nov 2021 08:57:33 +0000 (UTC)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=msoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic305-20.consmr.mail.ne1.yahoo.com
  • Ironport-data: A9a23:4LPZmKy+GABAgVLCuTJ6t+c7xyrEfRIJ4+MujC/XYbTApDNwg2QBy2QWDDjSOf2LNjHzed1xOYWz/B8H6pTUzNcyOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYueJQUVUj/nSH+OlUrOcY0ideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kuq38dEwBGeaPeFLWzHFRXbOnmF5Hry02lKA2bbwNYEdQjHOCmNUZJNdl68L2EFlyePScxaJED0cw/yJWZcWq/JfCOn+yvtCJyFXuYnLsxPIoAExe0Ygwp7ctXToTpZT0LxhWNk3e2Ypa2omTQe51w88nMcPDJ5IaongmzDfDDP9gT4qrfklgzcsAiWx22tQXSK6YP95DPGIpNkqbOgkUbw9RVYZhyc62olL6VxFYjHOcg5YtxXyKlFkplOD5WDbOUseNQ8RexR7F4zieuW/+BAofLpqawDuBtHSh36nelCP8X8QZE7jQyxKju3XLrkR7NfHcfQLTTTiFZk+CtxZ3MEsS+yF19fV3rhTtRd77RBii5nuNvxpaXdcJVfwz6AaKjKHT5m51w0BsoiFpMLQbWA0eHFTGFWNlW/v4DDxot/uZRBpxM5+K+CiqN3F9wXAqPEc5oMhs3zUniJA6jhXICNpueEJwprUZBhmoqw23QOMCa3n/QCLFO2hXPbwKvt50mqX0cw==
  • Ironport-hdrordr: A9a23:EmJjfKio4W2VJA1On33XO+6XenBQXu0ji2hC6mlwRA09TyXBrbHLoB1p726StN9xYgBapTnuAsm9qB/nmKKdpLNhWItKPzOWwldATrsSjrcKqgeIc0aVygce79YDT0EUMrLN5C1B7PoSlzPXLz9P+rW6GeuT9IHjJj9WPHhXgo9bnn9ENjo=
  • Ironport-phdr: A9a23:HMpIfRd8ChlXzhgvHrFgvi4elGM+Zt7LVj580XLHo4xHfqnrxZn+JkuXvawr0AWQG9mKoKsd2qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfglEnjWwbLd9IBmrsAncstQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kqFVrxCvpxJizIHbfI6bOv1lc6PBZNMVXnZNU9xNWyFDBI63cosBD/AGPeZdt4TzoFoOoge+BQa2GuzvzidHiGL4xK003eQhHw/G3AIhEtIBrHTUttL1NL8PWu2yyanI1jLDYO1Z2Tfh8ojIdQghrOqMXL1qccrRzk4vGxnYgVqOsIHoOS6e2esRvWaB9eVgSf6vhHA9qwF3ujWj2MQhh5TUio8XxV3J6Sp3zYIxKNO2VEJ2fNGqHZ9Tui+VOYV6XsIvTm51tCom1rEKp5C1cSYKxpg52RPSZfyJfo6V6RzgTOacOTZ1iXN/dL6ihhu//1KsxvD/W8S0ylpGsyVIn9jKu3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLEAvkqrbLZ8hzaI+m5YPsUnPBzH6lFnsgKCKcUUk/POo6+H9Yrn8o5+TLY50igXkPqQohMOzHP40MwgUUGib/uS806fv8lH+QLVPlvE2k6/Zv47GJckDp6O0AhVZ3psi5huxFTuqzdcVkHkdIF5Ydx+KjpDlO1TUL/D5Cfe/jU6skDBux/3eO73hGZLNIWbMkLf9Z7Z97FZcxREzzN9F55JUDbYBLOjuVUDvrNDYFAM2MxSow+b7D9Vwzp8RWWWWAqOALKzStUKI6fk0LumXZI4VvS79JOI/6/7vi385g14dcrOz0ZsZcnDrVshhdg+SZmOpidMcG08LuBA/RarkkhfKBTVUfjO5W782zjA9EoOvS4nZENODmruEiQK6FZ1fa2RxMceCH3nmeduLR+0LcGrGJ9RmnzMYT7+5Y54o1Rap8gP3nek0ZtHI8zEV4MqwnON+4PfewElaHdlcHs2d1GbLQ2wmxgvgqBcn1aB4pgpxxwXauUCZq+dfE91YvKsUF11ic5Xbyfd/EZb3UwPFONGEERC3S9WhBnc6Sddjm7cz
Hi Ian,

> Theorem listnat_strong_inductionT:
> forall P : list nat -> Type,
> (forall l0 : list nat, (forall l1 : list nat, ((l1 << l0) -> P l1)) -> P
> l0) ->
> forall l : list nat, P l.

you don't need the lexicographical ordering - the length is sufficient, so
that this can be proven for all lists (not just nat):

Require Import List.
Require Import Arith.Wf_nat.

Theorem induction_list_length : forall {T : Type} (P : list T -> Prop),
  (forall (l1 : list T), (forall (l2 : list T), length l2 < length l1 -> P
l2) -> P l1) ->
  forall (l : list T), P l.
Proof.
  intros T P HS l.
  apply (well_founded_induction_type (Arith.Wf_nat.well_founded_ltof (list T)
(@length T))).
  unfold ltof.
  apply HS.
Qed.

Best regards,

Michael

Archive powered by MHonArc 2.6.19+.

Top of Page