绑定器下的泛化表达式

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 tactic，它用可转换的术语替换了一个术语，并且概括了 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)) *)

绑定器下的泛化表达式

generalizing expressions under binders

coq

coq-tactic

ltac