CODEWITHSUNDEEP
coq
Alex
Alex

Reputation: 1631

apply argument to equal functions in Coq

Suppose I have two functions f and g and I know f = g. Is there a forward reasoning 'function application' tactic that will allow me to add f a = g a to the context for some a in their common domain? In this contrived example, I could use assert (f a = g a) followed by f_equal. But I want to do something like this in more complex situations; e.g.,

Lemma fapp : forall (A B : Type) (P Q : A -> B) (a : A), 
               (fun (a : A) => P a) = (fun (a : A) => Q a) -> 
               P a = Q a.

Upvotes: 0

Views: 2176

Answers (2)

user1494846
user1494846

Reputation: 244

I don't have a lot of experience with Coq or its tactics, but why not just use an auxiliary theorem?

Theorem fapp': forall (t0 t1: Type) (f0 f1: t0 -> t1),
  f0 = f1 -> forall (x0: t0), f0 x0 = f1 x0.
Proof.
intros.
rewrite H.
trivial.
Qed.

Lemma fapp : forall (A B : Type) (P Q : A -> B) (a : A), 
               (fun (a : A) => P a) = (fun (a : A) => Q a) -> 
               P a = Q a.
Proof.
intros.
apply fapp' with (x0 := a) in H.
trivial.
Qed.

Upvotes: 1

nobody
nobody

Reputation: 4264

I think I can't correctly infer the general problem that you have, given your description and example.

If you already know H : f = g, you can use that to rewrite H wherever you want to show something about f and g, or just elim H to rewrite everything at once. You don't need to assert a helper theorem and if you do, you'll obviously need something like assert or pose proof.

If that equality is hidden underneath some eta-expansion, like in your example, remove that layer and then proceed as above. Here are two (out of many) possible ways of doing that:

intros A B P Q a H. assert (P = Q) as H0 by apply H. rewrite H0; reflexivity.

This solves your example proof by asserting the equality, then rewriting. Another possibility is to define eta reduction helpers (haven't found predefined ones) and using these. That will be more verbose, but might work in more complex cases.

If you define

Lemma eta_reduce : forall (A B : Type) (f : A -> B),
    (fun x => f x) = f.
  intros. reflexivity.
Defined.

Tactic Notation "eta" constr(f) "in" ident(H) :=
  pattern (fun x => f x) in H;
  rewrite -> eta_reduce in H.

you can do the following:

intros A B P Q a H. eta P in H. eta Q in H. rewrite H; reflexivity.

(That notation is a bit of a loose cannon and might rewrite in the wrong places. Don't rely on it and in case of anomalies do the pattern and rewrite manually.)

Upvotes: 1

Related Questions