Funktsionaalprogrammeerimine 2022/23 sügis

Kodutöö 10

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

 app : (a->b) -> a
       ----------- 
    ->      b

Implikatsiooni sissetoomse (ehk {$\lambda$}-abstraktsiooni) reegel võtab implikatsiooni a->b ja eelduse a ning annab välja b

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

Need reeglid on sisse ehitatud -- definitsioone me anda ei saa (ja ei pea).

Kõik teised konstruktsioonid saame sisse tuua data abil loodud andmestruktuuridega. 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

-- 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 uut teoreemi (nagu idVec loengust) tõestama.

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