I am trying to write a tactic for currying functions, including universally quantified functions.
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.
How can I extend my curry tactic to handle universally quantified functions?
You can basically pattern-match on all the variants like so:
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.
Notice that C has sort Type, not Prop. And if you are willing to work in Prop, you get to use the setoid_rewrite tactic with logical equivalences. For example:
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.