Having implicit arguments · Coq users

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.

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?

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.

Stream: Coq users

Topic: Having implicit arguments

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

Janno (Apr 21 2022 at 09:44):