The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Out of curiosity,  Gaëtan, where did you get the name "commutative cut" for this? It's the first time I've heard of it.

Written from mobile. Excuse my limited communication.

On Fri, Mar 22, 2019, 5:28 AM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

The variable x depends on t, so when you match on t if you want to use x
at a type depending on the branch you have to do a commutative cut

Definition liftVal t : tyDenote t -> exp t :=
   match t with
   | Nat => fun x => NatLit x
   | Nat' => fun x => Nat'Lit x
   | Bool => fun x => BoolLit x
   end.

Gaëtan Gilbert

On 22/03/2019 09:17, Christian Kjær Larsen wrote:
> Hi,
>
> I have some GADT for expressions, and I want to lift values into
> expressions like this
>
> Inductive ty : Set :=
> | Nat  : ty
> | Nat' : ty
> | Bool : ty.
>
> Definition tyDenote (t : ty) : Set :=
>    match t with
>    | Nat  => nat
>    | Nat' => nat
>    | Bool => bool
>    end.
>
> Inductive exp : ty -> Set :=
> | NatLit : nat -> exp Nat
> | Nat'Lit : nat -> exp Nat'
> | BoolLit : bool -> exp Bool.
>
> Definition liftVal t (x : tyDenote t) : exp t :=
>    match t in ty return exp t with
>    | Nat => NatLit x
>    | Nat' => Nat'Lit x
>    | Bool => BoolLit x
>    end.
>
> But the last definition will not type check. Do any of you know how to
> write a function like this? One complication is probably that different
> object level types have the same denotation.
>
> Cheers,
> Christian
>