The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hi Christian,

In your case, you need to pass the argument of "tyDenote t" under the 
match. Intuitively, this is needed in order to make the dependent-match 
perform a kind of "type coercion" on "tyDenote t".

Definition liftVal t:  (tyDenote t) -> exp t :=
  match t in ty return (tyDenote t) -> exp t with
  | Nat => NatLit
  | Nat' => Nat'Lit
  | Bool => BoolLit
  end.

If your are not very familiar with dependent pattern-matching, the more 
easiest way is to build such complex terms, is to use the interactive 
prover. On your example, this gives:

Definition liftVal t (x:tyDenote t): exp t.
  destruct t; simpl in * |- *.
  - apply NatLit; auto.
  - apply Nat'Lit; auto.
  - apply BoolLit; auto.
Defined.

Then, you can "Print liftVal" and copy paste it in your file, if you 
prefer have the underlying term...

Regards,

Sylvain.

Le 22/03/2019 à 09:17, Christian Kjær Larsen a écrit :
> 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.