Definition I_am_one : nat := $(let x := constr:(2 - 1) in
                               exact x)$.
Print I_am_one.

Definition I_am_exactly_one : nat := $(let x := constr:(2 - 1) in
                                       let y := (eval compute in x) in
                                       exact y)$.
Print I_am_exactly_one.

Definition I_am_exactly_two : nat := S $(let x := constr:(2 - 1) in
                                         let y := (eval compute in x) in
                                         exact y)$.
Print I_am_exactly_two.

Ltac ret_and_left f :=
  let tac := ret_and_left in
  let T := type of f in
  match eval hnf in T with
    | ?a ∧ ?b ⇒ exact (proj1 f)
    | ?T' → _ ⇒
      let ret := constr:(fun x' : T' ⇒ let fx := f x' in
                                        $(tac fx)$) in
      let ret' := (eval cbv zeta in ret) in
      exact ret'
  end.

Goal ∀ A B : Prop, (A → A → A → A ∧ B) → True.
  intros A B H.
  pose $(ret_and_left H)$.

Admitted.

Ltac do_under_binders tac term := constr:(fun y ⇒ $(let z := tac (term y) in exact z)$).

Ltac hnf_under_binders term := do_under_binders ltac:(fun x ⇒ eval hnf in x) term.
Ltac hnf_under_all_binders term :=
  match term with
    | _ ⇒ do_under_binders hnf_under_all_binders term
    | _ ⇒ eval hnf in term
  end.

Definition unfold_me := 1.
Definition unfold_me_too := unfold_me.

Goal True.
  let x := hnf_under_binders (fun x : Type ⇒ unfold_me_too) in
  pose x.
  let x := hnf_under_binders (fun x y z w : Type ⇒ unfold_me_too) in
  pose x.
  let x := hnf_under_all_binders (fun x y z w : Type ⇒ unfold_me_too) in
  pose x.
Abort.

Class hnf_under_binders_helper {T P} (y : T) (z : P y)
  := make_hnf_under_binders_helper : P y.
Arguments hnf_under_binders_helper {T P} y z / .
Hint Extern 0 (hnf_under_binders_helper ?y ?z)
⇒ let z' := (eval hnf in z) in exact z' : typeclass_instances.

Ltac hnf_under_binders_84 x :=
  let x' := constr:(fun y ⇒ _ : hnf_under_binders_helper y (x y)) in
  let x'' := (eval unfold hnf_under_binders_helper in x') in
  constr:(x'').

Goal True.
  let x := hnf_under_binders_84 (fun x : Type ⇒ unfold_me_too) in
  pose x.
Abort.

Ltac make_apply_under_binders_in lem H :=
  let tac := make_apply_under_binders_in in
  match type of H with
    | ∀ x : ?T, @?P x
      ⇒ let ret := constr:(fun x' : T ⇒
                              let Hx := H x' in
                              $(let ret' := tac lem Hx in
                                exact ret')$) in
         let ret' := (eval cbv zeta in ret) in
         constr:(ret')
    | _ ⇒ let ret := constr:($(let H' := fresh in
                                pose H as H';
                                apply lem in H';
                                exact H')$) in
           let ret' := (eval cbv beta zeta in ret) in
           constr:(ret')
  end.

Tactic Notation "binder_apply" open_constr(lem) "in" hyp(H) :=
  let H' := make_apply_under_binders_in lem H in
  let H'' := fresh in
  pose proof H' as H'';
    clear H;
    rename H'' into H.

Require Import FunctionalExtensionality.

Goal ∀ A B P (f g : ∀ (x : A) (y : B x), P x y), (∀ x y, f x y = g x y) → f = g.
Proof.
  intros A B P f g H.
  eapply @functional_extensionality_dep in H.
  Undo.
  binder_apply @functional_extensionality_dep in H.
  binder_apply @functional_extensionality_dep in H.
  exact H.
Defined.

Class make_apply_under_binders_in_helper {T} (lem : T) {T'} (H : T') {T''} := do_make_apply_under_binders_in_helper : T''.

Class make_apply_under_binders_in_helper_helper {T} (H : T) {T'} (lem : T') {T''} := do_make_apply_under_binders_in_helper_helper : T''.

Hint Extern 0 (make_apply_under_binders_in_helper_helper ?H ?lem)
⇒ let H' := fresh in
   pose H as H';
     apply lem in H';
     exact H'
           : typeclass_instances.

Ltac make_apply_under_binders_in_84 lem H :=
  match type of H with
    | ∀ x : ?T, @?P x
      ⇒ let ret := constr:(fun x' : T ⇒
                              let Hx := H x' in
                              _ : make_apply_under_binders_in_helper lem Hx) in
         let ret' := (eval cbv zeta beta delta [do_make_apply_under_binders_in_helper make_apply_under_binders_in_helper] in ret) in
         let retT := type of ret' in
         let retT' := (eval cbv zeta beta delta [do_make_apply_under_binders_in_helper make_apply_under_binders_in_helper] in retT) in
         constr:(ret' : retT')
    | _ ⇒ let ret := constr:(_ : make_apply_under_binders_in_helper_helper H lem) in
           let ret' := (eval cbv beta zeta delta [make_apply_under_binders_in_helper_helper do_make_apply_under_binders_in_helper_helper] in ret) in
           let retT := type of ret' in
           let retT' := (eval cbv beta zeta delta [make_apply_under_binders_in_helper_helper do_make_apply_under_binders_in_helper_helper] in retT) in
           constr:(ret' : retT')
  end.

Hint Extern 0 (make_apply_under_binders_in_helper ?lem ?H) ⇒
let ret := make_apply_under_binders_in_84 lem H
in exact ret
   : typeclass_instances.

Ltac apply_under_binders_in_84 lem H :=
  let H' := make_apply_under_binders_in lem H in
  let H'' := fresh in
  pose proof H' as H'';
    clear H;
    rename H'' into H.

Goal ∀ A B P (f g : ∀ (x : A) (y : B x), P x y), (∀ x y, f x y = g x y) → f = g.
Proof.
  intros A B P f g H.
  apply_under_binders_in_84 @functional_extensionality_dep H.
  apply_under_binders_in_84 @functional_extensionality_dep H.
  exact H.
Defined.

Parameters T₁ T₂ T₃ : Type.
Parameter F : T₁ → T₃.
Parameter G : T₂ → T₃.
Parameters (t₁ : T₁) (t₂ : T₂).

Class MyNotation {A R} (a : A) (r : R) := {}.
Definition mynotation A R a r `{@MyNotation A R a r} := r.
Instance MyF x : MyNotation x (F x) | 10.
Instance MyG x : MyNotation x (G x) | 100.

Notation "% x"
  := ($(let ret := constr:(@mynotation _ _ x _ _) in
        let ret' := (eval cbv beta delta [mynotation] in ret) in
        exact ret')$)
       (at level 40, only parsing).
Check (% t₁).

Check (% t₂).

Check (fun x ⇒ % x).

Fail Check (% _).

Fail Check (% 1).

Ltac pick_percent x :=
  let T := type of x in
  let T1 := constr:(T₁) in
  let T2 := constr:(T₂) in
  first [ unify T T₁; exact (F x)
        | unify T T₂; exact (G x)
        | fail 1 "The typeof" x ":" T "is neither" T1 "nor" T2 ].

Notation "%% x"
  := ($(pick_percent x)$)
       (at level 40, only parsing).
Goal True.
  Check (%% t₁).

  Check (%% t₂).

  Check (fun x ⇒ %% x).

  Fail Check (%% _).

  Fail pose (%% 1).

Abort.

Parameter Compose11 : T₁ → T₁ → T₁.
Parameter Compose12 : T₁ → T₂ → T₁.
Parameter Compose21 : T₂ → T₁ → T₁.
Parameter Compose22 : T₂ → T₂ → T₂.

Class ComposeTo {A B C} (a : A) (b : B) (c : C) := {}.
Definition composition A B C a b c `{@ComposeTo A B C a b c} := c.
Instance ComposeTo11 x y : ComposeTo x y (Compose11 x y) | 10.
Instance ComposeTo12 x y : ComposeTo x y (Compose12 x y) | 100.
Instance ComposeTo21 x y : ComposeTo x y (Compose21 x y) | 100.
Instance ComposeTo22 x y : ComposeTo x y (Compose22 x y) | 1000.

Reserved Infix "∘" (at level 40, left associativity).

Notation "x ∘ y"
  := ($(let ret := constr:(@composition _ _ _ x y _ _) in
        let ret' := (eval cbv beta delta [composition] in ret) in
        exact ret')$)
       (only parsing).

Check (t₁ ∘ t₁).

Check (t₁ ∘ t₂).

Check (t₂ ∘ t₁).

Check (t₂ ∘ t₂).

Ltac head x :=
  match x with
    | ?f ?a ⇒ let log := constr:($(idtac x; exact I)$) in head f
    | _ ⇒ x
  end.

Goal True.
  let k := head (1 + 1 + 1 + 1) in
  pose k. Abort.

Set Universe Polymorphism.
Set Printing Universes.
Inductive eq {A} (x : A) : A → Set := eq_refl : eq x x.
Notation "x = y :> A" := (@eq A x y) : type_scope.
Notation "x = y" := (x = y :> _) : type_scope.
Definition Lift
: $(let U1 := constr:(Type) in
    let U0 := constr:(Type : U1) in
    let U0' := (eval simpl in U0) in
    exact (U0' → U1))$
  := fun A ⇒ A.
Check Lift.

Definition lift_eq {T x y} (p : x = y :> T) : x = y :> Lift T
  := match p with eq_refl _ ⇒ eq_refl _ end.

Definition NaiveFunext := ∀ A P (f g : ∀ x : A, P x),
                            (∀ x, f x = g x :> P x) → f = g.

Definition funext_downward_closed
: NaiveFunext → NaiveFunext
  := fun fs A P f g H
     ⇒ lift_eq (fs (Lift A) (fun x ⇒ Lift (P x))
                    f g
                    (fun x ⇒ lift_eq (H x))).

Goal ∀ x y : NaiveFunext, x = y.
Proof.
  intros x y; hnf in x, y.
  Fail apply x.

  admit.
Abort.

Goal ∀ x y : NaiveFunext, funext_downward_closed x = funext_downward_closed y.
Proof.
  intros x y; hnf in x, y.
  apply x.

  admit.
Abort.