Skip to content

Latest commit

 

History

History
178 lines (147 loc) · 6.27 KB

Day4a.org

File metadata and controls

178 lines (147 loc) · 6.27 KB

Imports and such

module Day4a

import System.File
import Data.Strings
import Data.Either
import Data.List
import Data.List.Quantifiers
import Data.List.Elem
import Decidable.Equality
import Data.Void
import Data.Nat
import Data.Nat.Order
import Decidable.Decidable
import Decidable.Order
import Data.String.Parser
import Data.Fin
import Data.Fin.Extra

%default total

Datatypes Describing the Solution

Represent Fields as finite numbers

Key : Type
Key = Fin 8

Cid : Key
Cid = FZ

Helpful Decision Procedure

It says that if we can decide a property for each finite number, we can decide whether it holds for all members of Fin n. I should probably add this to the contrib branch of the stdlib.

Our helper lemma:

natToFinLTE : (n : Nat) -> LTE (S n) m -> Fin m
natToFinLTE n = weakenLTE (last {n})

natToFinToNat :
  (n : Nat)
  -> (lte : LTE (S n) m)
  -> finToNat (natToFinLTE n lte) = n
natToFinToNat 0 (LTESucc lte) = Refl
natToFinToNat (S k) (LTESucc lte) = rewrite natToFinToNat k lte in Refl
-- natTOFinToNat n = ?nfn

-- lteDichotomy :

helper1 :
  {P : (Fin (S n1) -> Type)}
  -> P FZ
  -> (x : Fin (S n1))
  -> LTE (finToNat x) 0
  -> P x
helper1 pf FZ LTEZero = pf
-- helper1 (LTESucc y) _ impossibl

helper2 :
   {0 n1 : Nat}
   -> {P : Fin (S n1) -> Type}
   -> (bound' : Nat)
   -> (bounded : LTE (S bound') n1)
   -> P (FS $ natToFinLTE bound' bounded)
   -> ((x : Fin (S n1)) -> LTE (finToNat x) bound' -> P x )
   -> (x : Fin (S n1)) -> LTE (finToNat x) (S bound') -> P x
helper2 bound' bounded prf rec x lte with (isLTE (finToNat x) bound')
  helper2 bound' bounded prf rec x lte | Yes lte2 = rec _ lte2
  helper2 bound' bounded prf rec x lte | No nlte = rewrite eq in prf
    where
       natEq : finToNat x = S bound'
       natEq = LTEIsAntisymmetric _ _  lte (notLTEImpliesGT nlte)
       eq : x = (FS $ natToFinLTE bound' bounded)
       eq  = finToNatInjective _ _ $ trans natEq $ cong S (sym $ natToFinToNat _ _)


boundedFiniteDec :
  {0 n : Nat}
  -> {P : Fin n -> Type}
  -> (bound : Nat)
  -> (boundBounded : LTE (S bound) n)
  -> (Dec  (P (natToFinLTE bound boundBounded)) )
  -> ((x : Fin n) -> Dec (P x))
  -> Dec ((x : Fin n) -> LTE (finToNat x) bound -> P x )
boundedFiniteDec {  n = n} bound boundBounded (No contra) ddec =
  No $ \f => contra (f _ $ rewrite natToFinToNat bound boundBounded in lteRefl)
boundedFiniteDec {  n = S n1} 0 (LTESucc _) (Yes prf) ddec = Yes $ helper1 prf
boundedFiniteDec {  n = S n1} (S bound') (LTESucc lte) (Yes prf) ddec
  with (  boundedFiniteDec {  n = S n1} bound' (lteSuccRight lte) (ddec _) ddec)
  boundedFiniteDec {  n = S n1} (S bound') (LTESucc bounded) (Yes prf) ddec | No nrec =
    No $ \ f => nrec $ \x, lte => f _ (lteSuccRight lte)
  boundedFiniteDec {  n = S n1} (S bound') (LTESucc bounded) (Yes prf) ddec | Yes rec =
    Yes $ helper2 bound' bounded prf rec

record BoundedEx {n : Nat} (bound : Nat) (P : Fin n -> Type) where
  constructor BndEx
  {bndWitness : Fin n}
  0 bndLTE : LTE (finToNat bndWitness) bound
  bndPf : P bndWitness

boundedFiniteEx :
    {0 n : Nat}
    -> {P : Fin n -> Type}
    -> (bound : Nat)
    -> (boundBounded : LTE (S bound) n)
    -> (Dec  (P (natToFinLTE bound boundBounded)) )
    -> ((x : Fin n) -> Dec (P x))
    -> Dec (BoundedEx bound P)
boundedFiniteEx {n = n} bound boundBounded (Yes pf) ddec =
  Yes $ BndEx (rewrite natToFinToNat bound boundBounded in lteRefl) pf
boundedFiniteEx {n = S n1} 0 (LTESucc bounded)(No npf) ddec = No $ \bnd => helper (bndLTE bnd) (bndPf bnd)
  where
      helper : {x : Fin (S n1)} -> (0 _ : LTE (finToNat x) 0) -> P x -> Void
      helper {x = FZ} LTEZero pf = npf pf
boundedFiniteEx {n = S n1} (S bound') (LTESucc lte) (No npf) ddec with (boundedFiniteEx {  n = S n1} bound' (lteSuccRight lte) (ddec _) ddec)
  boundedFiniteEx {n = S n1} (S bound') (LTESucc lte) (No npf) ddec | Yes bnd =
    Yes $ BndEx (lteSuccRight $ bndLTE bnd) (bndPf bnd)
  boundedFiniteEx {n = S n1} (S bound') (LTESucc lte) (No npf) ddec | No rec =
    No \ bnd =>  void $ helper (bndLTE bnd) (bndPf bnd)
    where
      helper : {x : Fin (S n1)} ->  LTE (finToNat x) (S bound') -> P x -> Void
      helper {x = x} xlte px with (isLTE (finToNat x) bound')
        helper {x = x} xlte px | Yes blte = rec $ BndEx blte px
        helper {x = x} xlte px | No nlt = npf $ (rewrite (sym eq) in px)
          where
            eq : x = (FS $ natToFinLTE bound' lte)
            eq  = finToNatInjective _ _  $ trans (LTEIsAntisymmetric _ _  xlte (notLTEImpliesGT nlt)) $ cong S (sym $ natToFinToNat _ _)

The decision procedure itself

finiteDecEx : {k : Nat} -> {P : Fin k -> Type} -> ((x : Fin k) -> Dec (P x)) -> Dec (x : Fin k ** P x)
finiteDecEx {k = 0} dec = No $ \ pr => absurd (fst pr)
finiteDecEx {k = (S n1)} dec
  with (boundedFiniteEx (finToNat last) (elemSmallerThanBound (last {n = n1})) (dec _) dec)
  finiteDecEx {k = (S n1)} dec | Yes bnd = Yes (bndWitness bnd ** bndPf bnd)
  finiteDecEx {k = (S n1)} dec | No nbnd = No $ \ pr => nbnd $ BndEx lessThanLast (snd pr)
    where
      lessThanLast : {x : Fin (S n1)} -> LTE (finToNat x) (finToNat (last {n = n1} ))
      lessThanLast {x} =
        rewrite finToNatLastIsBound {n = n1}
        in fromLteSucc $ elemSmallerThanBound x

finiteDec : {n : Nat} -> {P : Fin n -> Type} -> ((x : Fin n) -> Dec (P x)) -> Dec ((x : Fin n) -> P x)
finiteDec {n = Z} dec = Yes $ \ x => absurd x
finiteDec {n = S n1} dec with (boundedFiniteDec (finToNat last) (elemSmallerThanBound (last {n = n1})) (dec _) dec)
    finiteDec {n = S n1} dec | Yes pf =
      Yes $ \ x => pf x $ rewrite finToNatLastIsBound {n = n1} in fromLteSucc $ elemSmallerThanBound _
    finiteDec {n = S n1} dec | No npf = No $ \f => npf $ \ x, lte => f x

Predicate for whether a list has all mandatory keys

-- HasAllKeys : List Key -> Type
-- HasAllKeys l = (k : Key) -> Either (k = Cid) (Elem k l)

It’s decidable whether a list has a given key



It’s decidable whether a list has all mandatory keys