|
Require Import FunctionalExtensionality.
Ltac make_apply_under_binders_in lem H :=
let tac := make_apply_under_binders_in in
match type of H with
| forall x : ?T, @?P x
=> let ret := constr:(fun x' : T =>
let Hx := H x' in
ltac:(let ret' := tac lem Hx in
exact ret')) in
match eval cbv zeta in ret with
| fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in
constr:(Some P')
end
| _ => let ret := constr:(ltac:(match goal with
| _ => (let H' := fresh in
pose H as H';
apply lem in H';
exact (Some H'))
| _ => exact (@None nat)
end
)) in
let ret' := (eval cbv beta zeta in ret) in
constr:(ret')
| _ => constr:(@None nat)
end.
Ltac apply_under_binders_in lem H :=
let H' := make_apply_under_binders_in lem H in
let H'0 := match H' with Some ?H'0 => constr:(H'0) end in
let H'' := fresh in
pose proof H'0 as H'';
clear H;
rename H'' into H.
Goal forall A B C (f g : forall (x : A) (y : B x), C x y), (forall x y, f x y = g x y) -> True.
Proof.
intros A B C f g H.
let lem := constr:(@functional_extensionality_dep) in
apply_under_binders_in lem H.
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
Abort.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
