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

postulate A : Set
postulate B : Set

postulate b : B

lemma0 : A -> B
lemma0 a = {!!}

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
   constructor _,_
   field 
      π1 : A
      π2 : 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
  case1 : A -> A ∨ B
  case2 : 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 { π1 = {!!} ;  π2 = {!!} }

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 (case1 a) = a
ex7 (case2 a) = a

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 = {!!}

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

contra-position1 :  {A : Set } {B : Set } → (B ∨ ( ¬ B ))  → (¬ B → ¬ A )→ (A → B)
contra-position1 {A} {B} = {!!}

double-neg :  {A : Set } → A → ¬ (¬ A)
double-neg = {!!}

double-neg' :  {A : Set } → A → ( A → ⊥ ) → ⊥ 
double-neg' = {!!}

double-neg1 :  {A : Set } → ¬ (¬ A) → A
double-neg1 x = {!!}

lem :  {A : Set } → A ∨ ( ¬ A )  -- 排中律 law of exclude middle LEM
lem = {!!}

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

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

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

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