module Live2 where {- A : Set Prime : Nat → Set Equals : Nat → Nat → Set _<_ : Nat → Nat → Set A → B (x : A) → P x -} I : {P : Set} → P → P I p = p K : {P Q : Set} → P → Q → P K p q = p S : {P Q R : Set} → (P → Q → R) → (P → Q) → P → R S = λ x → λ y → λ z → x z (y z) 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 comm∧ : {A B : Set} → A ∧ B → B ∧ A comm∧ (a , b) = (b , a) uncurry : {A B C : Set} → (A → B → C) → A ∧ B → C uncurry f (a , b) = f a b curry : {A B C : Set} → (A ∧ B → C) → A → B → C curry f a b = f (a , b) data _∨_ (A B : Set) : Set where left : A → A ∨ B right : B → A ∨ B ∨elim : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C ∨elim f g (left a) = f a ∨elim f g (right b) = g b distrib : {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) distrib (a , left b) = left (a , b) distrib (a , right c) = right (a , c) distrib' : {A B C : Set} → A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C) distrib' (left a) = left a , left a distrib' (right (b , c)) = right b , right c data ⊤ : Set where tt : ⊤ data ⊥ : Set where magic : {A : Set} → ⊥ → A magic () ¬_ : Set → Set ¬ A = A → ⊥ contradict : {A : Set} → ¬ (A ∧ ¬ A) contradict = λ x → snd x (fst x) contrapos : {A B : Set} → (A → B) → ¬ B → ¬ A contrapos = λ x y z → y (x z) not1 : {A B : Set} → A → ¬ A → B not1 = λ x y → magic (y x) not2 : {A B : Set} → (A → B) → (A → ¬ B) → ¬ A not2 = λ x y z → y z (x z) --de Morgan deMorgan1 : {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B deMorgan1 p = (λ x → p (left x)) , λ x → p (right x) deMorgan2 : {A B : Set} → (¬ A) ∧ (¬ B) → ¬ (A ∨ B) deMorgan2 (f , g) (left a) = f a deMorgan2 (f , g) (right b) = g b deMorgan3 : {A B : Set} → (¬ A) ∨ (¬ B) → ¬ (A ∧ B) deMorgan3 (left y) (y' , y0) = y y' deMorgan3 (right y) (y' , y0) = y y0 deMorgan4 : {A B : Set} → ¬ (A ∧ B) → (¬ A) ∨ (¬ B) deMorgan4 = λ x → left (λ x' → x (x' , {!!})) dndeMorgan4 : {A B : Set} → ¬ (A ∧ B) → ¬ ¬ ((¬ A) ∨ (¬ B)) dndeMorgan4 = λ x x' → x' (left (λ a → x' (right (λ b → x (a , b))))) lem1 : ∀{A}{B C : A → Set} → ((a : A) → B a ∧ C a) → ((a : A) → B a) ∧ ((a : A) → C a) lem1 {A} f = (λ (a : A) → fst (f a)) , λ (a : A) → snd (f a) lem2 : ∀{A}{B C : A → Set} → ((a : A) → B a) ∧ ((a : A) → C a) → (a : A) → B a ∧ C a lem2 (f , g) a = f a , g a data ∃ (A : Set)(B : A → Set) : Set where _,_ : (a : A) → B a → ∃ A B And : Set → Set → Set And A B = ∃ A (λ _ → B) lem3 : {A : Set}{B : A → Set}{C : Set} → ((a : A) → B a → C) → ∃ A (λ a → B a) → C lem3 f (a , b) = f a b lem4 : {A : Set}{B : A → Set}{C : Set} → (∃ A (λ a → B a) → C) → (a : A) → B a → C lem4 f a b = f (a , b) data Nat : Set where z : Nat s : Nat → Nat data Even : Nat → Set where zEven : Even z ssEven : ∀{n} → Even n → Even (s (s n)) data Odd : Nat → Set where zOdd : Odd (s z) ssOdd : ∀{n} → Odd n → Odd (s (s n)) oddtheneven : {n : Nat} → Odd n → Even (s n) oddtheneven zOdd = ssEven zEven oddtheneven (ssOdd p) = ssEven (oddtheneven p) eventhenodd : {n : Nat} → Even n → Odd (s n) eventhenodd zEven = zOdd eventhenodd (ssEven p) = ssOdd (eventhenodd p) oddeven : (n : Nat) → Odd n ∨ Even n oddeven z = right zEven oddeven (s n) with oddeven n ... | left p = right (oddtheneven p) ... | right p = left (eventhenodd p) mutual data even : Set where ez : even es : odd → even data odd : Set where os : even → odd nat2oddeven : Nat → odd ∨ even nat2oddeven z = right ez nat2oddeven (s n) with nat2oddeven n ... | left n' = right (es n') ... | right n' = left (os n') mutual odd2nat : odd → Nat odd2nat (os n) = s (even2nat n) even2nat : even → Nat even2nat ez = z even2nat (es n) = s (odd2nat n) oddeven2nat : odd ∨ even → Nat oddeven2nat (left n) = odd2nat n oddeven2nat (right n) = even2nat n data _≅_ {A : Set} : A → A → Set where refl : {a : A} → a ≅ a subst : (A : Set)(P : A → Set)(a a' : A) → a ≅ a' → P a → P a' subst A P a .a refl p = p resp : ∀{A B : Set}(f : A → B){a a'} → a ≅ a' → f a ≅ f a' resp f refl = refl ir : {A : Set}{a a' : A}(p q : a ≅ a') → p ≅ q ir refl refl = refl data _≤_ : Nat → Nat → Set where z≤ : ∀{n} → z ≤ n s≤ : ∀{m n} → m ≤ n → s m ≤ s n 1≤3 : s z ≤ s (s (s z)) 1≤3 = s≤ z≤ ¬3≤1 : ¬ (s (s (s z)) ≤ s z) ¬3≤1 (s≤ ()) refl≤ : ∀ n → n ≤ n refl≤ z = z≤ refl≤ (s n) = s≤ (refl≤ n) asym : ∀{m n} → m ≤ n → n ≤ m → m ≅ n asym z≤ z≤ = refl asym (s≤ p) (s≤ q) = resp s (asym p q) data List (A : Set) : Set where [] : List A _::_ : A → List A → List A length : ∀{A} → List A → Nat length [] = z length (a :: as) = s (length as) safehead : ∀{A} → (as : List A) → ∃ Nat (λ n → s n ≤ length as) → A safehead [] (a , ()) safehead (a :: as) p = a safetail : ∀{A} → (as : List A) → ∃ Nat (λ n → s n ≤ length as) → List A safetail [] (a , ()) safetail (a :: as) p = as