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