Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: indfun.ml Sprache: Coq

Original von: Coq^©

(* -*- 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.27 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.