バインダーの下で式を一般化する

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) 

および第2のもの：

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

をと一般化すると、A -> A -> Aとなります。ここでの難しさは、私が一般化しようとしています式は、バインダー中であるということである

(fun a b => somefun a b) 

と

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

：これは私の中に式を向けるだろう。私はそれを操作するための戦術またはLTACの表現を見つけることができませんでした。このようなことをどうすればできますか？

Answer 1

この回答には2つのキーがありますchange tactic、コンバーチブル1で1つの用語を置き換え、そしてあなたがg _ _ cしかしfun z => g _ _ zでない対処するようcを一般;この2番目のキーでは、引数に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. 
    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)) *) 

：ここ

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)) *) 

はむしろ poseを使用するよりも、 cbv betaをブロックするために id（恒等関数）を使用して代替バージョンであります