## Stream: Coq users

### Topic: Having implicit arguments

#### Julin S (Apr 21 2022 at 09:11):

I had a few types and definitions like:

``````Inductive type : Set :=
| Nat.

Definition typeDenote (t:type) : Set :=
match t with
| Nat => nat
end.

Inductive binop : type -> type -> type -> Set :=
| Plus : binop Nat Nat Nat
| Fn : forall (t1 t2 t3:type),
((typeDenote t1) -> (typeDenote t2) -> (typeDenote t3))
-> binop t1 t2 t3.
Arguments Fn {t1 t2 t3}.

Definition binopDenote {t1 t2 t3:type} (b:binop t1 t2 t3)
: (typeDenote t1) -> (typeDenote t2) -> (typeDenote t3) :=
match b with
| Plus => plus
| Fn f => f
end.
``````

This sort of works.

``````Check @Fn Nat Nat Nat (fun (x y:nat)=>x).
(*
Fn (fun x _ : nat => x)
: binop Nat Nat Nat
*)

Compute (binopDenote (@Fn Nat Nat Nat (fun (x y:nat)=>x))) 3 2.
(*
= 3
: typeDenote Nat
*)
``````

But could there be a way to have the `Nat Nat Nat` passed to `Fn` as implicit arguments?

So that I can do:

``````Compute (binopDenote (Fn (fun (x y:nat)=>x))) 3 2.
``````

The `Nat Nat Nat` can be inferred from the type of the function passed as argument to `Fn`, right? Is it not so?

#### Janno (Apr 21 2022 at 09:44):

You can use canonical structures but my approach seems awkward and relies on equality proofs and explicit rewriting. Somebody else can probably come up with a more reasonable approach.

``````Structure type' :=
{ #[canonical=no] type'_type :> type;
typeDenote' : Set;
#[canonical=no] typeDenote'_ok : typeDenote type'_type = typeDenote';
}.
(* [eq_refl] must be transparent here. *)
Canonical Structure type'_nat := {| type'_type := Nat; typeDenote' := nat; typeDenote'_ok := eq_refl |}.

Definition Fn' {t1 t2 t3 : type'} : (typeDenote' t1 -> typeDenote' t2 -> typeDenote' t3) -> binop t1 t2 t3 :=
match typeDenote'_ok t1 in _ = T1, typeDenote'_ok t2 in _ = T2, typeDenote'_ok t3 in _ = T3 return
(T1 -> T2 -> T3) -> _
with
| eq_refl, eq_refl, eq_refl => Fn
end.

Check Fn' (fun (x y:nat)=>x).
Compute (binopDenote (Fn' (fun (x y:nat)=>x))) 3 2.
``````

Last updated: Sep 30 2023 at 06:01 UTC