coq - Curry 通用量化函数

Question

我正在尝试编写柯里化(Currying)函数的策略，包括通用量化函数。

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.