咖喱普遍量化函数

Question

我正在尝试编写一个柯里函数的策略，包括普遍量化的函数。

Require Import Coq.Program.Tactics. 

Definition curry1 := forall A B C, (A /\ B -> C) -> (A -> B -> C). 
Definition curry2 := forall A B, (forall C, A /\ B -> C) -> (forall C, A -> B -> C). 
Definition curry3 := forall A, (forall B C, A /\ B -> C) -> (forall B C, A -> B -> C). 
(* etc. *) 

Ltac curry H := 
    let T := type of H in 
    match T with 
    | _ /\ _ -> _ => 
    replace_hyp H (fun H1 => fun H2 => H (conj H1 H2)) 
    | forall x, ?P x => 
    fail 1 "not implemented" 
    | _ => 
    fail 1 "not a curried function" 
    end. 

Example ex1 : curry1. 
Proof. 
    intros A B C H. 
    curry H. 
    assumption. 
Qed. 

Example ex2 : curry2. 
Proof. 
    intros A B H. 
    Fail curry H. (* Tactic failure: not a curried function. *) 
    Fail replace_hyp H (fun H1 => let H2 := H H1 in ltac:(curry H2)). (* Cannot infer an existential variable of type "Type" in environment: [...] *) 
Abort. 

如何扩展我的curry策略来处理普遍量化的功能？

Answer 1

可以基本模式匹配上像这样所有的变种：

Ltac curry H := 
    match type of H with 
    | _ /\ _ -> _ => 
     replace_hyp H (fun a b => H (conj a b)) 
    | forall C, _ /\ _ -> _ => 
     replace_hyp H (fun C a b => H C (conj a b)) 
    | forall B C, _ /\ _ -> _ => 
     replace_hyp H (fun B C a b => H B C (conj a b)) 
    | forall A B C, _ /\ _ -> _ => 
     replace_hyp H (fun A B C a b => H A B C (conj a b)) 
    end. 

注意C有排序Type，不Prop。如果你愿意在Prop工作，你可以使用setoid_rewrite逻辑等价的策略。例如：

Require Import Coq.Setoids.Setoid. 

Implicit Types C : Prop. 

Definition and_curry_uncurry_iff {A B C} : (A /\ B -> C) <-> (A -> B -> C) := 
    conj (fun H a b => H (conj a b)) (and_ind (P := C)). 

Ltac find_and_curry := 
    match goal with 
    | H : context [_ /\ _ -> _] |- _ => 
     setoid_rewrite and_curry_uncurry_iff in H 
    end. 

Example ex2_prop A B : (forall C, A /\ B -> C) -> (forall C, A -> B -> C). 
Proof. intros H. find_and_curry. assumption. Qed.