Coq: получить аргумент из контекста - PullRequest
Новая
       6

Coq: получить аргумент из контекста

0 голосов
/ 16 ноября 2018 
  (* 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 просто «угадывал» правильные аргументы, используя типы или даже имена терминов в контексте.

1 Ответ

0 голосов
/ 17 ноября 2018

Если контекст (т. Е. Список 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.
...