Last active
October 20, 2016 00:54
-
-
Save phi16/3a3e1cc20b96699ea7bd6a68ab9434c8 to your computer and use it in GitHub Desktop.
科哲
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module logic_practice where | |
| infixr 0 _$_ | |
| infixl 10 _⇒_ _⇔_ | |
| infixl 20 _∨_ _∧_ | |
| infix 30 ¬_ | |
| _$_ : {A B : Set} → (A → B) → A → B | |
| _$_ f = f | |
| data ¬_ (A : Set) : Set where | |
| data _∨_ (A B : Set) : Set where | |
| data _∧_ (A B : Set) : Set where | |
| data _⇒_ (A B : Set) : Set where | |
| data _⇔_ (A B : Set) : Set where | |
| data Proof : Set → Set where | |
| postulate DD : {A : Set} → A → Proof A | |
| postulate CD : {A B : Set} → B → Proof (A ⇒ B) | |
| postulate ID : {A B : Set} → B → ¬ B → Proof A | |
| postulate ShowDD : {A : Set} → Proof A → A | |
| postulate ShowCD : {A B : Set} → (A → Proof (A ⇒ B)) → A ⇒ B | |
| postulate ShowID₁ : {A : Set} → (A → Proof (¬ A)) → ¬ A | |
| postulate ShowID₂ : {A : Set} → (¬ A → Proof A) → A | |
| postulate R : {A : Set} → A → A | |
| postulate MP : {A B : Set} → A → A ⇒ B → B | |
| postulate MT : {A B : Set} → ¬ B → A ⇒ B → ¬ A | |
| postulate DN₁ : {A : Set} → ¬ ¬ A → A | |
| postulate DN₂ : {A : Set} → A → ¬ ¬ A | |
| postulate S₁ : {A B : Set} → A ∧ B → A | |
| postulate S₂ : {A B : Set} → A ∧ B → B | |
| postulate Adj : {A B : Set} → A → B → A ∧ B | |
| postulate Add₁ : {A B : Set} → A → A ∨ B | |
| postulate Add₂ : {A B : Set} → B → A ∨ B | |
| postulate MTP₁ : {A B : Set} → ¬ A → A ∨ B → B | |
| postulate MTP₂ : {A B : Set} → ¬ B → A ∨ B → A | |
| postulate BC₁ : {A B : Set} → A ⇔ B → A ⇒ B | |
| postulate BC₂ : {A B : Set} → A ⇔ B → B ⇒ A | |
| postulate CB : {A B : Set} → A ⇒ B → B ⇒ A → A ⇔ B | |
| -- Mixed Deduction Validity | |
| DD⇒DD : {A : Set} → A → A | |
| DD⇒DD a = | |
| ShowDD $ let | |
| _ = a | |
| in DD a | |
| DD⇒CD : {A B : Set} → A → B ⇒ A | |
| DD⇒CD a = | |
| ShowDD $ let | |
| _ = a | |
| in CD a | |
| DD⇒ID : {A B : Set} → A → ¬ A → B | |
| DD⇒ID a ¬a = | |
| ShowDD $ let | |
| _ = a | |
| in ID a ¬a | |
| CD⇒DD : {A B : Set} → A ⇒ B → A ⇒ B | |
| CD⇒DD a⇒b = | |
| ShowCD $ λ a → let | |
| _ = a | |
| in DD a⇒b | |
| CD⇒CD : {A B : Set} → A ⇒ B → A ⇒ B | |
| CD⇒CD a⇒b = | |
| ShowCD $ λ a → let | |
| b = MP a a⇒b | |
| in CD b | |
| CD⇒ID : {A B : Set} → ¬ A → A ⇒ B | |
| CD⇒ID ¬a = | |
| ShowCD $ λ a → let | |
| _ = a | |
| in ID a ¬a | |
| ID⇒DD : {A : Set} → A → ¬ A → A | |
| ID⇒DD a ¬a = | |
| ShowID₂ $ λ ¬a → let | |
| _ = a | |
| in DD a | |
| ID⇒CD : {A B : Set} → B → A ⇒ B | |
| ID⇒CD b = | |
| ShowID₂ $ λ ¬[a⇒b] → let | |
| _ = b | |
| in CD b | |
| ID⇒ID : {A : Set} → A → A | |
| ID⇒ID a = | |
| ShowID₂ $ λ ¬a → let | |
| _ = a | |
| in ID a ¬a | |
| -- Q10 ~ Q17 | |
| Q10 : {P Q R S T : Set} → P ∨ Q → P ⇒ S → Q ⇔ T → S ∨ T | |
| Q10 p∨q p⇒s q⇔t = | |
| ShowID₂ $ λ ¬[s∨t] → let | |
| ¬t = | |
| ShowID₁ $ λ t → let | |
| s∨t = Add₂ t | |
| in ID s∨t ¬[s∨t] | |
| q⇒t = BC₁ q⇔t | |
| ¬q = MT ¬t q⇒t | |
| p = MTP₂ ¬q p∨q | |
| s = MP p p⇒s | |
| s∨t = Add₁ s | |
| in DD s∨t | |
| Q11 : {P R S : Set} → ¬ (P ∧ R) ⇒ (S ⇒ R) → R ∨ ¬ S | |
| Q11 ¬[p∧r]⇒[s⇒r] = | |
| ShowID₂ $ λ ¬[r∨¬s] → let | |
| ¬r = | |
| ShowID₁ $ λ r → let | |
| r∨¬s = Add₁ r | |
| in ID r∨¬s ¬[r∨¬s] | |
| ¬[p∧r] = | |
| ShowID₁ $ λ p∧r → let | |
| r = S₂ p∧r | |
| in ID r ¬r | |
| s⇒r = MP ¬[p∧r] ¬[p∧r]⇒[s⇒r] | |
| ¬s = MT ¬r s⇒r | |
| r∨¬s = Add₂ ¬s | |
| in DD r∨¬s | |
| Q12 : {P Q T R : Set} → (Q ∧ ¬ T) ∨ ¬ (T ⇒ Q) → (P ⇒ Q) ∨ (T ∨ R) | |
| Q12 [q∧¬t]∨¬[t⇒q] = | |
| ShowID₂ $ λ ¬[[p⇒q]∨[t∨r]] → let | |
| ¬t = | |
| ShowID₁ $ λ r → let | |
| t∨r = Add₁ r | |
| [p⇒q]∨[t∨r] = Add₂ t∨r | |
| in ID [p⇒q]∨[t∨r] ¬[[p⇒q]∨[t∨r]] | |
| t⇒q = | |
| ShowCD $ λ t → let | |
| _ = t | |
| in ID t ¬t | |
| ¬¬[t⇒q] = DN₂ t⇒q | |
| q∧¬t = MTP₂ ¬¬[t⇒q] [q∧¬t]∨¬[t⇒q] | |
| q = S₁ q∧¬t | |
| p⇒q = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in CD q | |
| [p⇒q]∨[t∨r] = Add₁ p⇒q | |
| in DD [p⇒q]∨[t∨r] | |
| Q13 : {P Q R : Set} → P ⇔ (Q ⇔ R) → P ⇔ Q → R | |
| Q13 p⇔[q⇔r] p⇔q = | |
| ShowID₂ $ λ ¬r → let | |
| ¬p = | |
| ShowID₁ $ λ p → let | |
| p⇒q = BC₁ p⇔q | |
| q = MP p p⇒q | |
| p⇒[q⇔r] = BC₁ p⇔[q⇔r] | |
| q⇔r = MP p p⇒[q⇔r] | |
| q⇒r = BC₁ q⇔r | |
| r = MP q q⇒r | |
| in ID r ¬r | |
| q⇒p = BC₂ p⇔q | |
| ¬q = MT ¬p q⇒p | |
| [q⇔r]⇒p = BC₂ p⇔[q⇔r] | |
| ¬[q⇔r] = MT ¬p [q⇔r]⇒p | |
| q⇒r = | |
| ShowCD $ λ q → let | |
| _ = q | |
| in ID q ¬q | |
| r⇒q = | |
| ShowCD $ λ r → let | |
| _ = r | |
| in ID r ¬r | |
| q⇔r = CB q⇒r r⇒q | |
| in ID q⇔r ¬[q⇔r] | |
| Q14 : {P Q R S T : Set} → (P ⇔ Q ∧ S) ∨ (P ⇔ R ∧ T) → P ⇒ Q ∨ R | |
| Q14 [p⇔q∧s]∨[p⇔r∧t] = | |
| ShowCD $ λ p → let | |
| q∨r = | |
| ShowID₂ $ λ ¬[q∨r] → let | |
| ¬[p⇔q∧s] = | |
| ShowID₁ $ λ p⇔q∧s → let | |
| p⇒q∧s = BC₁ p⇔q∧s | |
| q∧s = MP p p⇒q∧s | |
| q = S₁ q∧s | |
| q∨r = Add₁ q | |
| in ID q∨r ¬[q∨r] | |
| p⇔r∧t = MTP₁ ¬[p⇔q∧s] [p⇔q∧s]∨[p⇔r∧t] | |
| p⇒r∧t = BC₁ p⇔r∧t | |
| r∧t = MP p p⇒r∧t | |
| r = S₁ r∧t | |
| q∨r = Add₂ r | |
| in DD q∨r | |
| in CD q∨r | |
| Q15 : {P Q R S T : Set} → (¬ P ∧ T) ∨ (¬ ¬ R ∧ ¬ S) → ¬ (S ∨ ¬ T) → ¬ Q ⇒ (¬ S ⇒ ¬ R ∧ P) → Q | |
| Q15 [¬p∧t]∨[¬¬r∧¬s] ¬[s∨¬t] ¬q⇒[¬s⇒¬r∧p] = | |
| ShowID₂ $ λ ¬q → let | |
| ¬s⇒¬r∧p = MP ¬q ¬q⇒[¬s⇒¬r∧p] | |
| s = | |
| ShowID₂ $ λ ¬s → let | |
| ¬r∧p = MP ¬s ¬s⇒¬r∧p | |
| ¬r = S₁ ¬r∧p | |
| ¬[¬¬r∧¬s] = | |
| ShowID₁ $ λ ¬¬r∧¬s → let | |
| ¬¬r = S₁ ¬¬r∧¬s | |
| in ID ¬r ¬¬r | |
| ¬p∧t = MTP₂ ¬[¬¬r∧¬s] [¬p∧t]∨[¬¬r∧¬s] | |
| ¬p = S₁ ¬p∧t | |
| p = S₂ ¬r∧p | |
| in ID p ¬p | |
| s∨¬t = Add₁ s | |
| in ID s∨¬t ¬[s∨¬t] | |
| Q16 : {P Q R : Set} → ¬ (P ⇔ Q) → ¬ (P ⇔ R) → Q ⇔ R | |
| Q16 ¬[p⇔q] ¬[p⇔r] = | |
| ShowID₂ $ λ ¬[q⇔r] → let | |
| ¬r = | |
| ShowID₁ $ λ r → let | |
| ¬q = | |
| ShowID₁ $ λ q → let | |
| r⇒q = | |
| ShowCD $ λ r → let | |
| _ = r | |
| in CD q | |
| q⇒r = | |
| ShowCD $ λ q → let | |
| _ = q | |
| in CD r | |
| q⇔r = CB q⇒r r⇒q | |
| in ID q⇔r ¬[q⇔r] | |
| p = | |
| ShowID₂ $ λ ¬p → let | |
| q⇒p = | |
| ShowCD $ λ q → let | |
| _ = q | |
| in ID q ¬q | |
| p⇒q = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in ID p ¬p | |
| p⇔q = CB p⇒q q⇒p | |
| in ID p⇔q ¬[p⇔q] | |
| p⇒r = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in CD r | |
| r⇒p = | |
| ShowCD $ λ r → let | |
| _ = r | |
| in CD p | |
| p⇔r = CB p⇒r r⇒p | |
| in ID p⇔r ¬[p⇔r] | |
| q = | |
| ShowID₂ $ λ ¬q → let | |
| r⇒q = | |
| ShowCD $ λ r → let | |
| _ = r | |
| in ID r ¬r | |
| q⇒r = | |
| ShowCD $ λ q → let | |
| _ = q | |
| in ID q ¬q | |
| q⇔r = CB q⇒r r⇒q | |
| in ID q⇔r ¬[q⇔r] | |
| ¬p = | |
| ShowID₁ $ λ p → let | |
| q⇒p = | |
| ShowCD $ λ q → let | |
| _ = q | |
| in CD p | |
| p⇒q = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in CD q | |
| p⇔q = CB p⇒q q⇒p | |
| in ID p⇔q ¬[p⇔q] | |
| p⇒r = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in ID p ¬p | |
| r⇒p = | |
| ShowCD $ λ r → let | |
| _ = r | |
| in ID r ¬r | |
| p⇔r = CB p⇒r r⇒p | |
| in ID p⇔r ¬[p⇔r] | |
| Q17 : {P S T : Set} → ¬ (P ⇔ T) → P ∨ S → ¬ (P ∧ S) ⇒ (T ⇔ S) | |
| Q17 ¬[p⇔t] p∨s = | |
| ShowCD $ λ ¬[p∧s] → let | |
| t⇔s = | |
| ShowID₂ $ λ ¬[t⇔s] → let | |
| ¬p = | |
| ShowID₁ $ λ p → let | |
| ¬s = | |
| ShowID₁ $ λ s → let | |
| p∧s = Adj p s | |
| in ID p∧s ¬[p∧s] | |
| ¬t = | |
| ShowID₁ $ λ t → let | |
| p⇒t = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in CD t | |
| t⇒p = | |
| ShowCD $ λ t → let | |
| _ = t | |
| in CD p | |
| p⇔t = CB p⇒t t⇒p | |
| in ID p⇔t ¬[p⇔t] | |
| t⇒s = | |
| ShowCD $ λ t → let | |
| _ = t | |
| in ID t ¬t | |
| s⇒t = | |
| ShowCD $ λ s → let | |
| _ = s | |
| in ID s ¬s | |
| t⇔s = CB t⇒s s⇒t | |
| in ID t⇔s ¬[t⇔s] | |
| s = MTP₁ ¬p p∨s | |
| t = | |
| ShowID₂ $ λ ¬t → let | |
| p⇒t = | |
| ShowCD $ λ p → let | |
| _ = p | |
| in ID p ¬p | |
| t⇒p = | |
| ShowCD $ λ t → let | |
| _ = t | |
| in ID t ¬t | |
| p⇔t = CB p⇒t t⇒p | |
| in ID p⇔t ¬[p⇔t] | |
| s⇒t = | |
| ShowCD $ λ s → let | |
| _ = s | |
| in CD t | |
| t⇒s = | |
| ShowCD $ λ t → let | |
| _ = t | |
| in CD s | |
| t⇔s = CB t⇒s s⇒t | |
| in ID t⇔s ¬[t⇔s] | |
| in CD t⇔s |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment