(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus Tutorial 4: Sets **) Section Tutorial4. (** two colours **) Inductive Colour : Set := | blue : Colour | red : Colour. (** more complicated colours**) Inductive ComplColour : Set := | orange : ComplColour | aBitDarker : Colour -> ComplColour | mix : ComplColour -> ComplColour -> ComplColour. (** "mix (aBitDarker blue) (aBitDarker red)" could be something like violet **) (** the identity function **) Definition id : Colour -> Colour := fun (c : Colour) => match c with | red => red | blue => blue end. (** again **) Definition id' : Colour -> Colour := fun c => c. (** can we prove id = id'? **) Axiom extensionality : forall A B : Set, forall f g : A -> B, (forall a : A, f a = g a) -> f = g. Lemma same : id = id'. apply extensionality. intro c. destruct c. reflexivity. reflexivity. Qed. Inductive Rows : Set := | r1 : Rows | r2 : Rows. Inductive Cols : Set := | c1 | c2. Definition Board : Set := Rows * Cols -> Colour. (** a special board: every field is red **) Definition allRed : Board := fun (rc : Rows * Cols) => red. (** More general sets could be more interesting! **) Variables A B : Set. (** this it the eta law: if you abstract a varia**) Lemma eta : forall f : A -> B, f = (fun a => f a). intro f. apply extensionality. intro a. reflexivity. Qed. (** let's do an exercise about isomorphism of sets **) (** do not worry about these commands for now: **) Open Scope type_scope. Set Implicit Arguments. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. (** Let's construct an isomorphism between two sets **) Definition S1 : Set := (A + B) * Colour. Definition S2 : Set := Colour * B + Colour * A. Definition f : S1 -> S2 := fun (s : S1) => match s with | (ab , c) => match ab with | (inl a) => inr (c , a) | (inr b) => inl (c , b) end end. Definition g : S2 -> S1 := fun s => match s with | inl (c , b) => (inr b , c) | inr (c , a) => (inl a , c) end. Lemma firstFthenGisID : forall s : S1, g(f(s)) = s. intro s. destruct s as (ab , c). destruct ab. simpl. reflexivity. unfold g. unfold f. reflexivity. Qed. Lemma firstGthenFisID : forall s : S2, f(g(s)) = s. intro s. destruct s; destruct p; reflexivity. Qed. End Tutorial4.