Mercurial > hg > Gears > GearsAgda

annotate logic.agda @ 948:e5288029f850

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RBTree fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Jul 2024 17:01:50 +0900
parents 0b791ae19543
children 057d3309ed9d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
948
e5288029f850 RBTree fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 782
diff changeset
1 {-# OPTIONS --safe --cubical-compatible #-}
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 module logic where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
781
Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level
Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Relation.Nullary
781
Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Binary hiding (_⇔_)
586
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
8 open import Relation.Binary.PropositionalEquality
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
9
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Data.Empty
586
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
11 open import Data.Nat hiding (_⊔_)
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 data Bool : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 true : Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 false : Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
609
79418701a283 add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 604
diff changeset
19 constructor ⟪_,_⟫
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 proj1 : A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 proj2 : B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 case1 : A → A ∨ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 case2 : B → A ∨ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 _⇔_ A B = ( A → B ) ∧ ( B → A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 double-neg A notnot = notnot A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 double-neg2 notnot A = notnot ( double-neg A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 dont-or :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 dont-or {A} {B} (case2 b) ¬A = b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 dont-orb :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 dont-orb {A} {B} (case1 a) ¬B = a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 infixr 130 _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 infixr 140 _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 infixr 150 _⇔_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 _/\_ : Bool → Bool → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 true /\ true = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 _ /\ _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
586
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
61 _<B?_ : ℕ → ℕ → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
62 ℕ.zero <B? x = true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
63 ℕ.suc x <B? ℕ.zero = false
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
64 ℕ.suc x <B? ℕ.suc xx = x <B? xx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
65
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
66 -- _<BT_ : ℕ → ℕ → Set
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
67 -- ℕ.zero <BT ℕ.zero = ⊤
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
68 -- ℕ.zero <BT ℕ.suc b = ⊤
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
69 -- ℕ.suc a <BT ℕ.zero = ⊥
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
70 -- ℕ.suc a <BT ℕ.suc b = a <BT b
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
71
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
72
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
73 _≟B_ : Decidable {A = Bool} _≡_
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
74 true ≟B true = yes refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
75 false ≟B false = yes refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
76 true ≟B false = no λ()
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
77 false ≟B true = no λ()
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents: 579
diff changeset
78
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 _\/_ : Bool → Bool → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 false \/ false = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 _ \/ _ = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 not_ : Bool → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 not true = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 not false = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 _<=>_ : Bool → Bool → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 true <=> true = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 false <=> false = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 _ <=> _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 infixr 130 _\/_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 infixr 140 _/\_