Mercurial > hg > Members > kono > Proof > agda-intro > agda

changeset 0:81966c2f4df6 draft default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Agda introduction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 16 Nov 2022 14:54:09 +0900
parents
children
files dag.agda data1.agda equality.agda lambda.agda level1.agda list.agda logic.agda practice-logic.agda practice-nat.agda record1.agda test.agda
diffstat 11 files changed, 895 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/dag.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,75 @@
+module dag where
+
+--         f0
+--       -----→
+--    t0         t1
+--       -----→
+--         f1
+
+
+data  TwoObject   : Set  where
+       t0 : TwoObject
+       t1 : TwoObject
+
+
+data TwoArrow  : TwoObject → TwoObject → Set  where
+       f0 :  TwoArrow t0 t1
+       f1 :  TwoArrow t0 t1
+
+
+--         r0
+--       -----→
+--    t0         t1
+--       ←-----
+--         r1
+
+data Circle  : TwoObject → TwoObject → Set  where
+       r0 :  Circle t0 t1
+       r1 :  Circle t1 t0
+
+data ⊥ : Set where
+
+⊥-elim : {A : Set } -> ⊥ -> A
+⊥-elim ()
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+data Bool  : Set  where
+       true :  Bool
+       false :  Bool
+
+data connected { V : Set } ( E : V → V → Set ) ( x y : V ) : Set  where
+    direct :   E x y → connected E x y 
+    indirect :  { z : V  } → E x z  →  connected {V} E z y → connected E x y
+
+lemma1 : connected TwoArrow t0 t1
+lemma1 =  {!!}
+
+lemma2 : ¬ ( connected TwoArrow t1 t0 )
+lemma2 = {!!}
+
+-- lemma2 (direct ())
+-- lemma2 (indirect () (direct _))
+-- lemma2 (indirect () (indirect _ _ ))
+
+lemma3 : connected Circle t0 t0
+lemma3 = {!!}
+
+data Dec (P : Set) : Set where
+   yes :   P → Dec P
+   no  : ¬ P → Dec P
+
+reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
+reachable {V} E x y = Dec ( connected {V} E x y )
+
+dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+lemma4 : dag TwoArrow
+lemma4 = {!!}
+
+lemma5 :  ¬ ( dag Circle )
+lemma5 x = ⊥-elim {!!}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/data1.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,121 @@
+module data1 where
+
+data _∨_ (A B : Set) : Set where
+  case1 : A → A ∨ B
+  case2 : B → A ∨ B
+
+ex1 : {A B : Set} → A → ( A ∨ B ) 
+ex1  a = case1 a
+
+ex2 : {A B : Set} → ( B → ( A ∨ B ) )
+ex2 = λ b → case2 b
+
+ex3 : {A B : Set} → ( A ∨ A ) → A 
+ex3 (case1 x) = x
+ex3 (case2 x) = x
+
+ex4 : {A B C : Set} →  A ∨ ( B ∨ C ) → ( A ∨  B ) ∨ C 
+ex4 (case1 a) = case1 (case1 a )
+ex4 (case2 (case1 b)) = case1 (case2 b)
+ex4 (case2 (case2 c)) = case2 c
+
+record _∧_ A B : Set where
+  constructor  ⟪_,_⟫
+  field
+     proj1 : A
+     proj2 : B
+
+open _∧_
+
+ex3' : {A B : Set} → ( A ∨ B ) →   A ∧ B   -- this is wrong
+ex3' = ?
+
+ex4' : {A B : Set} → ( A ∧ B ) →   A ∨ B   
+ex4' ab = case1 (proj1 ab )
+
+--- ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∨  B ) → C ) is wrong
+ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∧  B ) → C )
+ex5 (case1 a→c) ab = a→c (proj1 ab)
+ex5 (case2 b→c) ab = b→c (proj2 ab)
+
+data ⊥ : Set where
+
+⊥-elim : {A : Set } -> ⊥ -> A
+⊥-elim = {!!}
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+
+record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
+     field
+        fact1 : ( Cat ∨ Dog ) → ¬ Goat
+        fact2 : ¬ Cat →  ( Dog ∨ Rabbit )
+        fact3 : ¬ ( Cat ∨ Goat ) →  Rabbit
+
+postulate
+     lem : (a : Set) → a ∨ ( ¬ a )
+
+module tmp ( Cat Dog Goat Rabbit : Set ) (p :  PetResearch  Cat Dog Goat Rabbit ) where
+
+    open PetResearch
+
+    problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
+    problem0 with lem Cat  | lem Goat
+    ... | case1 cat | y = case1 (case1 {!!})
+    ... | case2 x | case1 goat = case1 {!!}
+    ... | case2 ¬cat | case2 ¬goat = case2 (fact3 p lemma1 ) where
+       lemma1 : ¬ (Cat ∨ Goat)
+       lemma1 (case1 cat) = ¬cat cat
+       lemma1 (case2 goat) = {!!}
+
+    problem1 : Goat → ¬ Dog
+    problem1 = {!!}
+ 
+    problem2 : Goat → Rabbit
+    problem2 = {!!}
+
+
+data Three : Set where
+  t1 : Three
+  t2 : Three
+  t3 : Three
+
+open Three
+
+infixl 110 _∨_ 
+
+--         t1
+--        /  \ r1
+--      t3 ←  t2
+--         r2
+
+data 3Ring : (dom cod : Three) → Set where
+   r1 : 3Ring t1 t2
+   r2 : 3Ring t2 t3
+   r3 : 3Ring t3 t1
+
+data Nat : Set where
+  zero : Nat
+  suc  : Nat →  Nat
+
+add : ( a b : Nat ) → Nat
+add zero x = x
+add (suc x) y = suc ( add x y )
+
+mul : ( a b : Nat ) → Nat
+mul zero x = zero
+mul (suc x) y = add y (mul x y)
+
+ex6 : Nat
+ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
+
+data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
+   direct :   E x y -> connected E x y
+   indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
+
+dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+lemma : ¬ (dag 3Ring )
+lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/equality.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,26 @@
+module equality where
+
+
+data _==_ {A : Set } : A → A → Set where
+   refl :  {x : A} → x == x
+
+ex1 : {A : Set} {x : A } → x == x
+ex1  = ?
+
+ex2 : {A : Set} {x y : A } → x == y → y == x
+ex2 = ?
+
+ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
+ex3 = {!!}
+
+ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
+ex4 = {!!}
+
+subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y
+subst {A} {x} {y} f refl fx = fx
+
+-- ex5 :   {A : Set} {x y z : A } →  x == y → y == z → x == z
+-- ex5 {A} {x} {y} {z} x==y y==z = subst (λ refl  → {!!} ) x==y {!!}
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lambda.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,115 @@
+module lambda ( A B : Set) (a : A ) (b : B ) where
+
+--   λ-intro 
+--
+--      A
+--   -------- id
+--      A
+--   -------- λ-intro ( =  λ ( x : A ) → x )
+--    A → A 
+
+A→A : A → A 
+A→A = λ ( x : A ) → x
+
+A→A'' : A → A 
+A→A'' = λ x  → x
+
+A→A' : A → A 
+A→A' x = x
+
+lemma2 : (A : Set ) →  A → A   --  これは  A → ( A  → A ) とは違う
+lemma2 = ?
+
+lemma3 : {A B : Set } → B → ( A → B )  -- {} implicit variable
+lemma3  b = λ _ → b    -- _ anonymous variable
+
+-- λ-intro 
+--
+--    a :  A
+--     :              f : A → B
+--    b :  B 
+--  ------------- f
+--    A → B
+
+--   λ-elim
+--
+--     a : A     f : A → B
+--   ------------------------ λ-elim 
+--          f a :  B      
+
+→elim : A → ( A → B ) → B
+→elim a f = f a 
+
+ex1 : {A B : Set} → Set 
+ex1 {A} {B} = {!!} -- ( A → B ) → A → B
+
+ex2 : {A : Set} → Set 
+ex2 {A}  =  A → ( A  → A )
+
+proof2 : {A : Set } → ex2 {A}
+proof2 {A} = {!!} where
+  p1 : {!!}      --- ex2 {A} を C-C C-N する
+  p1 = {!!}
+
+ex3 :  A → B     -- インチキの例
+ex3 a = {!!}
+
+ex4 : {A B : Set} → A → (B → B)  -- 仮定を無視してる
+ex4 {A}{B} a b = b
+
+---           [A]₁               not used   --- a
+---         ────────────────────
+---                 [B]₂                    --- b
+---         ──────────────────── (₂)
+---             B → B
+---         ──────────────────── (₁)  λ-intro
+---              A → (B → B) 
+
+
+ex4' :  A → (B → B)   -- インチキできる / 仮定を使える
+ex4'  = {!!}
+
+ex5 : {A B : Set} → A → B → A
+ex5 = {!!}
+
+
+
+postulate
+  Domain : Set   --  Range Domain : Set
+  Range : Set    -- codomain     Domain → Range, coRange ← coDomain
+  r : Range 
+
+ex6 : Domain → Range
+ex6 a = {!!}
+
+
+---                   A → B
+--                     :
+---                   A → B
+---         ─────────────────────────── 
+---              ( A → B ) → A → B
+---
+---              [A]₁     [A → B ]₂
+---         ───────────────────────────  λ-elim
+---                    B
+---         ───────────────────────────  ₁
+---                   A → B
+---         ───────────────────────────  ₂
+---              ( A → B ) → A → B
+
+--
+--  上の二つの図式に対応する二つの証明に対応するラムダ項がある
+--
+ex11 : ( A → B ) → A → B
+ex11  = {!!}
+
+ex12 : (A B : Set) → ( A → B ) → A → B
+ex12 = {!!}
+
+ex13 : {A B : Set} → ( A → B ) → A → B
+ex13 {A} {B} = {!!}
+
+ex14 : {A B : Set} → ( A → B ) → A → B
+ex14 x = {!!}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/level1.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,25 @@
+module level1 where
+
+open import Level
+
+ex1 : { A B : Set} → Set
+ex1 {A} {B} =  A → B
+
+ex2 : { A B : Set} →  ( A → B ) → Set
+ex2 {A} {B}  A→B  =  ex1 {A} {B}
+
+ex7 : {A B : Set} → Set _
+ex7 {A} {B} = lemma2 ( A → B ) _ -- → A → B
+
+
+-- record FuncBad (A B : Set) : Set where
+--   field
+--      func : A → B → Set
+
+record Func {n : Level} (A B : Set n ) : Set (suc n) where
+  field
+    func :  A → B  → Set n
+
+record Func2 {n : Level} (A B : Set n ) : Set {!!} where
+  field
+    func : A → B  → Func A B
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/list.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,127 @@
+module list where
+                                                                        
+postulate A : Set
+
+postulate a : A
+postulate b : A
+postulate c : A
+
+
+infixr 40 _::_
+data  List  (A : Set ) : Set  where
+   [] : List A
+   _::_ : A →  List A → List A 
+
+--
+--                           A      List A
+--     -------------- []    ---------------- _::_
+--         List A               List A
+--
+
+infixl 30 _++_
+_++_ :   {A : Set } → List A → List A → List A
+[] ++ y = y
+(x :: x₁) ++ y = x :: (x₁ ++ y )
+
+l1 = a :: []
+l2 = a :: b  :: a :: c ::  []
+
+l3 = l1 ++ l2
+
+data Node  ( A : Set  ) : Set  where
+   leaf  : A → Node A
+   node  : Node A → Node A → Node A
+
+flatten :  { A : Set } → Node A → List A
+flatten ( leaf a )   = a :: []
+flatten ( node a b ) = flatten a ++ flatten b
+
+n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
+
+open  import  Relation.Binary.PropositionalEquality
+
+++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
+++-assoc A [] ys zs = let open ≡-Reasoning in
+  begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
+   ( [] ++ ys ) ++ zs
+  ≡⟨ refl ⟩
+    ys ++ zs
+  ≡⟨⟩
+    [] ++ ( ys ++ zs )
+  ∎
+  
+++-assoc A (x :: xs) ys zs = let open  ≡-Reasoning in
+  begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
+    ((x :: xs) ++ ys) ++ zs
+  ≡⟨ refl ⟩
+     (x :: (xs ++ ys)) ++ zs
+  ≡⟨ refl ⟩
+    x :: ((xs ++ ys) ++ zs)
+  ≡⟨ cong (_::_ x) (++-assoc A xs ys zs) ⟩ 
+    x :: (xs ++ (ys ++ zs))
+  ≡⟨ refl ⟩
+    (x :: xs) ++ (ys ++ zs)
+  ∎
+
+-- open import Data.Nat
+
+data Nat : Set where
+  zero : Nat 
+  suc  : Nat → Nat
+
+_+_ : Nat → Nat → Nat
+zero + y = y
+suc x + y = suc (x + y)
+
+sym1 : {A : Set} → {a b : A} → a ≡ b → b ≡ a
+sym1 {_} {a} {.a} refl = refl
+
+trans1 : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+trans1 {_} {a} {b} {.a} refl refl = refl
+
+cong1 : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b 
+cong1 f refl = refl
+
+induction : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x
+induction P initial induction-setp zero = initial
+induction P initial induction-setp (suc x) =  induction-setp x ( induction P initial induction-setp x)
+
+induction' : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x
+induction' P initial induction-setp x = {!!} where
+    ind1 : {!!} → P x
+    ind1 = {!!}
+
++-comm : {x y : Nat} → x + y ≡ y + x
++-comm {zero} {y} = sym1 lemma01  where
+   lemma01 : {y : Nat} → y + zero ≡ y
+   lemma01 {zero} = refl                               --      (zero + zero ) → zero → zero + zero ≡ zero
+   lemma01 {suc y} = cong1 (λ x → suc x) (lemma01 {y}) ---  (suc y + zero) ≡ suc y
+                               --   suc (y + zero) ≡ suc y  ← y + zero ≡ y 
++-comm {suc x} {y} = {!!}
+
+_*_ : Nat → Nat → Nat
+zero * y = zero
+suc x * y = y + (x * y)
+
+--
+--     * * *    * *
+--     * * *  ≡ * *
+--              * *
+
+*-comm : {x y : Nat} → x * y ≡ y * x
+*-comm = {!!}
+
+length : {L : Set} → List L →  Nat
+length [] = zero
+length (_ :: T ) = suc ( length T )
+
+lemma : {L : Set} → (x y : List L ) → ( length x + length y ) ≡ length ( x ++ y )
+lemma [] [] = refl
+lemma [] (_ :: _) = refl
+lemma (H :: T) L =  let open  ≡-Reasoning in
+  begin 
+     {!!}
+  ≡⟨ {!!} ⟩
+     {!!}
+  ∎
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,58 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding (_⇔_)
+open import Data.Empty
+
+
+data Bool : Set where
+   true : Bool
+   false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   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
+
+-- data ⊥ : Set where
+
+-- ⊥-elim : {n : Level} {A : Set n } → ⊥ → A
+--⊥-elim ()
+
+-- ¬_ : {n : Level } → Set n → Set n
+-- ¬ A = A → ⊥
+
+_⇔_ : {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 _⇔_
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/practice-logic.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,134 @@
+{-# 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} = {!!}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/practice-nat.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,118 @@
+module practice-nat where
+
+open import Data.Nat 
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality hiding (_⇔_)
+open import logic
+
+-- hint : it has two inputs, use recursion
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<> = {!!}  
+
+-- hint : use recursion
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡ = {!!}
+
+-- hint : use refl and recursion
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< = {!!}
+
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
+¬a≤a = {!!}
+
+-- hint : make case with la first
+a<sa : {la : ℕ} → la < suc la 
+a<sa = {!!}
+
+-- hint  : ¬ has an input, use recursion
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< = {!!}
+
+-- hint : two inputs, try nat-<>
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
+>→¬< = {!!}
+
+-- hint : make cases on all arguments. return case1 or case2
+-- hint : use with on suc case
+<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ = {!!}
+
+max : (x y : ℕ) → ℕ
+max = {!!}
+
+sum :  (x y : ℕ) → ℕ
+sum zero y = y
+sum (suc x) y = suc ( sum x y )
+
+sum' :  (x y : ℕ) → ℕ
+sum' x zero = x
+sum' x (suc y) = suc (sum' x y)
+
+sum-sym0 :  {x y : ℕ} → sum x y ≡ sum' y x
+sum-sym0 {zero} {zero} = refl
+sum-sym0 {suc x} {y} = cong (λ k → suc k ) (sum-sym0 {x} {y})
+sum-sym0 {zero} {y}  = refl
+
+sum-6 : sum 3 4 ≡ 7
+sum-6 = refl
+
+sum1 : (x y : ℕ) → sum x (suc y)  ≡ suc (sum x y )
+sum1 x y = let open ≡-Reasoning in 
+   begin 
+       sum x (suc y)
+   ≡⟨ {!!} ⟩
+       suc (sum x y )
+   ∎
+
+sum0 : (x : ℕ) → sum 0 x  ≡ x
+sum0 zero = refl
+sum0 (suc x) = refl 
+
+sum-sym : (x y : ℕ) → sum x y  ≡ sum y x
+sum-sym = {!!}
+
+sum-assoc : (x y z : ℕ) → sum x (sum y z ) ≡ sum (sum x y)  z 
+sum-assoc = {!!}
+
+mul :  (x y : ℕ) → ℕ
+mul x zero = zero
+mul x (suc y) = sum x ( mul x y )
+
+mulr :  (x y : ℕ) → ℕ
+mulr zero y = zero
+mulr (suc x) y = sum y ( mulr x y )
+
+mul-sym1 : {x y : ℕ } → mul x y ≡ mulr y x
+mul-sym1 {zero} {zero} = refl
+mul-sym1 {zero} {suc y} = begin
+     mul zero (suc y)
+   ≡⟨⟩
+     sum 0 (mul 0 y)
+   ≡⟨ cong (λ k → sum 0 k ) {!!}  ⟩
+      sum 0 (mulr y 0)
+   ≡⟨⟩
+     mulr (suc y) zero
+   ∎ where open ≡-Reasoning 
+mul-sym1 {suc x} {y} = {!!}
+
+mul-9 : mul 3 4 ≡ 12
+mul-9 = {!!}
+
+mul-distr1 : (x y : ℕ) → mul x (suc y) ≡ sum x ( mul x y )
+mul-distr1 = {!!}
+
+mul-sym0 : (x : ℕ) → mul zero x  ≡ mul x zero 
+mul-sym0 = {!!}
+
+mul-sym : (x y : ℕ) → mul x y  ≡ mul y x
+mul-sym = {!!}
+
+mul-distr : (y z w : ℕ) → sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
+mul-distr = {!!}
+
+mul-assoc : (x y z : ℕ) → mul x (mul y z ) ≡ mul (mul x y)  z 
+mul-assoc = {!!}
+
+evenp : (x : ℕ) → Bool
+evenp = {!!}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/record1.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,52 @@
+module record1 where
+
+record _∧_ (A B : Set) : Set where
+  field
+     π1 : A
+     π2 : B
+
+ex0 : {A B : Set} → A ∧ B →  A
+ex0 =  _∧_.π1 
+
+ex1 : {A B : Set} → ( A ∧ B ) → A 
+ex1 a∧b =  _∧_.π1 a∧b
+
+open _∧_
+
+ex0' : {A B : Set} → A ∧ B →  A
+ex0' =  π1 
+
+ex1' : {A B : Set} → ( A ∧ B ) → A 
+ex1' a∧b =  π1 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 B : Set} → A → ( A ∧ A ) 
+ex4 a  = record { π1 = {!!} ;  π2 = {!!} }
+
+ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
+ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} }
+
+--
+--                                 [(A → B ) ∧ ( B →  C) ]₁  
+--                                ──────────────────────────────────── π1
+--     [(A → B ) ∧ ( B →  C) ]₁        (A → B )    [A]₂
+--   ──────────────────────────── π2 ─────────────────────── λ-elim
+--          ( B →  C)                     B
+--   ─────────────────────────────────────────── λ-elim
+--                   C
+--   ─────────────────────────────────────────── λ-intro₂
+--                 A → C
+--   ─────────────────────────────────────────── λ-intro₁
+--     ( (A → B ) ∧ ( B →  C) )  → A → C
+
+ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
+ex6 x a = {!!}
+
+ex6' : {A B C : Set} →  (A → B ) → ( B →  C)   → A → C
+ex6' = {!!}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test.agda	Wed Nov 16 14:54:09 2022 +0900
@@ -0,0 +1,44 @@
+module test where
+
+open import Data.Nat
+
+a : ℕ
+a = 1 
+
+-- _*_ has precedence 7 over precedence 6 of _+_
+-- precedence of both defined in module Agda.Builtin.Nat
+
+-- _*_ has precedence 7 over precedence 6 of _+_
+-- precedence of both defined in module Agda.Builtin.Nat
+ex₁ : ℕ
+ex₁ = 1 + 3 * 4
+
+-- Propositional equality and some related properties can be found
+-- in Relation.Binary.PropositionalEquality.
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+ex₂ : 3 + 5 ≡ 2 * 4
+ex₂ = refl
+
+
+open import Data.Nat.Properties using (*-comm; +-identityʳ)
+
+ex₃ : ∀ m n → m * n ≡ n * m
+ex₃ m n = *-comm m n
+
+induction : (P : (x : ℕ ) → Set) 
+   → (initial : P zero ) 
+   → (induction-step : ((x : ℕ) → P x → P (suc x))) 
+   → (x : ℕ) → P x
+induction P initial induction-step = ?
+
+test1 : (n : ℕ) → n + 0 ≡ n 
+test1 n = induction  (λ n → n + 0 ≡ n) t1 t2 n where
+    cong : {N : Set } →  (f : N → N ) → { x y : N } → x ≡ y → f x ≡ f y
+    cong f refl = refl
+    t1 :  (zero + 0 ≡ zero)
+    t1 = refl
+    t2 : (x : ℕ) → x + 0 ≡ x → suc x + 0 ≡ suc x
+    t2 x eq = cong suc eq
+