Semideciders

Semideciders.v

CoInductive Partial {A : Type} : Type :=
 | Now : A -> Partial
 | Later : Partial -> Partial.

Arguments Partial : clear implicits.

(** We can use this to loop. *)
CoFixpoint loop {A : Type} := @Later A loop.

Definition unfold_Partial {A : Type} : forall (px : Partial A),
  px = match px with
      | Now x => Now x
      | Later px' => Later px'
      end.
Proof. destruct px; reflexivity. Qed.


(** Run a partial computation for n steps, returning the value if
    we got a value in that many steps or fewer. *)
Fixpoint runPartial {A : Type} (px : Partial A)
  (n : nat) : option A := match px with
  | Now x => Some x
  | Later px' => match n with
    | 0 => None
    | S n' => runPartial px n'
    end 
  end.
  
Inductive PEval {A} {a : A} : Partial A -> Prop :=
  | PEvalNow : PEval (Now a)
  | PEValLater : forall e', PEval e' -> PEval (Later e').

Arguments PEval {A} a e : clear implicits.

Record SemiDec {P : Type} :=
  { decide : Partial P
  ; decide_ok : P -> exists p, PEval p decide }.