Funktsionaalprogrammeerimine 2024/25 sügis

Kodutöö 12

Tõestused Idris2-s. NB! Koodi sees on mitmed väikesed ülesanded.

Lausearvutus

Idris-e loogika aluseks on keelde sisse ehitatud implikatsion (ehk funktsioonitüüp).

Implikatsiooni väljaviimise (ehk funktsiooni rakenduse) reegel võtab implikatsiooni a->b ja eelduse a ning annab välja b

 ?f ?x : (a->b) -> a
         ----------- 
      ->      b

Implikatsiooni sissetoomse (ehk {$\lambda$}-abstraktsiooni) reegli järgi saame järeldada implikatsiooni a->b -- eeldusel, et saame näidata b kui meile on antud a.

 (\ x => ?y) :   a
                 .
                 .
                 .
                 b
               ------
          ->   a -> b

Reegli nime asemel kasutame vastavalt funktsioonirakendust või funktsiooni defineerimise süntaksit.

Kõik teised konstruktsioonid saame sisse tuua data abil loodud andmestruktuuridega, mille kontruktoriteks on sissetoomise reeglid.

Esmalt on ülesandeks kontrollida, kas väljaviimise reeglid on Idrises tuletatavad.

Konjunktsioon

-- ainult täielikud funktsioonid tagavad turvalisuse
%default total  

infixl 10 /\
data (/\) : Type -> Type -> Type where
    ConI : a -> b 
           ------
        -> a /\ b

-- Väljaviimise reegleid ise defineerima ei pea aga saame nende paikapidavust kontrollida.
conEl : a /\ b
        ------
     ->   a

-- Reegel kehtib, kui saame anda definitsiooni.
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 kehtib kummaliselt kõlav väide: 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õrduste teooria 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 tõestama uut teoreemi, nagu idVec sõltuvat tüüpide loengus.)

Võrduse väljaviimiseks on rewrite .. in .. reegel.

  rewrite .. in .. : a=b -> Pb 
                     ----------
                 ->     Pa

S.t. kui meil on vaja tõestada S (n+0) = S n ja me teame võrdust eq: n+0 = n siis rewrite eq asendab eesmärgis n+0-d n-dega. Jääb tõestada S n = S n.

Muide, rewrite-i saab ka ise implementeerida, aga seda on ebamugavam kasutada. Idrise sisseehitatud rewrite suudab P ise tuletada aga myrewrite puhul on vaja see argumendiks anda.

myrewrite : (p:a -> Type) -> {x:a} -> {y:a} -> x=y -> p y -> p x
myrewrite p Refl h = h

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