diff options
| -rw-r--r-- | test-suite/output/FunExt.out | 15 | ||||
| -rw-r--r-- | test-suite/output/FunExt.v | 129 | ||||
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 19 |
3 files changed, 163 insertions, 0 deletions
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 000000000..b97fe7a88 --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,15 @@ +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not a non-dependent hypothesis. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not a non-dependent hypothesis. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v new file mode 100644 index 000000000..b5469b70b --- /dev/null +++ b/test-suite/output/FunExt.v @@ -0,0 +1,129 @@ +Require Import FunctionalExtensionality. + +(* Basic example *) +Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z). +intro H. +extensionality in H. +symmetry in H. +assumption. +Qed. + +(* Test rejection of non-equality *) +Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''. +intros H H' H''. +Fail extensionality in H. +clear H'. +Fail extensionality in H. +Fail extensionality in H''. +Abort. + +(* Test rejection of dependent equality *) +Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. +intros p H. +Fail extensionality in p. +clear H. +extensionality in p. +assumption. +Qed. + +(* Test dependent functional extensionality *) +Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b), + (forall x y, f x y = g x y) -> f = g. +intros * H. +extensionality in H. +assumption. +Qed. + +(* Other tests, courtesy of Jason Gross *) + +Goal forall A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c), (forall a b c, f a b c = g a b c) -> f = g. +Proof. + intros A B C D f g H. + extensionality in H. + match type of H with f = g => idtac end. + exact H. +Qed. + +Section test_section. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = g a b c). + Goal f = g. + Proof. + extensionality in H. + match type of H with f = g => idtac end. + exact H. + Qed. +End test_section. + +Section test2. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + extensionality in H. + match type of H with (fun b a c => f a b c) = (fun b' a' c' => g a' b' c') => idtac end. + exact H. + Qed. +End test2. + +Section test3. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a c, (fun b => f a b c) = (fun b => g a b c)). + Goal (fun a c b => f a b c) = (fun a c b => g a b c). + Proof. + extensionality in H. + match type of H with (fun a c b => f a b c) = (fun a' c' b' => g a' b' c') => idtac end. + exact H. + Qed. +End test3. + +Section test4. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c -> Type) + (H : forall b, (forall a c d, f a b c d) = (forall a c d, g a b c d)). + Goal (fun b => forall a c d, f a b c d) = (fun b => forall a c d, g a b c d). + Proof. + extensionality in H. + exact H. + Qed. +End test4. + +Section test5. + Goal nat -> True. + Proof. + intro n. + Fail extensionality in n. + constructor. + Qed. +End test5. + +Section test6. + Goal let f := fun A (x : A) => x in let pf := fun A x => @eq_refl _ (f A x) in f = f. + Proof. + intros f pf. + extensionality in pf. + match type of pf with f = f => idtac end. + exact pf. + Qed. +End test6. + +Section test7. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, True -> f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun a b c (_ : True) => f a b c) = (fun a' b' c' (_ : True) => g a' b' c') => idtac end. + constructor. + Qed. +End test7. + +Section test8. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : True -> forall a b c, f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun (_ : True) a b c => f a b c) = (fun (_ : True) a' b' c' => g a' b' c') => idtac end. + constructor. + Qed. +End test8. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 04d9a6704..133eba702 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -68,6 +68,25 @@ Tactic Notation "extensionality" ident(x) := apply forall_extensionality) ; intro x end. +(** Iteratively apply [functional_extensionality] on an hypothesis + until finding an equality statement *) + +Tactic Notation "extensionality" "in" hyp(H) := + let rec iter_fun_ext := + lazymatch type of H with + | _ = _ => exact H + | forall x, _ => + eapply functional_extensionality_dep; intro x; + (specialize (H x) || fail "Not a non-dependent hypothesis"); iter_fun_ext + | _ => fail "Not an extensional equality" + end in + let H' := fresh "H" in + simple refine (let H' := _ in _); + [shelve| + iter_fun_ext| + clearbody H'; move H' before H; + (clear H; rename H' into H) || fail "Not a non-dependent hypothesis"]. + (** Eta expansion follows from extensionality. *) Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : |