Mercurial > hg > Members > kono > Proof > automaton

comparison agda/logic.agda @ 73:031e00cea8f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 07 Nov 2019 11:36:23 +0900
parents c75aee1d6b4b
children 762d5a6fbe09
comparison
equal deleted inserted replaced
72:c75aee1d6b4b 73:031e00cea8f1
81 bool-≡-? : (a b : Bool) → Dec ( a ≡ b ) 81 bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
82 bool-≡-? true true = yes refl 82 bool-≡-? true true = yes refl
83 bool-≡-? true false = no (λ ()) 83 bool-≡-? true false = no (λ ())
84 bool-≡-? false true = no (λ ()) 84 bool-≡-? false true = no (λ ())
85 bool-≡-? false false = yes refl 85 bool-≡-? false false = yes refl
86
87 ¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false
88 ¬-bool-t {true} ne = ⊥-elim ( ne refl )
89 ¬-bool-t {false} ne = refl
90
91 ¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true
92 ¬-bool-f {true} ne = refl
93 ¬-bool-f {false} ne = ⊥-elim ( ne refl )
94
95 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
96 lemma-∧-0 {true} {true} refl ()
97 lemma-∧-0 {true} {false} ()
98 lemma-∧-0 {false} {true} ()
99 lemma-∧-0 {false} {false} ()
100
101 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
102 lemma-∧-1 {true} {true} refl ()
103 lemma-∧-1 {true} {false} ()
104 lemma-∧-1 {false} {true} ()
105 lemma-∧-1 {false} {false} ()