{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Exercise 6: Inductive relations Deadline: 12/3/10 Use the coursework submission (id: 272)) system to submit the coursework after demonstrating it in the lab to me or Darin. Prove the following propositions by completing the sheds { .. }. Note that not all propositions may be provable. If you think that a proposition is unprovable clearly mark this one by adding a line: -- impossible. -} module ex06 where open import Data.Nat open import Relation.Nullary open import Data.String open import Relation.Binary.PropositionalEquality {- Even we inductively define the predicate even. -} data Even : ℕ → Set where zero : Even zero sucsuc : ∀ {n} → Even n → Even (suc (suc n)) {- show that 4 is even. -} even4 : Even 4 even4 = {!!} {- show that 3 is not even. -} ¬even3 : ¬ (Even 3) ¬even3 = {!!} {- show that sucsuc is invertible -} inv-sucsuc : ∀ {n} → Even (suc (suc n)) → Even n inv-sucsuc = {!!} {- show that there is at most one proof of even. -} even-unique : ∀ {m} → (p q : Even m) → p ≡ q even-unique = {!!} {- show that even is decidable. -} even? : (n : ℕ) → Dec (Even n) even? = {!!} {- Combinatoric logic: we extend propositional logic by conjunction: -} data Formula : Set where Atom : String → Formula _⇒_ : (A B : Formula) → Formula _∧_ : (A B : Formula) → Formula data Context : Set where ε : Context _·_ : (Γ : Context) → (A : Formula) → Context infixl 7 _∧_ infixr 6 _⇒_ infix 4 _⊢sk_ infix 4 _⊢_ infixl 5 _·_ data _⊢_ : Context → Formula → Set where ass : ∀ {Γ A} → Γ · A ⊢ A weak : ∀ {Γ A B} → Γ ⊢ A → Γ · B ⊢ A app : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B abs : ∀ {Γ A B} → Γ · A ⊢ B → Γ ⊢ A ⇒ B {- To prove a conjuction we prove both components -} pair : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B {- To use a conjunction is the same as assuming both components -} elim : ∀ {Γ A B C} → Γ · A · B ⊢ C → Γ · A ∧ B ⊢ C {- In combinatory logic we add three combinators pair, fst and snd -} data _⊢sk_ : Context → Formula → Set where ass : ∀ {Γ A} → Γ · A ⊢sk A weak : ∀ {Γ A B} → Γ ⊢sk A → Γ · B ⊢sk A app : ∀ {Γ A B} → Γ ⊢sk A ⇒ B → Γ ⊢sk A → Γ ⊢sk B K : ∀ {Γ A B} → Γ ⊢sk A ⇒ B ⇒ A S : ∀ {Γ A B C} → Γ ⊢sk (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C pair : ∀ {Γ A B} → Γ ⊢sk A ⇒ B ⇒ A ∧ B fst : ∀ {Γ A B} → Γ ⊢sk A ∧ B ⇒ A snd : ∀ {Γ A B} → Γ ⊢sk A ∧ B ⇒ B {- Show that the two derivation relations are equivalent. Hint: You are welcome to reuse (and extend) proofs from l11.agda -} ⊢sk→⊢ : ∀ {Γ A} → Γ ⊢sk A → Γ ⊢ A ⊢sk→⊢ = {!!} ⊢→⊢sk : ∀ {Γ A} → Γ ⊢ A → Γ ⊢sk A ⊢→⊢sk = {!!}