# How can I get types to compute?

**URL:** <https://discourse.rocq-prover.org/t/how-can-i-get-types-to-compute/308>\
**Category:** Using Rocq\
**Created:** [May 30, 2019, 9:24pm UTC](https://discourse.rocq-prover.org/t/how-can-i-get-types-to-compute/308 "2019-05-30T21:24:04Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [May 30, 2019, 9:24pm UTC](https://discourse.rocq-prover.org/t/how-can-i-get-types-to-compute/308/1 "2019-05-30T21:24:05Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [May 30, 2019, 9:53pm UTC](https://discourse.rocq-prover.org/t/how-can-i-get-types-to-compute/308/2 "2019-05-30T21:53:31Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [May 30, 2019, 10:05pm UTC](https://discourse.rocq-prover.org/t/how-can-i-get-types-to-compute/308/3 "2019-05-30T22:05:24Z")

</div>

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