Generalizing expressions under binders

Link:: https://stackoverflow.com/q/46458710

Display all goals and responses

Question

I need to generalize expression under the binder. For example, I have in my goal two expressions:

(fun a b => g a b c)

and

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

And I want to generalize g _ _ c part:

One way to do is to rewrite them first into:

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

and the second into:

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

And then, to generalize (fun x y, g x y c) as somefun with type A -> A -> A. This will turn my expressions into:

(fun a b => somefun a b)

and

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

The difficulty here is that the expression I am trying to generalize is under the binder. I could not find either a tactic or LTAC expression to manipulate it. How can I do something like this?

Answer

There are two keys to this answer: the change tactic, which replaces one term with a convertible one, and generalizing c so that you deal not with g _ _ c but fun z => g _ _ z; this second key allows you to deal with g rather than with g applied to its arguments. Here, I use the pose tactic to control what function applications get β reduced:

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)).forall c : A,
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
Proof.forall c : A,
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
  intro c.c: A
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c)) pose (fun z x y => g x y z) as g'.c: A
g':= fun z x y : A => g x y z: A -> A -> A -> A
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
  change g with (fun x y z => g' z x y).c: A
g':= fun z x y : A => g x y z: A -> A -> A -> A
(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.c: A
g':= fun z x y : A => g x y z: A -> A -> A -> A
(fun a b : A => g' c a b) =
(fun a b : A => f (g' c a b))
  generalize (g' c).c: A
g':= fun z x y : A => g x y z: A -> A -> A -> A
forall a : A -> A -> A,
(fun a0 b : A => a a0 b) =
(fun a0 b : A => f (a a0 b)) intro somefun.c: A
g':= fun z x y : A => g x y z: A -> A -> A -> A
somefun: A -> A -> A
(fun a b : A => somefun a b) =
(fun a b : A => f (somefun a b)) clear g'.c: A
somefun: A -> A -> A
(fun a b : A => somefun a b) =
(fun a b : A => f (somefun a b))

Here is an alternate version that uses id (the identity function) to block cbv beta, rather than using 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)).forall c : A,
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
Proof.forall c : A,
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
  intro c.c: A
(fun a b : A => g a b c) =
(fun a b : A => f (g a b c))
  change g with (fun a' b' c' => (fun z => id (fun x y => g x y z)) c' a' b').c: A
(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.c: A
(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)).c: A
forall a : A -> A -> A,
(fun a0 b : A => a a0 b) =
(fun a0 b : A => f (a a0 b)) intro somefun.c: A
somefun: A -> A -> A
(fun a b : A => somefun a b) =
(fun a b : A => f (somefun a b))