coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why doesn't compute this recursive function on Z?

From: Lars Rasmusson <lars.rasmusson AT ri.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Why doesn't compute this recursive function on Z?
Date: Fri, 26 May 2017 06:30:42 +0000
Accept-language: en-US, sv-SE
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lars.rasmusson AT ri.se; spf=Pass smtp.mailfrom=lars.rasmusson AT ri.se; spf=None smtp.helo=postmaster AT se-out1.mx-wecloud.net
Ironport-phdr: 9a23:8A30DhVvNgpAHvTaKvRbI5in/FbV8LGtZVwlr6E/grcLSJyIuqrYbBCOt8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwewt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZIYJEuEPP/tXr5PlqlUOsxWwGBWsCu3sxD9JmnD50rY30+s9HQHDxgEsA84CvGrSod7oNKkSS+e1zKzQwDvFdfxWwyz945XUfB87uvGMWK9wcdHKyUkoEQPOk1KdqYj/MDOPzeQBqXKb4PB7VeKqlm4nsBpxoj+pxso3kInJh5gZykva+ihgxos+ON62SFZjbNOnFJZcrT+WO5VrTs84XW1luCY3xqcCtJO1ZCQG1YgrywTCZ/Cbb4SE+A7vWPyQLDp7nH5ldqywihWu/UWlz+DxVNS73VRJoydAkdTDq2sC2h3W58SaRPZy40mh1DOM2g/P9u5JI0Y5nrfBJZE72L4/jJ8TvFzDHiDonEX2i7ebdl469eSx7OTnf6nmqoKGO49xhQDyK6ovldKjDuQ8NQgOQnWU9f661LL94U31WLRKjvsonanFqJ3XJsAWqrSnDwNLz4ov8QizAjem3dgCmXQKIkpJeBedgIjoP1HOLur4DfC6g1m0lDdk3erGPqb7DpXXNHfDi7Lhfatm605Hzwozy8tS54hVCr0bO/L8RFf9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaEsKEKAJHHon90pEGEQvwN4QvagwAmJVicWbHKvVYo94Cs6AcSoF9GQaJqqheml1T2gVqdffWVbEUuLFz+8c4yeQLEWYTmXP9R6lTosT7nnUIJ3hkLmjxPz17cydrmcwSYfr5+2jNU=

(** * How can I compute with integers Z in Coq?

I write the sum of 1 to n with well-founded recursion,
essentially like this.

fix sum_n n _ := if 0 <? n then n + sum_n (n-1) _ else 0.

When using nat I can use Compute to run the function
but when using Z the program doesn't reduce.

*)

Require Import Arith.Arith Program.Utils Wellfounded.

Fixpoint sum_n (n:nat) (H: Acc lt n) {struct H} : nat.
refine (if dec (0 <? n) then n + sum_n (n-1) _ else 0).
apply (Acc_inv H); apply Nat.ltb_lt in e; auto with *.
Defined.

Compute (sum_n 50 (lt_wf _)). (* Prints 1275 *)

Require Import ZArith Zwf.
Open Scope Z.

Fixpoint sum_nZ (n:Z) (H: Acc (Zwf 0) n) {struct H} : Z.
refine (if dec (0 <? n) then n + sum_nZ (n-1) _ else 0).
apply (Acc_inv H); apply Z.ltb_lt in e; split; auto with *.
Defined.

Compute (sum_nZ 50 ((Zwf_well_founded _) _)). (* Doesn't reduce... *)

Attachment: smime.p7s
Description: S/MIME cryptographic signature

[Coq-Club] Why doesn't compute this recursive function on Z?, Lars Rasmusson, 05/26/2017
- Re: [Coq-Club] Why doesn't compute this recursive function on Z?, Anton Trunov, 05/26/2017
  - RE: [Coq-Club] Why doesn't compute this recursive function on Z?, Soegtrop, Michael, 05/29/2017