Mercurial > hg > Gears > GearsAgda
view logic.agda @ 825:02f431665ebc
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 29 Jan 2024 11:42:39 +0900 |
parents | 0b791ae19543 |
children | e5288029f850 |
line wrap: on
line source
module logic where open import Level open import Relation.Nullary open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality open import Data.Empty open import Data.Nat hiding (_⊔_) data Bool : Set where true : Bool false : Bool record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where constructor ⟪_,_⟫ field proj1 : A proj2 : B data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where case1 : A → A ∨ B case2 : B → A ∨ B _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) _⇔_ A B = ( A → B ) ∧ ( B → A ) contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A double-neg A notnot = notnot A double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A double-neg2 notnot A = notnot ( double-neg A ) de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) dont-or {A} {B} (case2 b) ¬A = b dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b ) dont-orb {A} {B} (case1 a) ¬B = a infixr 130 _∧_ infixr 140 _∨_ infixr 150 _⇔_ _/\_ : Bool → Bool → Bool true /\ true = true _ /\ _ = false _<B?_ : ℕ → ℕ → Bool ℕ.zero <B? x = true ℕ.suc x <B? ℕ.zero = false ℕ.suc x <B? ℕ.suc xx = x <B? xx -- _<BT_ : ℕ → ℕ → Set -- ℕ.zero <BT ℕ.zero = ⊤ -- ℕ.zero <BT ℕ.suc b = ⊤ -- ℕ.suc a <BT ℕ.zero = ⊥ -- ℕ.suc a <BT ℕ.suc b = a <BT b _≟B_ : Decidable {A = Bool} _≡_ true ≟B true = yes refl false ≟B false = yes refl true ≟B false = no λ() false ≟B true = no λ() _\/_ : Bool → Bool → Bool false \/ false = false _ \/ _ = true not_ : Bool → Bool not true = false not false = true _<=>_ : Bool → Bool → Bool true <=> true = true false <=> false = true _ <=> _ = false infixr 130 _\/_ infixr 140 _/\_