(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus Tutorial 4: Sets **) Section Tutorial4. (** two colours **) Inductive Colour : Set := | blue : Colour | red : Colour. (** the identity function **) Definition id : Colour -> Colour := (** again **) Definition id' : Colour -> Colour := (** can we prove id = id'? **) Lemma same : id = id'. Inductive Rows : Set := Inductive Cols : Set := Definition Board : Set := (** a special board: every field is red **) Definition allRed : Board := (** 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). (** 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 := Definition S2 : Set := End Tutorial4.