gistfile1.idr

import Prelude.Vect

%default total

sumPairs : Vect (S n) Nat -> Vect n Nat
sumPairs (h1 :: h2 :: tl) = (h1 + h2) :: sumPairs (h2 :: tl)
sumPairs [h]              = []

-- try to show how non-top-level pattern matching won't work

snoc : Vect n a -> a -> Vect (S n) a
snoc [] a       = [a]
snoc (h :: t) a = h :: snoc t a

next : Vect n Nat -> Vect (S n) Nat
next []       = [1]
next [_]      = [1, 1]
next (h :: t) = snoc (1 :: sumPairs (h :: t)) 1

codata Triangle : a -> Nat -> Type where
  triangle : (n : Nat) -> Vect n a -> Triangle a (S n) -> Triangle a n

pascal_triangle_aux : (n : Nat) -> Vect n Nat -> Triangle Nat n
pascal_triangle_aux n v = triangle n v (pascal_triangle_aux (S n) (next v))

pascal_triangle : Triangle Nat Z
pascal_triangle = pascal_triangle_aux Z []

-- show how (n + step) part effects inference
pascal_triangle_row_aux : (step : Nat) -> Triangle Nat n -> Vect (n + step) Nat
pascal_triangle_row_aux Z         (triangle n v _)    ?= {pf1} v
pascal_triangle_row_aux (S step') (triangle _ _ next) ?= {pf2} pascal_triangle_row_aux step' next

lt_down : (a : Nat) -> (b : Nat) -> LTE (S (S a)) (S b) -> (LTE (S a) b)
lt_down _ _ a = ?lts_lt

natToFin_bounded : (a : Nat) -> (b : Nat) -> (pf : LTE (S a) b) -> Fin b
natToFin_bounded Z Z lteZero impossible
natToFin_bounded (S _) Z lteZero impossible
natToFin_bounded Z (S n) pf = fZ
natToFin_bounded (S a) (S b) pf = fS (natToFin_bounded a b (lt_down _ _ pf))

pascal_nth : (row : Nat) -> (col : Nat) -> (pf : LT col row) -> Nat
pascal_nth row_idx col_idx pf = index f row
  where
    row : Vect row_idx Nat
    row = pascal_triangle_row_aux row_idx pascal_triangle

    f : Fin row_idx
    f = natToFin_bounded col_idx row_idx pf

toLTE : (a : Nat) -> (b : Nat) -> (pf : a <= b = True) -> LTE a b
toLTE Z Z _ = lteZero
toLTE Z (S _) _ = lteZero
toLTE (S _) Z refl impossible
toLTE (S a) (S b) pf = ?toLTE4

---------- Proofs ----------

Main.pf1 = proof
  intros
  rewrite sym (plusZeroRightNeutral n)
  refine value

Main.pf2 = proof
  intros
  rewrite (plusSuccRightSucc n step')
  refine value

Main.lts_lt = proof
  intros
  refine fromLteSucc
  exact a1