{-# OPTIONS --allow-unsolved-metas #-}
module practice-logic where

postulate A : Set
postulate B : Set

postulate b : B

lemma0 : A -> B
lemma0 a = b

id : { A : Set } → ( A → A )
id = {!!}

id' : { A : Set } → ( A → A )
id' x  = {!!}

_・_ : {A B C : Set } → {!!}
f ・ g = λ x → f ( g x )    


Lemma1 : Set
Lemma1 = A -> ( A -> B ) -> B

lemma1 : Lemma1
lemma1 a f = f a

-- lemma1 a a-b = a-b a

lemma2 : Lemma1
lemma2 = \a b -> {!!}

-- lemma1 = \a a-b -> a-b a
-- lemma1 = \a b -> b a
-- lemma1  a b = b a

lemma3 : Lemma1
lemma3 = \a -> ( \b -> {!!} )

record _∧_ (A B : Set) : Set where
   field 
      and1 : A
      and2 : B

data _∧d_ ( A B : Set ) : Set where
  and : A -> B -> A ∧d B

Lemma4 : Set
Lemma4 = B -> A -> (B ∧ A)
lemma4 : Lemma4
lemma4 = \b -> \a -> {!!}

Lemma5 : Set
Lemma5 = (A ∧ B) -> B

lemma5 : Lemma5
lemma5 = \a -> {!!}

data _∨_  (A B : Set) : Set where
  or1 : A -> A ∨ B
  or2 : B -> A ∨ B

Lemma6  : Set
Lemma6 = B -> ( A ∨ B )

lemma6 : Lemma6
lemma6 = \b -> {!!}

open _∧_

ex1 : {A B : Set} → ( A ∧ B ) → A 
ex1 a∧b = {!!}

ex2 : {A B : Set} → ( A ∧ B ) → B 
ex2 a∧b = {!!}

ex3 : {A B : Set} → A → B → ( A ∧ B ) 
ex3 a b = {!!}

ex4 : {A : Set} → A → ( A ∧ A ) 
ex4 a  = record { and1 = {!!} ;  and2 = {!!} }

ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
ex5 a∧b∧c = {!!}

ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
ex6  p a = {!!} 

ex7 : {A : Set} → ( A ∨ A ) → A
ex7 = {!!}

ex8 : {A B : Set} → B → ( A ∨ ( B → A ) ) → A
ex8 = {!!}

open import Relation.Nullary
open import Relation.Binary
open import Data.Empty

contra-position :  {A : Set } {B : Set } → (A → B) → ¬ B → ¬ A
contra-position {A} {B}  f ¬b a = {!!}

double-neg :  {A : Set } → A → ¬ ¬ A
double-neg x y = y x


lemma :  {A : Set } →  A ∨ ( ¬ A ) → ¬ ¬ A → A
lemma = {!!}

double-neg2 :  {A : Set } → ¬ ¬ ¬ A → ¬ A
double-neg2 = {!!}

de-morgan :  {A B : Set } →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
de-morgan {A} {B} = {!!}

dont-or : {A  : Set } { B : Set  } →  A ∨ B → ¬ A → B
dont-or {A} {B} = {!!}