Functional Programming 2021/22 fall

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