Quelle bug_3286.v Sprache: Coq

Require Import TestSuite.funext.

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.

quality92%

¤ Dauer der Verarbeitung: 0.7 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.