Stream: Coq users

Topic: Having implicit arguments


view this post on Zulip 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?

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC