(** Introduction to Formal Reasoning (G52IFR) Tutorial 5 **) (** don't worry about this *) Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. Section CurryHoward. (** some variables *) Variables A B C : Set. Variables A' B' C' : Prop. (** I want to explain how to define functions by using the Curry-Howard correspondence *) Lemma lemma : (A' -> B') /\ (A' -> C') -> (A' -> B' /\ C'). intro abac. intro a. destruct abac as [ab ac]. split. apply ab. exact a. exact (ac a). Qed. Definition function : (A -> B) * (A -> C) -> (A -> B * C) := fun abac => fun a => match abac with | (ab , ac) => ( ab(a) , ac a ) end. End CurryHoward. Section Colours. (** 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. Variables A B : Set. (** 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 Colours.