The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

(* I apologize if I am somwhat repeating myself, but I would like to
   ask advice on how to best do a certain kind of rewriting that involves
   matching lambda abstractions (so my expectations are not high).
   Suppose we assume extensionality: *)

Axiom extensionality: forall (A B : Set), forall (f g : A -> B),
   (forall x : A, f x = g x) -> f = g.

(* We would like to rewrite using the following eta_rule. *)

Lemma eta_rule (A B : Set) (f : A -> B): (fun x => f x) = f.
Proof.
  auto using extensionality.
Qed.

Hint Rewrite eta_rule : extrules.

(* However, it's not clear to me how to use eta_rule for rewriting. *)

Lemma test1 (A B C : Set) (g : (A -> B) -> C) (f : A -> B): g (fun x
=> f x) = g f.
Proof.
  intros.
  (* Attempt 1: rewrite eta_rule. *)
  (* Attempt 1 results in:
     Error: Abstracting over the term "fun x : A => f x" leads to a term
     "fun y : A -> ?17982 => g y = g f" which is ill-typed. *)
  (* Attempt 2 does nothing: *)
  autorewrite with extrules.
  (* But we can tell Coq what we want using patterns. *)
  pattern (fun x : A => f x).
  rewrite eta_rule.
  reflexivity.
Qed.

(* What would be a good way to write a tactic that does the above for me?
   It should automatically find a subterm on which the eta rule is
applicable. *)

(* A related question is how to rewrite "f (g x)" to "(comp f g) x" where 
"comp"
   is function composition: *)

Definition comp {A B C : Set} (f : B -> C) (g : A -> B) (x : A) := f (g x).

Lemma comp_rule (A B C : Set) (f : B -> C) (g : A -> B) (x : A) :
  f (g x) = (comp f g) x.
Proof.
  auto.
Qed.

Lemma test2 (A B C : Set) (f : B -> C) (g : A -> B) (x : A) :
  f (g x) = (comp f g) x.
Proof.
  intros.
  (* Attempt 1 : rewrite comp_rule. *)
  (* Attempt 1 gives:
     Error: Abstracting over the term "f (g x) = comp f g x" leads to a term
     "fun y : ?18079 => y" which is ill-typed. *)
  (* It works if I help Coq with pattern: *)
  pattern (f (g x)).
  rewrite comp_rule.
  auto.
Qed.

(* Actually, what does "ill-typed"  the error message mean in this case?

   With kind regards,

   Andrej
*)