Library Coq.Logic.FunctionalExtensionality
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.
Statements of functional extensionality for simple and dependent functions.
Extensionality of foralls follows from functional extensionality.
A version of functional_extensionality_dep which is provably
equal to eq_refl on fun _ => eq_refl
Apply functional_extensionality, introducing variable x.
Iteratively apply functional_extensionality on an hypothesis
until finding an equality statement
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);
destruct Heq;
rename H_out into H.
Eta expansion is built into Coq.