\documentclass{exam} \usepackage{agda} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage[greek,english]{babel} \usepackage{textgreek} \usepackage{hyperref} \DeclareUnicodeCharacter{"2096}{\ensuremath{_k}} \DeclareUnicodeCharacter{"22A8}{\ensuremath{\models}} \DeclareUnicodeCharacter{"2248}{\ensuremath{\approx}} \begin{document} \AgdaHide{ \begin{code} module Exercise2 where infix 2 _×_ _⊔_ infix 3 _≡_ infix 3 _≈_ data Nat : Set where zero : Nat succ : Nat → Nat {-# BUILTIN NATURAL Nat #-} _+_ : Nat → Nat → Nat m + zero = m m + succ n = succ (m + n) data Empty : Set where record Unit : Set where data _×_ (A B : Set) : Set where _,_ : A → B → A × B data _⊔_ (A B : Set) : Set where inl : A → A ⊔ B inr : B → A ⊔ B data _≡_ {A : Set} (a : A) : A → Set where refl : a ≡ a open import Agda.Primitive using (Level) renaming (_⊔_ to max) data Σ {l l'} (A : Set l) (B : A → Set l') : Set (max l l') where _,_ : (a : A) → B a → Σ A B ⊤ : Set ⊤ = Unit _∧_ : (A B : Set) → Set _∧_ = _×_ ¬_ : (A : Set) → Set ¬_ A = A → Empty record _≈_ (A B : Set) : Set where field ltr : A → B rtl : B → A open _≈_ \end{code} } \title{Types for Programs and Proofs 2017/2018\\Exercise Session 2} \maketitle \section{Exercises} \begin{questions} \question The type of the identity function \AgdaFunction{I} with implicit polymorphism is \begin{code} I : ∀ {X : Set} → X → X \end{code} Write \AgdaFunction{I} using λ-notation. \begin{code} I = {!!} \end{code} \question Define the \AgdaFunction{K}- and \AgdaFunction{S}-combinators. \begin{code} K : ∀ {X Y : Set} → X → Y → X K = {!!} S : ∀ {X Y Z : Set} → (X → Y) → (X → Y → Z) → X → Z S = {!!} \end{code} \question Define the \AgdaFunction{I}-combinator using only application, \AgdaFunction{K} and \AgdaFunction{S}. \begin{code} I' : ∀ {X : Set} → X → X I' = {!!} \end{code} \question Prove symmetry and transitivity of propositional identity \AgdaDatatype{\_≡\_} by pattern matching. \begin{code} sym : ∀ {A} {a b : A} → a ≡ b → b ≡ a sym = {!!} trans : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans = {!!} \end{code} \question Prove symmetry and transitivity without pattern matching by using \AgdaFunction{subst}. \begin{code} subst : ∀ {A} {P : A → Set} {a b} → a ≡ b → P a → P b subst refl p = p sym' : ∀ {A} {a b : A} → a ≡ b → b ≡ a sym' = {!!} trans' : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans' = {!!} \end{code} \question Prove commutativity of addition \AgdaFunction{\_+\_}. \begin{code} 0-neutral-right : ∀ {m} → m + 0 ≡ m 0-neutral-right = {!!} 0-neutral-left : ∀ {n} → 0 + n ≡ n 0-neutral-left = {!!} succ-+-right : ∀ {m n} → m + succ n ≡ succ (m + n) succ-+-right = {!!} succ-+-left : ∀ {m n} → succ m + n ≡ succ (m + n) succ-+-left = {!!} comm-+ : ∀ {m n} → m + n ≡ n + m comm-+ = {!!} \end{code} \question Prove the commutativity, idempotency and neutrality laws for conjunction \AgdaFunction{\_∧\_}. \begin{code} comm-∧ : ∀ {A B} → A ∧ B ≈ B ∧ A comm-∧ = {!!} idem-∧ : ∀ {A} → A ∧ A ≈ A idem-∧ = {!!} neutral-∧ : ∀ {A} → A ∧ ⊤ ≈ A neutral-∧ = {!!} \end{code} \question Prove the involution law for negation, assuming you can decide whether a type is empty (the false proposition) or inhabited (the true proposition). \AgdaHide{ \begin{code} module M where \end{code} } \begin{code} postulate L : ∀ {A} → A ⊔ (A → Empty) invol-¬ : ∀ {A} → ¬ ¬ A ≈ A invol-¬ = {!!} \end{code} \question Find a Kripke structure\cite[Chapter 10]{stump16} \AgdaBound{k} where negation is \emph{not} involutive, i.\,e.\ there is a formula \AgdaBound{f} and a world \AgdaBound{w} such that the instance of the law fails there. \AgdaHide{ \begin{code} data Formula : Set where $: Nat → Formula True : Formula False : Formula Implies : Formula → Formula → Formula And : Formula → Formula → Formula Or : Formula → Formula → Formula Not : Formula → Formula Not f = Implies f False \end{code} } \begin{code} record KripkeStructure : Set₁ where field -- a set of worlds W : Set -- a reflexive and transitive relation on W R : W → W → Set reflR : ∀ (w : W) → R w w transR : ∀ {w v u : W} → R w v → R v u → R w u -- a valuation telling whether atomic formula i is true or false in a given -- world V : W → Nat → Set monoV : ∀ {w v : W} → R w v → ∀ (i : Nat) → V w i → V v i open KripkeStructure _,_⊨ₖ_ : ∀ (k : KripkeStructure) → W k → Formula → Set k , w ⊨ₖ$ x = V k w x k , w ⊨ₖ True = Unit k , w ⊨ₖ False = Empty k , w ⊨ₖ Implies f₁ f₂ = ∀ {v : W k} → R k w v → k , v ⊨ₖ f₁ → k , v ⊨ₖ f₂ k , w ⊨ₖ And f₁ f₂ = k , w ⊨ₖ f₁ × k , w ⊨ₖ f₂ k , w ⊨ₖ Or f₁ f₂ = k , w ⊨ₖ f₁ ⊔ k , w ⊨ₖ f₂ \end{code} \AgdaHide{ \begin{code} data World : Set where w₀ : World w₁ : World data Rel : World → World → Set where r₀₀ : Rel w₀ w₀ r₁₁ : Rel w₁ w₁ -- ... refl-Rel : ∀ (w : World) → Rel w w refl-Rel w₀ = r₀₀ refl-Rel w₁ = r₁₁ trans-Rel : ∀ {w v u : World} → Rel w v → Rel v u → Rel w u trans-Rel = {!!} Val : World → Nat → Set Val = {!!} mono-Val : ∀ {w v : World} → Rel w v → ∀ (i : Nat) → Val w i → Val v i mono-Val = {!!} f : Formula f = {!!} k : KripkeStructure k = record { W = World ; R = Rel ; reflR = refl-Rel ; transR = trans-Rel ; V = Val ; monoV = mono-Val } w : World w = {!!} \end{code} } \begin{code} not-invol-Not : (k , w ⊨ₖ Implies (Not (Not f)) f) → Empty not-invol-Not = {!!} \end{code} \end{questions} \begin{thebibliography}{9} \bibitem{stump16} Aaron Stump, \textit{Verified Functional Programming in Agda}, Association for Computing Machinery and Morgan \& Claypool Publishers, 2016. \bibitem{dybjer17} Peter Dybjer, \textit{An Introduction to Programming and Proving in Agda}, 2017. \bibitem{agda17} Agda contributors, \textit{The Agda User Manual}, \url{https://agda.readthedocs.io/en/latest/}, 2017. \end{thebibliography} \end{document}