Corecursion via destructors?

Using Coq
1

Hi all,

I’m trying to explore corecursive definitions as “pattern matching” on the destructors of the (potentially coinductive) type to define a destructor of the left hand side of the function type, along with recursion in the coinductive case. For example, I have this working for products and sums:

Section sum.
  Variables A B : Type.

  Record sum_elim_cases (source : Type) target :=
    { left_case : A → target
    ; right_case : B → target
    }.
  Arguments left_case {source} {target}.
  Arguments right_case {source} {target}.

  Definition sum_eliminator source := ∀ target, sum_elim_cases source target → (source → target).

  Definition sum_eliminator_sum : sum_eliminator (A + B) :=
    λ _ cases s, match s with
                 | inl a => cases.(left_case) a
                 | inr b => cases.(right_case) b
                 end.

  Definition sum_intro {source} (elim : sum_eliminator source) : source → A + B :=
    elim
      (A + B)%type
      {| left_case := inl
       ; right_case := inr
      |}.

  Definition sum_elim_intro {source} (f : source → A + B) : sum_eliminator source :=
    λ _ cases x, match f x with
                 | inl a => cases.(left_case) a
                 | inr b => cases.(right_case) b
                 end.
End sum.

Section prod.
  Variables A B : Type.

  Inductive prod_elim_cases (source : Type) target :=
  | π₁ : (A → target) → prod_elim_cases source target
  | π₂ : (B → target) → prod_elim_cases source target.

  Arguments π₁ {source} {target}.
  Arguments π₂ {source} {target}.

  Definition prod_eliminator source :=
    ∀ target, prod_elim_cases source target → (source → target).

  Definition prod_eliminator_prod : prod_eliminator (A * B) :=
    λ _ elim p,
    match p with
    | (a, b) =>
      match elim with
      | π₁ f => f a
      | π₂ g => g b
      end
    end.

  Definition prod_intro {source} (elim: prod_eliminator source) : source → A * B :=
    λ s, ((elim A (π₁ (λ a, a)) s), (elim B (π₂ (λ b, b)) s)).

  Definition prod_elim_intro {source} (f : source → A * B) : prod_eliminator source :=
    λ _ elim s,
    match f s with
    | (a, b) =>
      match elim with
      | π₁ f => f a
      | π₂ g => g b
      end
    end.
End prod.

But when I try it for a coinductive case:

CoInductive conat :=
| co0 : conat
| coS : conat → conat.

Record conat_elim_cases source target :=
  { zero_case : unit → target
  ; succ_case : source → target
  }.

Arguments zero_case {source} {target}.
Arguments succ_case {source} {target}.

Definition conat_eliminator source := ∀ target, conat_elim_cases source target → (source → target).

Definition conat_eliminator_conat : conat_eliminator conat :=
  λ _ cases cn,
  match cn with
  | co0 => cases.(zero_case) tt
  | coS cn' => cases.(succ_case) cn'
  end.

Fail Definition conat_intro {source} (elim : conat_eliminator source) : source → conat :=
  cofix conat_intro' (s : source) : conat :=
    elim
      conat
      {| zero_case := λ _, co0
       ; succ_case := λ s', coS (conat_intro' s')
      |} s.

the last definition does indeed fail due to the guardedness check.

I have two questions on this:

  1. Is this definition actually non-productive in some way I’m missing, or is it just that coq’s check is overzealous? Or is it actually productive but there’s no (known?) syntactic check that could accept this without accepting bad definitions?
  2. Is there any existing literature on defining (corecursive) introduction rules this way?
2

I think this is productive, but it’s pretty hard to formalize because it relies on parametricity.

The intuition is that conat_eliminator source is isomorphic to source -> option source and that’s how you can connect your definition to a guarded definition. The isomorphism is nontrivial to prove.

Coq’s syntactic checks for recursion are really limited. A better approach is to track productivity in the type system, and the relevant keyword is Clocked Type Theory.

3

Ah, thank you! This works

Definition conat_intro {source} (elim : conat_eliminator source) : source → conat :=
  cofix conat_intro' (s : source) : conat :=
    match elim
            (unit + source)%type
            {| zero_case := inl; succ_case := inr |}
            s
    with
    | inl _ => co0
    | inr s' => coS (conat_intro' s')
    end.