FunctionalExtensionality.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic extensionality to apply the axiom of extensionality to an equality goal.

The converse of functional extensionality.

Lemma equal_f : forall {A B : Type} {f g : A -> B},
  f = g -> forall x, f x = g x.forall (A B : Type) (f g : A -> B),
f = g -> forall x : A, f x = g x
Proof.forall (A B : Type) (f g : A -> B),
f = g -> forall x : A, f x = g x
  intros.A, B:Type
f, g:A -> B
H:f = g
x:A
f x = g x
  rewrite H.A, B:Type
f, g:A -> B
H:f = g
x:A
g x = g x
  auto.
Qed.

Lemma equal_f_dep : forall {A B} {f g : forall (x : A), B x},
  f = g -> forall x, f x = g x.forall (A : Type) (B : A -> Type)
  (f g : forall x : A, B x),
f = g -> forall x : A, f x = g x
Proof.forall (A : Type) (B : A -> Type)
  (f g : forall x : A, B x),
f = g -> forall x : A, f x = g x
intros A B f g <- H; reflexivity.
Qed.

Statements of functional extensionality for simple and dependent functions.

Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

Lemma functional_extensionality {A B} (f g : A -> B) :
  (forall x, f x = g x) -> f = g.A, B:Type
f, g:A -> B
(forall x : A, f x = g x) -> f = g
Proof.A, B:Type
f, g:A -> B
(forall x : A, f x = g x) -> f = g
  intros ; eauto using @functional_extensionality_dep.
Qed.

Extensionality of ∀s follows from functional extensionality.

Lemma forall_extensionality {A} {B C : A -> Type} (H : forall x : A, B x = C x)
: (forall x, B x) = (forall x, C x).A:Type
B, C:A -> Type
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
Proof.A:Type
B, C:A -> Type
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
  apply functional_extensionality in H.A:Type
B, C:A -> Type
H:B = C
(forall x : A, B x) = (forall x : A, C x) destruct H.A:Type
B:A -> Type
(forall x : A, B x) = (forall x : A, B x) reflexivity.
Defined.

Lemma forall_extensionalityP {A} {B C : A -> Prop} (H : forall x : A, B x = C x)
: (forall x, B x) = (forall x, C x).A:Type
B, C:A -> Prop
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
Proof.A:Type
B, C:A -> Prop
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
  apply functional_extensionality in H.A:Type
B, C:A -> Prop
H:B = C
(forall x : A, B x) = (forall x : A, C x) destruct H.A:Type
B:A -> Prop
(forall x : A, B x) = (forall x : A, B x) reflexivity.
Defined.

Lemma forall_extensionalityS {A} {B C : A -> Set} (H : forall x : A, B x = C x)
: (forall x, B x) = (forall x, C x).A:Type
B, C:A -> Set
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
Proof.A:Type
B, C:A -> Set
H:forall x : A, B x = C x
(forall x : A, B x) = (forall x : A, C x)
  apply functional_extensionality in H.A:Type
B, C:A -> Set
H:B = C
(forall x : A, B x) = (forall x : A, C x) destruct H.A:Type
B:A -> Set
(forall x : A, B x) = (forall x : A, B x) reflexivity.
Defined.

A version of functional_extensionality_dep which is provably equal to eq_refl on fun _ ⇒ eq_refl

Definition functional_extensionality_dep_good
           {A} {B : A -> Type}
           (f g : forall x : A, B x)
           (H : forall x, f x = g x)
  : f = g
  := eq_trans (eq_sym (functional_extensionality_dep f f (fun _ => eq_refl)))
              (functional_extensionality_dep f g H).

Lemma functional_extensionality_dep_good_refl {A B} f
  : @functional_extensionality_dep_good A B f f (fun _ => eq_refl) = eq_refl.A:Type
B:A -> Type
f:forall x : A, B x
functional_extensionality_dep_good f f
  (fun x : A => eq_refl) = eq_refl
Proof.A:Type
B:A -> Type
f:forall x : A, B x
functional_extensionality_dep_good f f
  (fun x : A => eq_refl) = eq_refl
  unfold functional_extensionality_dep_good; edestruct functional_extensionality_dep; reflexivity.
Defined.

Opaque functional_extensionality_dep_good.

Lemma forall_sig_eq_rect
      {A B} (f : forall a : A, B a)
      (P : { g : _ | (forall a, f a = g a) } -> Type)
      (k : P (exist (fun g => forall a, f a = g a) f (fun a => eq_refl)))
      g
: P g.A:Type
B:A -> Type
f:forall a : A, B a
P:{g0 : forall x : A, B x |
forall a : A, f a = g0 a} -> Type
k:P
  (exist
     (fun g0 : forall x : A, B x =>
      forall a : A, f a = g0 a) f
     (fun a : A => eq_refl))
g:{g0 : forall x : A, B x |
forall a : A, f a = g0 a}
P g
Proof.A:Type
B:A -> Type
f:forall a : A, B a
P:{g0 : forall x : A, B x |
forall a : A, f a = g0 a} -> Type
k:P
  (exist
     (fun g0 : forall x : A, B x =>
      forall a : A, f a = g0 a) f
     (fun a : A => eq_refl))
g:{g0 : forall x : A, B x |
forall a : A, f a = g0 a}
P g
  destruct g as [g1 g2].A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g1:forall x : A, B x
g2:forall a : A, f a = g1 a
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) g1 g2)
  set (g' := fun x => (exist _ (g1 x) (g2 x))).A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g1:forall x : A, B x
g2:forall a : A, f a = g1 a
g':=fun x : A => exist (eq (f x)) (g1 x) (g2 x):forall x : A, {x0 : B x | f x = x0}
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) g1 g2)
  change g2 with (fun x => proj2_sig (g' x)).A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g1:forall x : A, B x
g2:forall a : A, f a = g1 a
g':=fun x : A => exist (eq (f x)) (g1 x) (g2 x):forall x : A, {x0 : B x | f x = x0}
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) g1
     (fun x : A => proj2_sig (g' x)))
  change g1 with (fun x => proj1_sig (g' x)).A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g1:forall x : A, B x
g2:forall a : A, f a = g1 a
g':=fun x : A => exist (eq (f x)) (g1 x) (g2 x):forall x : A, {x0 : B x | f x = x0}
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x)))
  clearbody g'; clear g1 g2.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x)))
  cut (forall x, (exist _ (f x) eq_refl) = g' x).A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
(forall x : A, exist (eq (f x)) (f x) eq_refl = g' x) ->
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x)))
A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
forall x : A, exist (eq (f x)) (f x) eq_refl = g' x
  {A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
(forall x : A, exist (eq (f x)) (f x) eq_refl = g' x) ->
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x))) intro H'.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
H':forall x : A,
exist (eq (f x)) (f x) eq_refl = g' x
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x)))
    apply functional_extensionality_dep_good in H'.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
H':(fun x : A => exist (eq (f x)) (f x) eq_refl) =
g'
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A => proj1_sig (g' x))
     (fun x : A => proj2_sig (g' x)))
    destruct H'.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a)
     (fun x : A =>
      proj1_sig (exist (eq (f x)) (f x) eq_refl))
     (fun x : A =>
      proj2_sig (exist (eq (f x)) (f x) eq_refl)))
    exact k. }A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
forall x : A, exist (eq (f x)) (f x) eq_refl = g' x
  {A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x : A, B x | forall a : A, f a = g a} ->
Type
k:P
  (exist
     (fun g : forall x : A, B x =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x : A, {x0 : B x | f x = x0}
forall x : A, exist (eq (f x)) (f x) eq_refl = g' x intro x.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x0 : A, B x0 |
forall a : A, f a = g a} -> Type
k:P
  (exist
     (fun g : forall x0 : A, B x0 =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x0 : A, {x : B x0 | f x0 = x}
x:A
exist (eq (f x)) (f x) eq_refl = g' x
    destruct (g' x) as [g'x1 g'x2].A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x0 : A, B x0 |
forall a : A, f a = g a} -> Type
k:P
  (exist
     (fun g : forall x0 : A, B x0 =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x0 : A, {x : B x0 | f x0 = x}
x:A
g'x1:B x
g'x2:f x = g'x1
exist (eq (f x)) (f x) eq_refl =
exist (eq (f x)) g'x1 g'x2
    destruct g'x2.A:Type
B:A -> Type
f:forall a : A, B a
P:{g : forall x0 : A, B x0 |
forall a : A, f a = g a} -> Type
k:P
  (exist
     (fun g : forall x0 : A, B x0 =>
      forall a : A, f a = g a) f
     (fun a : A => eq_refl))
g':forall x0 : A, {x : B x0 | f x0 = x}
x:A
exist (eq (f x)) (f x) eq_refl =
exist (eq (f x)) (f x) eq_refl
    reflexivity. }
Defined.

Definition forall_eq_rect
      {A B} (f : forall a : A, B a)
      (P : forall g, (forall a, f a = g a) -> Type)
      (k : P f (fun a => eq_refl))
      g H
  : P g H
  := @forall_sig_eq_rect A B f (fun g => P (proj1_sig g) (proj2_sig g)) k (exist _ g H).

Definition forall_eq_rect_comp {A B} f P k
  : @forall_eq_rect A B f P k f (fun _ => eq_refl) = k.A:Type
B:A -> Type
f:forall a : A, B a
P:forall g : forall x : A, B x,
(forall a : A, f a = g a) -> Type
k:P f (fun a : A => eq_refl)
forall_eq_rect f P k f (fun a : A => eq_refl) = k
Proof.A:Type
B:A -> Type
f:forall a : A, B a
P:forall g : forall x : A, B x,
(forall a : A, f a = g a) -> Type
k:P f (fun a : A => eq_refl)
forall_eq_rect f P k f (fun a : A => eq_refl) = k
  unfold forall_eq_rect, forall_sig_eq_rect; simpl.A:Type
B:A -> Type
f:forall a : A, B a
P:forall g : forall x : A, B x,
(forall a : A, f a = g a) -> Type
k:P f (fun a : A => eq_refl)
match
  functional_extensionality_dep_good
    (fun x : A => exist (eq (f x)) (f x) eq_refl)
    (fun x : A => exist (eq (f x)) (f x) eq_refl)
    (fun x : A => eq_refl) in (_ = y)
  return
    (P (fun x : A => proj1_sig (y x))
       (fun x : A => proj2_sig (y x)))
with
| eq_refl => k
end = k
  rewrite functional_extensionality_dep_good_refl; reflexivity.
Qed.

Definition f_equal__functional_extensionality_dep_good
           {A B f g} H a
  : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a.A:Type
B:A -> Type
f, g:forall x : A, B x
H:forall x : A, f x = g x
a:A
f_equal (fun h : forall x : A, B x => h a)
  (functional_extensionality_dep_good f g H) = H a
Proof.A:Type
B:A -> Type
f, g:forall x : A, B x
H:forall x : A, f x = g x
a:A
f_equal (fun h : forall x : A, B x => h a)
  (functional_extensionality_dep_good f g H) = H a
  apply forall_eq_rect with (H := H); clear H g.A:Type
B:A -> Type
f:forall x : A, B x
a:A
f_equal (fun h : forall x : A, B x => h a)
  (functional_extensionality_dep_good f f
     (fun a0 : A => eq_refl)) = eq_refl
  change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)).A:Type
B:A -> Type
f:forall x : A, B x
a:A
f_equal (fun h : forall x : A, B x => h a)
  (functional_extensionality_dep_good f f
     (fun a0 : A => eq_refl)) =
f_equal (fun h : forall x : A, B x => h a) eq_refl
  apply f_equal, functional_extensionality_dep_good_refl.
Defined.

Definition f_equal__functional_extensionality_dep_good__fun
           {A B f g} H
  : (fun a => f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H)) = H.A:Type
B:A -> Type
f, g:forall x : A, B x
H:forall x : A, f x = g x
(fun a : A =>
 f_equal (fun h : forall x : A, B x => h a)
   (functional_extensionality_dep_good f g H)) = H
Proof.A:Type
B:A -> Type
f, g:forall x : A, B x
H:forall x : A, f x = g x
(fun a : A =>
 f_equal (fun h : forall x : A, B x => h a)
   (functional_extensionality_dep_good f g H)) = H
  apply functional_extensionality_dep_good; intro a; apply f_equal__functional_extensionality_dep_good.
Defined.

Apply functional_extensionality, introducing variable x.

Tactic Notation "extensionality" ident(x) :=
  match goal with
    [ |- ?X = ?Y ] =>
    (apply (@functional_extensionality _ _ X Y) ||
     apply (@functional_extensionality_dep _ _ X Y) ||
     apply forall_extensionalityP ||
     apply forall_extensionalityS ||
     apply forall_extensionality) ; intro x
  end.

Iteratively apply functional_extensionality on an hypothesis until finding an equality statement

(* Note that you can write [Ltac extensionality_in_checker tac ::= tac tt.] to get a more informative error message. *)
Ltac extensionality_in_checker tac :=
  first [ tac tt | fail 1 "Anomaly: Unexpected error in extensionality tactic.  Please report." ].
Tactic Notation "extensionality" "in" hyp(H) :=
  let rec check_is_extensional_equality H :=
      lazymatch type of H with
      | _ = _ => constr:(Prop)
      | forall a : ?A, ?T
        => let Ha := fresh in
           constr:(forall a : A, match H a with Ha => ltac:(let v := check_is_extensional_equality Ha in exact v) end)
      end in
  let assert_is_extensional_equality H :=
      first [ let dummy := check_is_extensional_equality H in idtac
            | fail 1 "Not an extensional equality" ] in
  let assert_not_intensional_equality H :=
      lazymatch type of H with
      | _ = _ => fail "Already an intensional equality"
      | _ => idtac
      end in
  let enforce_no_body H :=
      (tryif (let dummy := (eval unfold H in H) in idtac)
        then clearbody H
        else idtac) in
  let rec extensionality_step_make_type H :=
      lazymatch type of H with
      | forall a : ?A, ?f = ?g
        => constr:({ H' | (fun a => f_equal (fun h => h a) H') = H })
      | forall a : ?A, _
        => let H' := fresh in
           constr:(forall a : A, match H a with H' => ltac:(let ret := extensionality_step_make_type H' in exact ret) end)
      end in
  let rec eta_contract T :=
      lazymatch (eval cbv beta in T) with
      | context T'[fun a : ?A => ?f a]
        => let T'' := context T'[f] in
           eta_contract T''
      | ?T => T
      end in
  let rec lift_sig_extensionality H :=
      lazymatch type of H with
      | sig _ => H
      | forall a : ?A, _
        => let Ha := fresh in
           let ret := constr:(fun a : A => match H a with Ha => ltac:(let v := lift_sig_extensionality Ha in exact v) end) in
           lazymatch type of ret with
           | forall a : ?A, sig (fun b : ?B => @?f a b = @?g a b)
             => eta_contract (exist (fun b : (forall a : A, B) => (fun a : A => f a (b a)) = (fun a : A => g a (b a)))
                                    (fun a : A => proj1_sig (ret a))
                                    (@functional_extensionality_dep_good _ _ _ _ (fun a : A => proj2_sig (ret a))))
           end
      end in
  let extensionality_pre_step H H_out Heq :=
      let T := extensionality_step_make_type H in
      let H' := fresh in
      assert (H' : T) by (intros; eexists; apply f_equal__functional_extensionality_dep_good__fun);
      let H''b := lift_sig_extensionality H' in
      case H''b; clear H';
      intros H_out Heq in
  let rec extensionality_rec H H_out Heq :=
      lazymatch type of H with
      | forall a, _ = _
        => extensionality_pre_step H H_out Heq
      | _
        => let pre_H_out' := fresh H_out in
           let H_out' := fresh pre_H_out' in
           extensionality_pre_step H H_out' Heq;
           let Heq' := fresh Heq in
           extensionality_rec H_out' H_out Heq';
           subst H_out'
      end in
  first [ assert_is_extensional_equality H | fail 1 "Not an extensional equality" ];
  first [ assert_not_intensional_equality H | fail 1 "Already an intensional equality" ];
  (tryif enforce_no_body H then idtac else clearbody H);
  let H_out := fresh in
  let Heq := fresh "Heq" in
  extensionality_in_checker ltac:(fun tt => extensionality_rec H H_out Heq);
  (* If we [subst H], things break if we already have another equation of the form [_ = H] *)
  destruct Heq; rename H_out into H.

Eta expansion is built into Coq.

Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) :
  f = fun x => f x.A:Type
B:A -> Type
f:forall x : A, B x
f = (fun x : A => f x)
Proof.A:Type
B:A -> Type
f:forall x : A, B x
f = (fun x : A => f x)
  intros.A:Type
B:A -> Type
f:forall x : A, B x
f = (fun x : A => f x)
  reflexivity.
Qed.

Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x.A, B:Type
f:A -> B
f = (fun x : A => f x)
Proof.A, B:Type
f:A -> B
f = (fun x : A => f x)
  apply (eta_expansion_dep f).
Qed.