I’m trying to define a “partten” function in Rocq. This function processes a list and returns a list of natural numbers representing the consecutive repetition counts of elements. For example, partten [Red; Red; Blue; Blue; Blue; Green; Red; Red] equals [2; 3; 1; 2]. For some types I can define such function:
Require Import Coq.Lists.List.
Import ListNotations.
Module bool_partten.
Inductive color :=
| Red
| Green
| Blue.
Definition color_eq_b (c1 c2 : color) : bool :=
match c1, c2 with
| Red, Red => true
| Green, Green => true
| Blue, Blue => true
| _, _ => false
end.
Fixpoint partten (l : list color) : list nat :=
match l with
| nil => nil
| hd0 :: tl =>
match tl with
| nil => [1]
| hd1 :: _ =>
let p := partten tl in
if color_eq_b hd0 hd1
then
match p with
| nil => [42] (* will never happen *)
| p_hd :: p_tl => (S p_hd) :: p_tl
end
else 1 :: p
end
end.
Compute (partten [Red; Red; Blue; Blue; Blue; Green; Red; Red]).
The code above define take use of color_eq_b to define parttne funciton for color.
However, if I can’t define a bool function to compare two elements of certain types, it seems that I can’t define partten funcion for that type.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Logic.Classical.
Module prop_partten.
Definition T := nat -> nat.
Definition eq_T (t1 t2 : T) : Prop := forall (n : nat), t1 n = t2 n.
Fixpoint partten (l : list T) : list nat.
destruct l as [| hd0 tl].
+ exact nil.
+ inversion tl as [|hd1 _].
- exact [1].
- try (destruct (classic (eq_T hd0 hd1))).
Abort.
Here I try to destruct classic (eq_T hd0 hd1) to compare the two elements (hd0,hd1), but this tactic fails in Rocq. It says:
Incorrect elimination in the inductive type “or”:
the return type has sort “Set” while it should be SProp or Prop.
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort “Set” because proofs can be eliminated only to build proofs.
Is there any method that I can define the partten function only using a Prop function to compare elements? Or it’s just impossible to do so?
Basically, yes.
What is happening here is that you are writing a term of type list nat. list nat is a “computationally relevant type” (something in Type) and not just a proof of a proposition (something in Prop). (You might think of “computationally relevant types” as “actual data.”)
What you presumably want to do is make a choice of whether your two functions are equal, and then branch based on that choice (i.e. return different lists). But think about how that is supposed to work in this case:
Definition func1 (n : nat) := 0.
Definition func2 (n : nat) := n - n.
(* This function can be defined in axiom-free Coq. *)
Definition func3 (n : nat) := if all numbers < n reach 1 in the Collatz sequence within n steps then 0 else 1.
Compute (partten [func1; func2; func3]).
Here, you would basically want Coq to decide whether func1, func2, and func3 always return the same values. While obvious for func1 and func2, the answer is unknown for func3. In general, this is undecidable, as you would have to solve the halting problem. So while Coq allows you to use classical logic in your proofs, it does not allow you to write functions (computing “actual data”) where the outcome of your function depends on a classical case distinction.
Of course, just like classical is an Axiom saying we can use classical logic, we can define a similar axiom saying we can use classical logic and have our computations depend on it. But this is somewhat dubious. The main question is: Why do you want to define your function partten for objects whose equality is not decidable?
@JoJoDeveloping Wouldn’t indeed assuming (or taking as argument, as I do below), that T has decidable equality (strictly?) do the trick? (Strictly in the sense that it is the weakest assumption that does.)
Require Import Coq.Lists.List.
Import ListNotations.
Section prop_partten.
Context {T : Type}.
Hypothesis eq_T : forall (t1 t2 : T),
{t1 = t2} + {t1 <> t2}.
Fixpoint partten (l : list T) : list nat.
Proof.
destruct l as [|h t] eqn:E.
+ exact [].
+ inversion t as [|h' _].
- exact [1].
- destruct (eq_T h h') eqn:E'.
* ...
Thank you very much to explain all these. Now I understand that if the equality of two elements is not decidable, the result of partten is not computable.
Actually I’m trying to define this function to prove some property of certain kinds of list. It seems that if I want my proof works for any type of list, I can’t use such partten function in the proof. Anyway, thank you a lot! 
I’ve tried this out, and this really works. In fact I think the hypothesis you introduce is similar to what @JoJoDeveloping has advised:
However I can’t prove the hypothesis for type like nat -> nat, and I think this is exactly the weakest assumption of the type T that I can define partten function over. Anyway, thank you for your idea!
I hope JoJo or somebody will correct us both. 
In particular, I think I have botched terminology: mine is a sum type, not a disjunction, so that was “computable decidable equality”, not just “decidable equality”, I think. But someone else will have to explain that…
However I can’t prove the hypothesis for type like nat → nat
Sure you can, just beware what is what: your second definition of partten is a generic one, and it is the one you would typically want (IOW, it could stand on its own in a Lists library), though in the form I have written it, i.e. with arguments instead of axioms. To then use it, you rather call it with a T together with a proof that T has (computably?) decidable equality. And that, in case T := nat -> nat, is indeed going to be by some functional extensionality…
Usually your sum type is meant by “decidable equality.” The usual definitions (as found in e.g. stdpp) are
Definition decidable (P : Prop) := sumbool P (not P).
Definition eq_dec (T : Type) := forall (a b : T), decidable (a = b).
Indeed, you can assume eq_dec T and then defining such a function partten makes a lot of sense.
You can also prove eq_dec T for any T by assuming some stronger axioms like “everything is decidable” which is like a “computational” version of excluded middle (with the or replaced by the informative sumbool). Whether such axioms make sense here is up to question, you can often get by without such axioms by proving an existential (i.e you prove exists (l : list T), l has certain properties which only requires the normal law of excluded middle, not the sumbool one).
But without such strong axioms, you won’t be able to prove eq_dec (nat -> nat). In particular, function extensionality is not enough since the codomain is infinite / you would have to test for equality at infinitely many points / you would have to solve the halting problem.
1 Like
Talking about “strong axioms” is a bit misleading here. Indeed, eq_dec (nat -> nat) is a consequence of the limited principle of omniscience, which is one of the mildest axioms out there.
2 Likes