# How can I get types to compute?

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?

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

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