{-# OPTIONS --without-K #-} module Seance1 where -- import Relation.Binary.PropositionalEquality as Eq -- open Eq using (_≡_; refl; sym; trans; cong; cong-app) -- open Eq.≡-Reasoning -- Type C-c C-L for loading/compiling the file. -- For most exercises, try C-c C-a (automatic solution finder). -- If this fails, try C-c C-c (case study, on an arguement you'll be asked for). -- In all ases, you should be able to understand (and rebuild by hand) all proposed solutions. -- If not, please ask. -- * Elementary types -- An empty type data ⊥ : Set where -- A unit type data ⊤ : Set where ⋆ : ⊤ exe1 : ∀ {A : Set} -> ( A -> ⊤ ) exe1 x = ⋆ exe2 : ∀ {A : Set} -> A -> A exe2 x = x exe3 : ∀ {A : Set} -> ⊥ -> A exe3 () -- is the type ⊤ -> ⊥ inhabited ? -- ⊤ may play the rôle of the True proposition. -- ⊥ may play the rôle of the False proposition. -- Not to be confused with boolean "values" encoded below. -- * The Boolean type data Bool : Set where true : Bool false : Bool -- Propose an adequate cooding of the following (standard) boolean functions. -- Can you reduce the number of defining lines by factorizing some cases ? and : Bool -> Bool -> Bool and true true = true and true false = false and false true = false and false false = false or : Bool -> Bool -> Bool or false y = y or true _ = true negate : Bool -> Bool negate true = false negate false = true implies : Bool -> Bool -> Bool implies x true = true implies x false = negate x implies' : Bool -> Bool -> Bool implies' false _ = true implies' true y = y -- * equality data _≡_ {A : Set} (x : A) : A -> Set where refl : x ≡ x cong : ∀ {A B : Set}{x y : A} -> (f : A -> B) -> (x ≡ y) -> (f x ≡ f y) cong {x} {y} f refl = refl ≡-trans : ∀ {A : Set}{x y z : A} -> (x ≡ y) -> (y ≡ z) -> (x ≡ z) ≡-trans refl refl = refl ≡-sym : ∀ {A : Set} {x y : A} -> (x ≡ y) -> (y ≡ x) ≡-sym refl = refl -- * Product and sum data _×_ (A B : Set) : Set where _,_ : A -> B -> A × B fst : ∀ {A B : Set} -> A × B -> A fst (a , b) = a snd : ∀ {A B : Set} -> A × B -> B snd (a , b) = b factor_pair : ∀ {A B C : Set} -> (C -> A) -> (C -> B) -> C -> A × B factor_pair f g c = (f c , g c) data _+_ (A B : Set) : Set where inl : A -> A + B inr : B -> A + B factor_sum : ∀ {A B C : Set} -> (A -> C) -> (B -> C) -> (A + B) -> C factor_sum f g (inl a) = f a factor_sum f g (inr b) = g b -- * Naturals data Nat : Set where z : Nat s : Nat -> Nat sum : Nat -> Nat -> Nat sum1 : Nat -> Nat -> Nat sum z n = n sum (s m) n = s (sum m n) sum-z : ∀ {m : Nat} -> (m ≡ sum m z) sum-z {z} = refl sum-z {s m} = cong s sum-z sum-si : ∀ {m n : Nat} -> (sum m (s n) ≡ sum (s m) n) sum-si {z} {n} = refl sum-si {s m} {n} = cong s sum-si sum-s : ∀ {m n : Nat} -> (sum m (s n) ≡ s (sum m n)) sum-s {z} {n} = refl sum-s {s m} {n} = cong s sum-s sum-com : (m n : Nat) -> (sum m n ≡ sum n m) sum-com z n = ≡-trans refl (sum-z {n}) sum-com (s m) n = ≡-trans {Nat} {sum (s m) n} {s (sum m n)} {sum n (s m)} refl (≡-trans {Nat} {s (sum m n)} {s (sum n m)} {sum n (s m)} (cong s (sum-com m n)) (≡-sym sum-s)) sum1 m z = m sum1 m (s n) = s (sum1 m n) equal1 : (m n : Nat) -> (sum m n ≡ sum1 n m) equal1 z n = refl equal1 (s m) n = cong s (equal1 m n) equal2 : (m n : Nat) -> (sum m n ≡ sum1 m n) equal2 m n = ≡-trans (sum-com m n) (equal1 n m)