Coq：从上下文中导出参数

Question

  (* I have a section with many variables and definitions. *)
  Section SectionWithDefs.

    Context {A B C: Type}.

    Variable arg1: A -> B.
    Variable arg2: B -> C.

    (* Functions that uses these variables. *)
    Definition f a := arg2 (arg1 a).  
      ...

  End SectionWithDefs.

  (* Now I want to use some of these functions. *)
  Section AnotherSection.

    Context {A B C: Type}.

    (* Here are the arguments. *)
    Variable arg1: A -> B.
    Variable arg2: B -> C.

    Variable a: A.

    Section CallFunctionWithArgiments.

      (* We can directly pass the arguments to the function...*)
      Eval compute in (f arg1 arg2 a).

    End CallFunctionWithArgiments.

    Section LetBlock.

      (* ... or we can create a sequence of let expression. *)
      Let f := f arg1 arg2.
        ...

      Eval compute in (f a).

    End LetBlock.

  End AnotherSection.

使用第一种方法真的很难，因为维护这样的代码非常困难。当有超过 5 个不同的函数且每个函数有 4-5 个参数时，写作变得非常痛苦。

第二种情况更方便。但是我仍然有很多带有“let”声明的额外行：

   Let f1 := ... 
   Let f2 := ...
      ...
   Let fn := ...

有什么办法可以避免这种额外的样板文件吗？理想情况下，我希望 Coq 在上下文中使用类型甚至术语名称来“猜测”正确的参数。

Answer 1

如果上下文（即arg1、arg2 等的列表）足够简单，您可以使用类型类而不必传递参数。

  (* I have a section with many variables and definitions. *)
  Section SectionWithDefs.

    Context {A B C: Type}.

    Class Arg1 : Type := arg1 : A -> B.
    Context `{IArg1 : Arg1}.

    Class Arg2 : Type := arg2 : B -> C.
    Context `{IArg2 : Arg2}.

    (* Functions that uses these variables. *)
    Definition f a := arg2 (arg1 a).  

    (* ... *)

  End SectionWithDefs.

  (* Now I want to use some of these functions. *)
  Section AnotherSection.

    Context {A B C: Type}.

    (* Here are the arguments. *)
    Context `{MyIArg1 : Arg1 A B}.
    Context `{MyIArg2 : Arg2 B C}.

    Variable a: A.

    Section CallFunctionWithInstances.

      (* The implicit type class arguments [IArg1] and [IArg2] are
         resolved using instances in scope...*)
      Compute (f a).

    End CallFunctionWithInstances.

  End AnotherSection.