Formalizing "finite or infinite" in Coq

Question

In Coq, I am trying to formalize the notion of a finite or infinite sequence, e.g. of natural numbers: call it a run, and call pos a finite run.

I think I cannot use plain stdlib Streams since I have a possible base case: the first consequence, compared to Stream, is that my run_hd, run_tl, etc., up to run_nth must return options since I can have empty runs, but I guess that is not a problem.

The actual problem is that eventually I do not know how to define a usable predicate and/or computable function to determine/state/distinguish between finite and infinite runs.

Here is some minimal code that I hope is representative enough, where I am trying to have structural sub-typing, but I just cannot get to the bottom of it:

CoInductive run : Set :=
  | RunO : run  (* base for finite runs *)
  | RunS : nat -> run -> run.

Inductive pos : Set :=  (* structurally a finite run *)
  | PosO : pos
  | PosS : nat -> pos -> pos.

Definition IsFinRun (r : run) : Prop.
  Admitted.  (* HOW? *)

Coercion pos_to_run (p : pos) : run.
  Admitted.  (* easy *)

Coercion run_to_pos (r : run) : IsFinRun r -> pos.
  Abort.     (* HOW? *)

For example, among many variations, I have tried:

Definition IsFinRun (r : run) : Prop :=
  exists n : nat, forall m : nat,
    m <= n <-> run_nth m r <> None.

Coercion run_to_pos (r : run) :
  IsFinRun r -> pos.
Proof.  (* in proof mode to explore it *)
  unfold IsFinRun.
  intros H.
  destruct H.  (* ERROR:
    Case analysis on sort Set is not allowed
    for inductive definition ex. *)

(The same error, just on sort Type, happens if I replace Set with Type everywhere. In fact, I do not understand why that error at all, given n is a nat.)

(I have tried to keep the whole thing as brief as possible, but I can post more/full code if necessary, just please let me know.)

What am I missing? In particular, how could I fix/complete the code up to run_to_pos? Thanks in advance for any help or insight.

Answer 1

Since the error you encountered is that you can't deconstruct a proof term whose type's type is Prop to construct the value whose type's type is Set, one ad hoc workaround is to use an inductive Prop with one constructor (which is the special case that can be deconstructed in Set or Type). You can define finiteness of a sequence as a "Prop with one constructor" IsFinRun as follows:

CoInductive run : Set :=
  | RunO : run  (* base for finite runs *)
  | RunS : nat -> run -> run.

Inductive pos : Set :=  (* structurally a finite run *)
  | PosO : pos
  | PosS : nat -> pos -> pos.

Definition tail_run (r : run) : option run :=
  match r with
  | RunO => None
  | RunS _ t => Some t
  end.

Inductive IsFinRun (r : run) : Prop :=
| isfinrun : (forall t, tail_run r = Some t -> IsFinRun t) -> IsFinRun r.

Fixpoint run_to_pos (r : run) (i : IsFinRun r) {struct i} : pos :=
  match r return IsFinRun r -> pos with
  | RunO => fun _ => PosO
  | RunS h t => fun i => PosS h (match i with isfinrun _ j => run_to_pos t (j _ eq_refl) end)
  end i.

Answer 2

This is my second attempt to solve the problem, it is completely different from the first.

Would it be fix the problem to pass in an upper bound of the length and a proof that that length is correct?

CoInductive run : Set :=
  | RunO : run  (* base for finite runs *)
  | RunS : nat -> run -> run.

Inductive pos : Set :=  (* structurally a finite run *)
  | PosO : pos
  | PosS : nat -> pos -> pos.

Fixpoint pos_to_run (p : pos) : run :=
  match p with
  | PosO => RunO
  | PosS x xs => RunS x (pos_to_run xs)
  end
.

Fixpoint run_to_pos_option (n : nat) (r : run) : option pos :=
  match n, r with
  | _, RunO => Some PosO
  | 0, _ => None
  | S n', RunS x xs =>
      match run_to_pos_option n' xs with
      | None => None
      | Some w => Some (PosS x w)
      end
  end
.

Definition IsFinRun (n : nat) (r : run) : Prop :=
  run_to_pos_ok n r <> None.

Definition safe_get (t : Type) (x : option t) (witness : x <> None) : t.
  destruct x.
  auto.
  assert ((None : option t) = None) by auto.
  intuition.
Defined.

Definition run_to_pos (n : nat) (r : run) (witness : IsFinRun n r) : pos :=
  let result_option := run_to_pos_option n r in
  safe_get pos result_option witness
.
```

Answer 3

Another way to approach the problem is to characterize isFinRun inductivelly and to define run_to_pos by structural induction on the proof of isFinRun. Notice that isFinRun r is used to justify termination of the Fixpoint but not to drive the computation. The computation is driven by the structure of r.

This is a good example for the application of the Braga method. The slogan would be: use a specific Prop bounded fuel instead of Type bounded fuel in nat .

CoInductive run : Set :=
  | RunO : run  (* base for finite runs *)
  | RunS : nat -> run -> run.

Inductive pos : Set :=  (* structurally a finite run *)
  | PosO : pos
  | PosS : nat -> pos -> pos.

Fixpoint pos_to_run p :=
  match p with
  | PosO     => RunO
  | PosS n p => RunS n (pos_to_run p)
  end.

Inductive isFinRun : run -> Prop :=
  | iFRO :     isFinRun RunO
  | iFRS n r : isFinRun r 
            -> isFinRun (RunS n r).

Definition is_RunS r :=
  match r with
  | RunO     => False
  | RunS _ _ => True
  end.

(* partial inverse of RunS *)
Definition RunS_inv r : is_RunS r -> run :=
  match r with
  | RunO     => fun C => match C with end
  | RunS _ s => fun _ => s
  end.

(* We get the exact sub-term "s" of "RunS n s" *) 
Goal forall n s, RunS_inv (RunS n s) I = s.
Proof. reflexivity. Qed.

(* partial inverse of isFinRun (RunS _ _), BEWARE of structural decrease *)
Definition isFinRun_inv {r} (fr : isFinRun r) : forall hr : is_RunS r, isFinRun (RunS_inv r hr) :=
  match fr with
  | iFRO       => fun C => match C with end
  | iFRS _ _ h => fun _ => h
  end.

(* Inversion of isFinRun (RunS _ _) *)
Definition isFinRunS_inv {n r} (fr : isFinRun (RunS n r)) : isFinRun r :=
  isFinRun_inv fr I.

(* We get the exact sub-proof "fr" for "iFRS n r fr" *) 
Goal forall n r fr, isFinRunS_inv (iFRS n r fr) = fr.
Proof. reflexivity. Qed. 

Fixpoint run_to_pos {r} (hr : isFinRun r) { struct hr } : { p | pos_to_run p = r } :=
  match r return isFinRun r -> _ with
  | RunO     => fun _  => exist _ PosO eq_refl
  | RunS n r => fun hr => let (p,hp) := run_to_pos (isFinRunS_inv hr) in 
                          exist _ (PosS n p) match hp with eq_refl => eq_refl end
  end hr.

Answer 4

The problem

Informally, we want a type of "finite or infinite sequences", henceforth "runs", with the following form:

• The finite runs:

[]
[1]
[1,2]
[1,2,...,n]

and so on for all n.

• The infinite runs:

[1,2,...,n,---]

for all n, for all possible infinite tails,
where every finite initial segment is a finite run.

A solution

(I have changed few names re the initial code to reflect a different interpretation of the terms.)

Here is some code that seems to do the trick, with the merits, I'd propose, that 1) it quite directly reflects the form of the requirement (the informal construction), and 2) it is very simple and effective to use down the line.

Essentially, finRun as a sigma-type instead of a Prop, and leveraging pos_to_run: then, from an element of finRun r, we can directly extract a (the) p corresponding to r, where p is an element of a plain inductive type, so easy to work with.

A crucial point is that we interpret RunE (and PosE) as the bottom of a finite sequence, while the head in RunN (and PosN) is the initial element of the (possibly infinite, for RunN) sequence.

That entails that the natural way to "progress" such sequences (construct a "next" element) is with append, not with cons.

(** A [run] is a possibly infinite sequence. *)

CoInductive run : Set :=
  | RunE : run                 (* bottom *)
  | RunN : nat -> run -> run.  (* initial+rest *)

(** A [pos] structurally is a finite [run]. *)

Inductive pos : Set :=
  | PosE : pos                 (* bottom *)
  | PosN : nat -> pos -> pos.  (* initial+rest *)

(** Conversions to [run] from finite. *)

Definition nat_to_pos (n : nat) : pos :=
  PosN n PosE.

Fixpoint pos_to_run (p : pos) : run :=
  match p with
  | PosE      => RunE
  | PosN n p' => RunN n (pos_to_run p')
  end.

(** Conversions from [run] to finite. *)

Definition finRun (r : run) : Set :=
  {p : pos | r = pos_to_run p}.

Definition run_to_pos r : finRun r -> pos :=
  fun h => let (p, _) := h in p.

(I am not an expert, and I am sure my presentation is at least clumsy: suggestions and objections, on my analysis as well as the code, are very welcome.)

[*] This solution is based on (my understanding of) an initial suggestion by Naïm Favier given in a comment to the question.