Praktikum 11
Tõestused Idris2-s. NB! Koodi sees on mitmed väikesed ülesanded.
Lausearvutus
data
abil loodud andmestruktuuridega
saame lisada uusi loogika-reegleid, kus
kontruktoriteks on sissetoomise reeglid.
Konjunktsioon
-- ainult täielikud funktsioonid tagavad turvalisuse %default total infixl 10 /\ data (/\) : Type -> Type -> Type where ConI : a -> b ------ -> a /\ b -- Lisaks võime (aga ei pea) funktsioonidena -- defineerida väljaviimise reeglid conEl : a /\ b ------ -> a -- ... mille väärtus on leitud mustrisobituse abil. conEl = ?conEl_v conEr : a /\ b ------ -> b conEr = ?conEr_v
Disjunktsioon
infixl 11 \/ data (\/) : Type -> Type -> Type where DisjIl : a ------ -> a \/ b DisjIr : b ------ -> a \/ b disjE : (a\/b) -> (a -> c) -> (b -> c) ---------------------------------- -> c disjE x f g = ?disjE_v
Eitus ja väärus
%hide Not -- juba std. teegis olemas data Not : Type -> Type where NotI : (a -> Void) ----------- -> Not a NotE : Not a -> a ---------- -> Void NotE x = ?NotE_v --data Void : Type where ---- meelega jäetud tühjaks VoidE : Void ---- -> b VoidE q impossible
Lausearvutuse ülesanne ex1
ex1 : a /\ (b -> c) /\ (a -> b) ------------------------- -> c ex1 = ?ex1_v
Kalmeri lemmikväide:
Klassikalises loogikas a "põhjustab" b-d või b "põhjustab" a-d -- iga a ja b korral. (Näiteks a:="Täna on reede", b:="vihma sajab".)
--(Vihje: kasuta lambdat) ex2 : a \/ Not a -------------------- -> (a -> b) \/ (b -> a) ex2 a = ?ex2_v
Paaris
Mingi oma teooria lisamiseks tuleb defineerida data
vastavate aksioomidega.
Näiteks teooria paarisarvudest.
data Even : Nat -> Type where Even_Zero : -------- Even 0 Even_Succ : Even n ------------ -> Even (2+n) even4 : Even 4 even4 = ?even4_v even8 : Even 8 even8 = ?even8_v plusEvenEven : Even n -> Even m ------------------ -> Even (n+m) plusEvenEven a b = ?plusEvenEven_v multEvenEven : Even n -> Even m ------------------ -> Even (n*m) multEvenEven a b = ?multEvenEven_v
Paaris/Paaritu
data Odd : Nat -> Type where Odd_one : -------- Odd 1 Odd_Succ : Odd n ----------- -> Odd (2+n) odd7 : Odd 7 odd7 = ?odd7_v evenOdd : Even n ---------- -> Odd (1+n) evenOdd e = ?evenOdd_v plusOddOdd : Odd n -> Odd m ------------------- -> Even (n+m) plusOddOdd a b = ?plusOddOdd_v plusEvenOdd : Even n -> Odd m ------------------- -> Odd (n+m) plusEvenOdd a b = ?plusEvenOdd_v plusNullOdd : Odd m ------------ -> Odd (m+0) plusNullOdd a = ?plusNullOdd_v
Võrdused ja rewrite
Võrdus on standardteegis defineeritud põhimõtteliselt nii:
data (=) : Type -> Type -> Type where Refl : {a:Type} ---------- -> a = a
Nii saame defineerida üldisi võrdusi ja ei pea enam iga kasutuse jaoks uut teoreemi (nagu idVec
loengust) tõestama.
Näidis
Proovi ka ise seda lahendada, et aru saada, kuidas rewrite töötab.
plusNull : (n:Nat) --------- -> n+0 = n plusNull 0 = Refl plusNull (S k) = rewrite plusNull k in Refl
Ülesanne: liitmise assotsiatiivsus
Kasuta rewrite-i.
plusAssoc : (m:Nat) -> (n:Nat) -> (q:Nat) ------------------------------ -> m + (n + q) = (m + n) + q plusAssoc m n q = ?plusAssoc_v
Tärnülesanne: multOddOdd
-- Vihjed: case-split a ja b (tuleb kolm juhtu) -- Esimene juht on triviaalne, teised vajavad natuke vaeva. -- -- Märkus: Idrise poolt genereeritud 2+n asemel tuleb -- käsitsi panna S (S n) selleks, et muutuja n oleks kättesaadav. multOddOdd : (n:Nat) -> (m:Nat) -> Odd n -> Odd m ------------------------------------------- -> Odd (n*m) multOddOdd n m a b = ?multOddOdd_v