coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] well-founded induction on the size of the derivation tree of Prop

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] well-founded induction on the size of the derivation tree of Prop
Date: Sat, 2 Feb 2019 21:54:42 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-CY1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Oe8bmRIHepYl0haUKdmcpTZWNBhigK39O0sv0rFitYgeKf7xwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicZOTAk7GHZhM9+g75Urx+6vRNz35LYbZuJOPZiY6/Qe84RS2pbXsZWUixMGoeyYJEUD+oGO+ZTspDxqFgOrRu5AwmsC/7kxCJIhnDo26063P0tGhzE0gw9AtkDt3rUo8j1NKYTSuC50rXEwSjfY/5N2Tf975TIchU7rvGNWbJ8a9beyU4qFw7ciFibtI/rPyuN2+kCr2SX9e5tWfy1h2MosQ19vzqiyt8iiobXhY8Z1lXJ+CBnz4s6P9K0Vkt2bNyrHZZeuSGXMoV2T8w+TGxrvSs216AJtJG6cSUM1Z8p3QTQa+adfIiN+h/jVPieITN/hH99YLyymxG8/VS+xuHlSMS70ktGojNCktbXqH8BzRvT6tWbSvRm+UehxDCP2B3J5uFcO0A0krbbJIA9zb4sl5oTtkLDEjXxmEXrkK+WckIk+u+r6+j9frrmoZqcO5d1igH4LKsuhtSyDOskPgQUW2WX5/6w2bL58UHkQrhGlvg2nbPYsJDeK8QbvKm5AwpN34Yt9hm/Dzan0M8GkXUbMV5JZAmKj4juO1HSJfD3F/a/g1C2nDh3wPDGO6XtAo/RIXjbjLfhYbF95lZAxwo01NBT/o5bCrUcIP3oQULxr9zZDhohMwOu2ernCdN91pkfWW2VGKOZPrnS4he04bdlKO6VIYQRpTzVKv4/5veog2Vz0QsWerDs1p8KYli5GO5nKgOXeyy/rM0GFDIotxE5SqSvul2FVzEbXHa/Wa15rhEmQNaoAYfRXdr12eSp3CCnG5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFRDeHwGb9k7gmnsUrB85QiK+PV/iMCspe6j4p14PHWnBA2szdzCpbEij3ffyRPhmoNAgQO8uVnu0UkkQWD1rR9iv1cU9dU4qERC1poBdvn1+V/TuvKdEfBc9OOFAn0ZPyDWWt0ZeNohtgEbgB6BsmoiQ3F02yyGbgJmreXBZsytKXBw3z2IMU7wHHDhvAs

Hi,

Conceptually, when proving one inductively defined Prop from another can be considered as a translation between derivation trees. However, I am recently running into a problem that, when taking this view, such translation does not have to be structural. In particular, sometimes generated inductive hypothesis by `induction` doesn't make immediately sense, but can be applied to some other derivation trees after certain processing, so that some measure can also be applied to argue termination.

The tricky part here is Prop -> nat is not meaningfully definable type, because Prop cannot be eliminated in Type/Set, so even if I know how to define measures on paper, I am not able to define one in Coq.

Is there any way out so that well-founded induction can be done intuitively?

Sincerely Yours,

Jason Hu

[Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jason -Zhong Sheng- Hu, 02/02/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Fabian Kunze, 02/02/2019
  - Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jason -Zhong Sheng- Hu, 02/04/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Matthieu Sozeau, 02/03/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jan Bessai, 02/03/2019