Stream: Coq users

Topic: coqidetop died badly.


view this post on Zulip leafGecko (Apr 24 2021 at 09:54):

Inductive nat: Set := O: nat | S: nat -> nat.
Definition x := S (S (S O)).
Print x.
(* Recursively define plus. *)
Fixpoint my_plus (u: nat) (v: nat) :=
match u with
| O => v
| S(u') => S(my_plus u' v)
end.

Compute my_plus S(S(O)) S(O).

when executed to the last line, the coqide shows the "coqidetop died badly." error.
Any help is appreciated, thanks in advance!

view this post on Zulip Michael Soegtrop (Apr 25 2021 at 08:09):

Some more information is required. The following does work for me (with Coq/CoqIDE 8.13.2, but very likely also with previous versions):

Inductive nat: Set := O: nat | S: nat -> nat.
Definition x := S (S (S O)).
Print x.
(* Recursively define plus. *)
Fixpoint my_plus (u: nat) (v: nat) :=
match u with
| O => v
| S(u') => S(my_plus u' v)
end.

Compute my_plus (S(S O)) (S O).

Note that Compute my_plus S(S(O)) S(O) without outer parenthesis does not parse in a usual environment, so I guess you are doing something slightly different than you wrote. In Coq parenthesis are not used as function call operators, but to group terms. So fapplied to x is written just f x or (f x). f (x) is also valid - a redundant pair of parenthesis around x, but a bit confusing.

You would get a stack overflow if you use very large Peano (non binary) numbers:

Require Import Nat.

Compute (pow 2 15). (* Works *)
Compute (pow 2 16). (* Stack overflow *)

but this is explicitly a stack overflow and not a "Coqtop died badly", but that might have been different in older versions.

The Coqtop died badly is more commonly a configuration issue - things like using file names or paths which are not valid Coq module names, but then you would get an error earlier.

view this post on Zulip Michael Soegtrop (Apr 25 2021 at 08:15):

OK, I see this is already solved in a double posted thread.

view this post on Zulip Michael Soegtrop (Apr 25 2021 at 08:16):

@zhengyu shi : in the future please avoid to post the same question twice.


Last updated: Mar 28 2024 at 21:01 UTC