(* Dokazovalni pomočnik Coq - demo. *) (* === Logika === *) (* Distributivnost konjunkcije in disjunkcije - verzija 1 *) Proposition distr_1 (p q r : Prop) : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r). Proof. split. - intro H. destruct H as [H1 H2]. destruct H2 as [G1 | G2]. + left. split. * exact H1. * assumption. + right. split ; assumption. - intros [[H1 H2] | [G1 G2]]. + split. * assumption. * tauto. + tauto. Qed. (* Distributivnost konjunkcije in disjunkcije - verzija 2 *) Proposition distr_2 (p q r : Prop) : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r). Proof. tauto. Qed. Print distr_2. (* Frobeniusov zakon - verzija 1 *) Proposition frobenius_1 (A : Type) (p : Prop) (q : A -> Prop) : (exists x : A, p /\ q x) <-> p /\ exists x, q x. Proof. split. - intro H. destruct H as [y [H1 H2]]. split. + assumption. + exists y. assumption. - intros [G1 G2]. destruct G2 as [x G2']. exists x. split ; assumption. Qed. (* Frobeniusov zakon - verzija 2 *) Proposition frobenius_2 (A : Type) (p : Prop) (q : A -> Prop) : (exists x, p /\ q x) <-> p /\ exists x, q x. Proof. split. - intros [x [? ?]]. split ; auto. now exists x. - intros [G1 [x G2']]. now exists x. Qed. (* Frobeniusov zakon - verzija 3 *) Proposition frobenius_3 (A : Type) (p : Prop) (q : A -> Prop) : (exists x, p /\ q x) <-> p /\ exists x, q x. Proof. firstorder. Qed. (* === Izomorfizmi === *) (* Preslikava f : A -> B je izomorfizem *) Definition is_iso {A B : Type} (f : A -> B) := exists (g : B -> A), (forall y, f (g y) = y) /\ (forall x, g (f x) = x). (* Identiteta na A *) Definition id (A : Type) := fun (x : A) => x. (* Identiteta je izomorfizem. *) Proposition id_is_iso (A : Type) : is_iso (id A). Proof. (* unfold is_iso. exists (id A). split. - intro x. unfold id. reflexivity. - reflexivity. *) now exists (id A). Qed. (* Kompozicija funkcij *) Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). Notation "g 'o' f" := (compose g f) (at level 50). Lemma gregor (p q r : Prop) : (p /\ q -> r) <-> (p -> q -> r). Proof. tauto. Qed. (* Kompozicija izomorfizmov je izomorfizem. *) Proposition comp_iso (A B C : Type) (f : A -> B) (g : B -> C) : is_iso f -> is_iso g -> is_iso (g o f). Proof. intros [f' [H1 H2]] [g' [G1 G2]]. exists (f' o g'). split. - intro z. unfold compose. rewrite H1. rewrite G1. reflexivity. - intro x. unfold compose. rewrite G2. apply H2. Qed. (* Množici A in B sta izomorfni *) Definition iso (A B : Type) := exists f : A -> B, is_iso f. Notation "A ≅ B" := (iso A B) (at level 40). (* Enotski tip *) Print unit. (* Produkt A in enote je izomoren A *) Proposition iso_unit_product (A : Type) : A * unit ≅ A. Proof. exists (fun p => fst p). exists (fun x => (x, tt)). split. - reflexivity. - intro p. destruct p as [x y]. destruct y. simpl. reflexivity. Qed. (* Princip ekstenzionalnosti za funkcije. *) Axiom funext : forall (A B : Type) (f g : A -> B), (forall x, f x = g x) -> f = g. (* Eksponentni zakon. *) Proposition iso_curry (A B C : Type) : (A * B -> C) ≅ (A -> (B -> C)). Proof. exists (fun f => (fun (x : A) => fun (y : B) => f (x, y))). exists (fun g => (fun (p : A * B) => g (fst p) (snd p))). split. - intro g. apply funext. intro. now apply funext. - intro f. apply funext. now intros [? ?]. Qed. (* f je injektivna funkcija *) Definition injective {A B : Type} (f : A -> B) := forall x y, f x = f y -> x = y. (* f je surjektivna funkcija *) Definition surjective {A B : Type} (f : A -> B) := forall y, exists x, f x = y. (** Potenčna množica A *) Definition P (A : Type) := A -> Prop. Notation "x ∈ S" := (S x) (at level 40, only parsing). (** Enojec {x} *) Definition singleton {A : Type} (x : A) : P A := fun y => x = y. (** Preslikava x ↦ {x} je injektivna *) Proposition singleton_injective (A : Type) : injective (fun (x : A) => singleton x). Proof. intros x y. intro E. assert (H : singleton y x = singleton x x). { now rewrite E. } unfold singleton in H. symmetry. now rewrite H. Qed. (** Presek podmnožic *) Definition intersection {A : Type} (S T : P A) := fun (x : A) => x ∈ S /\ x ∈ T. (** Slika podmnožice *) Definition image {A B : Type} (f : A -> B) (S : P A) : P B := fun (y : B) => exists x : A, x ∈ S /\ f x = y. (** Preslikava f : A -> B je injektivna natanko tedaj, ko f_* komutira s preseki. *) Proposition injective_image_intersection (A B : Type) (f : A -> B) : injective f <-> forall S T : P A, forall y, y ∈ image f (intersection S T) <-> y ∈ intersection (image f S) (image f T). Proof. split. - { intros f_inj S T. intro y. split. - intros [x [[x_S x_T] fx_y]]. split ; now exists x. - intros [[x1 [x1_S fx1_y]] [x2 [x2_T fx2_Y]]]. exists x1. split. + split. * assumption. * assert (E : x1 = x2). { apply f_inj. congruence. } destruct E. assumption. + assumption. } - { intro H. intros x y fx_fy. pose (z := f x). assert (K : z ∈ intersection (image f (singleton x)) (image f (singleton y))). { split. - now exists x. - now exists y. } now destruct (proj2 (H (singleton x) (singleton y) z) K) as [a [[[] []] ?]]. } Qed.