blob: ecb7428e9c67651012d396d268503d215a953603 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** 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.
Proof.
intros.
rewrite H.
auto.
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.
Proof.
intros ; eauto using @functional_extensionality_dep.
Qed.
(** 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)) ; intro x
end.
(** Eta expansion follows from extensionality. *)
Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) :
f = fun x => f x.
Proof.
intros.
extensionality x.
reflexivity.
Qed.
Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x.
Proof.
apply (eta_expansion_dep f).
Qed.
|
