3
$\begingroup$

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).

It's straightforward to formalize something resembling second-order arithmetic or something resembling higher-order arithmetic in Coq if there are a fixed number of possible levels.

I'm curious if there's a way to define such a notion, though, for an infinite number of levels.

Require Import BinNums.

Definition col (X : Type) : Type := X -> bool.

(* This is bad because it only goes up to 2 levels *)
Inductive col_hierarchy_bad_1 : Type :=
| catom : N -> col_hierarchy_bad_1
| ccol1 : (col N) -> col_hierarchy_bad_1
| ccol2 : (col (col N)) -> col_hierarchy_bad_1.

(* This attempt doesn't even compile. I'm trying to decorate "col_hierarchy"
   with the kind of thing it contains and then later figure out how to stitch
   the different col_hierarchies together into a single type. *)
(*
Inductive col_hierarchy_bad_2 (contents : Type) : Type :=
| catom : N -> col_hierarchy_bad_2 N
| ccol : forall T : Type, (col_hierarchy_bad_2 T -> col_hierarchy_bad_2 (col T)). 
*)
$\endgroup$
4
  • 6
    $\begingroup$ Slightly off-topic, but except if you are adding a strong variant of the excluded middle axiom, representing predicates on X as functions X -> bool is never going to work. You should use X -> Prop instead. $\endgroup$ Mar 7 at 7:07
  • 1
    $\begingroup$ The coq-definition tag makes very little sense to me. $\endgroup$ Mar 8 at 17:27
  • 1
    $\begingroup$ Gregory, could you please react to Bubbler's answer. Is that what you're looking for? If not, please clarify. $\endgroup$ Mar 8 at 17:28
  • 1
    $\begingroup$ I accepted the answer now (and also upvoted it before). It was exactly what I was looking for. Sorry, I thought that did not require an explicit message. I originally used the tag definition because the question is about how to define a concept expressed informally, rather than how to prove something. I can remove the tag if it doesn't make sense. $\endgroup$ Mar 8 at 18:25

2 Answers 2

7
$\begingroup$

A simple way is to define the type in terms of the Peano natural numbers nat.

Require Import BinNums Arith.

Definition col (X : Type) : Type := X -> bool.

Fixpoint col_repeat (n : nat) (X : Type) : Type :=
match n with
| O => X
| S n => col (col_repeat n X)
end.

Inductive col_hierarchy : Type :=
| ccoln (n : nat) : col_repeat n N -> col_hierarchy.

This way, ccoln 0 corresponds to your catom, ccoln 1 to ccol1, and so on, and ccoln n is defined for every natural number n.

$\endgroup$
1
$\begingroup$

Your definition is awkward because of strict positivity requirements in inductive datatypes.

Your definition of col is really a decidable subset and there exists an alternative strictly positive encoding of subsets in terms of the image of a function.

Inductive hierarchy: nat -> Type :=
| catom: N -> hierarchy 0
| cimage {n} (X: Set): (X -> hierarchy n) -> hierarchy (S n).

The decidable hierarchy consists of

Fixpoint decidable {n} (h: hierarchy) : Type :=
  match h with
  | catom _ => unit
  | cimage X P => (forall y. {exists x. P x = y} + {~exists x. P x = y}) * forall x. decidable (P x)
  end.

A little mucky but I thought it was worth mentioning. The image strictly positive encoding trick is often useful for some constructions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.