How can I get types to compute?

Using Coq
1

Hey! So I started to learn some Coq today (I’ve done some Agda). I’m doing stuff with session types, and I have the following:

Require Import Unicode.Utf8.

Inductive type (A : Type) : Set :=
| End : type A
| Send : type A → type A
| Receive : type A → type A
| Branch : list (type A) → type A
| Select : nat → type A.

Fixpoint dual {A} (t₁ : type A) (t₂ : type A) : Prop :=
  match (t₁, t₂) with
  | (End _, End _) => True
  | (Send _ t₁', Receive _ t₂') => dual t₁' t₂'
  | (Receive _ t₁', Send _ t₂') => dual t₁' t₂'
  | (Branch _ ts, Select _ n) => True
  | (Select _ n, Branch _ ts) => True
  | _ => False
  end.

Module Type Basis.
  Parameter A : Type.
  Parameter var : type A → Type.
End Basis.

Module Process (B : Basis).
  Import B.
  Inductive Process : type A → Set := 
  | P0 : Process (End A)
  | PNew : ∀ {t}, Process t → Process t
  | PInput : ∀ {t : type A},  Process t → Process (Send A t)
  | POutput : ∀ {t}, Process t → Process (Receive A t)
  (* branch needs an heterogenous list of types *)
  | PComp : ∀ {t₁ t₂}, Process t₁ → Process t₂ → dual t₁ t₂ → Process (End _)
  .

  Theorem meh : dual (Send A (End A)) (Receive A (End A)).
    simpl. trivial. Qed.
  Check PComp (PInput P0) (POutput P0) True.
End Process.

While the theorem holds, the Check command is unable to see that PInput P0 and POutput P0 have types that are dual. How should I get the computation to “advance” so that Coq sees this?

2

The unique inhabitant of the type True (which dual ... computes to) is called I: Check PComp (PInput P0) (POutput P0) I. works fine.

3

Oh my I’m stupid, I tried tt (for unit), didn’t think of actually checking what the constructor for True was, thank you!