Обобщающие выражения под связывателями

Question

Мне нужно обобщить выражение под связующим. Например, в моей цели есть два выражения:

(fun a b => g a b c)

а также

(fun a b => f (g a b c))

И я хочу обобщить g _ _ c часть:

Один из способов сделать это - сначала переписать их в:

(fun a b => (fun x y =>  g x y c) a b)

а второй в:

(fun a b =>
   f (
       (fun x y =>  g x y c) a b
   ))

А потом обобщать (fun x y, g x y c) как somefun с типом A -> A -> A, Это превратит мои выражения в:

(fun a b => somefun a b)

а также

(fun a b => f (somefun a b))

Трудность здесь в том, что выражение, которое я пытаюсь обобщить, находится под переплетом. Я не мог найти ни тактику, ни выражение LTAC, чтобы манипулировать ею. Как я могу сделать что-то подобное?

Answer 1

Есть два ключа к этому ответу: change тактика, которая заменяет один термин на конвертируемый и обобщающий c так что ты имеешь дело не с g _ _ c но fun z => g _ _ z; этот второй ключ позволяет вам иметь дело с g а не с g применяется к своим аргументам. Здесь я использую pose Тактика управления тем, какие функции приложения получают β:

Axiom A : Type.
Axiom f : A -> A.
Axiom g : A -> A -> A -> A.
Goal forall c, (fun a b => g a b c) = (fun a b => f (g a b c)).
Proof.
  intro c.
  pose (fun z x y => g x y z) as g'.
  change g with (fun x y z => g' z x y).
  (*   (fun a b : A => (fun x y z : A => g' z x y) a b c) =
       (fun a b : A => f ((fun x y z : A => g' z x y) a b c)) *)
  cbv beta.
  (* (fun a b : A => g' c a b) = (fun a b : A => f (g' c a b)) *)
  generalize (g' c); intro somefun; clear g'.
  (* (fun a b : A => somefun a b) = (fun a b : A => f (somefun a b)) *)

Вот альтернативная версия, которая использует id (функция идентичности), чтобы заблокировать cbv betaвместо использования pose:

Axiom A : Type.
Axiom f : A -> A.
Axiom g : A -> A -> A -> A.
Goal forall c, (fun a b => g a b c) = (fun a b => f (g a b c)).
Proof.
  intro c.
  change g with (fun a' b' c' => (fun z => id (fun x y => g x y z)) c' a' b').
  (*   (fun a b : A =>
        (fun a' b' c' : A => (fun z : A => id (fun x y : A => g x y z)) c' a' b') a b c) =
       (fun a b : A =>
        f
          ((fun a' b' c' : A => (fun z : A => id (fun x y : A => g x y z)) c' a' b') a
             b c)) *)
  cbv beta.
  (* (fun a b : A => id (fun x y : A => g x y c) a b) =
     (fun a b : A => f (id (fun x y : A => g x y c) a b)) *)
  generalize (id (fun x y : A => g x y c)); intro somefun.
  (* (fun a b : A => somefun a b) = (fun a b : A => f (somefun a b)) *)