|
(* -*- coq-prog-args: ("-async-proofs" "no") -*- *)
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 success on dependent equality *)
Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1.
intros p 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 => f a b) = (fun b' a' => g a' b') => 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) => f) = (fun (_ : True) => g) => idtac end.
constructor.
Qed.
End test8.
Section test9.
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.
pose H as H'.
extensionality in H.
extensionality in H'.
let T := type of H in let T' := type of H' in constr_eq T T'.
match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end.
exact H'.
Qed.
End test9.
Section test10.
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 : f = g).
Goal True.
Proof.
Fail extensionality in H.
constructor.
Qed.
End test10.
Section test11.
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 = f a b c).
Goal True.
Proof.
pose H as H'.
pose (eq_refl : H = H') as e.
extensionality in H.
Fail extensionality in H'.
clear e.
extensionality in H'.
let T := type of H in let T' := type of H' in constr_eq T T'.
lazymatch type of H with f = f => idtac end.
constructor.
Qed.
End test11.
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
