Adding an "extensionality in H" tactic which applies functional

extensionality in H supposed to be a quantified equality until
giving a bare equality.

Thanks to Jason Gross and Jonathan Leivent for suggestions and
examples.

1 files changed, 129 insertions, 0 deletions

diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v
new file mode 100644
index 0000000000..b5469b70bf
--- /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.