Coq：从上下文中得出论点
Coq: Derive argument from context
(* 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.
很难使用第一种方法，因为维护这样的代码非常困难。当有超过五个不同的函数，每个函数有 4-5 个参数时，写起来真的很痛苦。
第二种情况比较方便。但是我还有很多额外的行带有 "let" 声明：
Let f1 := ...
Let f2 := ...
...
Let fn := ...
有什么办法可以避免这种额外的样板文件吗？理想情况下，我希望 Coq 仅 "guess" 使用上下文中的类型甚至术语名称来更正参数。
如果上下文（即 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.
(* 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.
很难使用第一种方法，因为维护这样的代码非常困难。当有超过五个不同的函数，每个函数有 4-5 个参数时，写起来真的很痛苦。
第二种情况比较方便。但是我还有很多额外的行带有 "let" 声明：
Let f1 := ...
Let f2 := ...
...
Let fn := ...
有什么办法可以避免这种额外的样板文件吗？理想情况下，我希望 Coq 仅 "guess" 使用上下文中的类型甚至术语名称来更正参数。
如果上下文（即 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.