AlecsFerra

Local Definitions Proposal

The Issue

Suppose we are working with the following Liquid Haskell code:

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--reflection" @-}

AlecsFerra

nix-shell -p "python3.withPackages (ps: with ps; [ dbus-python distro ])" --run "python3 <your-eduroam.py>"

AlecsFerra

#! /usr/bin/env python3

# flatten.py
# Copyright (C) 2024 Alessio Ferrarini <github.com/alecsferra>
# 
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
# 

AlecsFerra

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import Text.Printf (printf)

AlecsFerra

module AxiomK where

open import Relation.Binary.PropositionalEquality using (_≡_)
open _≡_

-- All the equality proofs are the same ⁾
-- Unless we use the `--without-K` option ⁾
same-≡ : ∀ {l} {A : Set l} {a b : A} → (p₁ p₂ : a ≡ b) → p₁ ≡ p₂
same-≡ refl refl = refl

AlecsFerra

module RewriteAbuse where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite (sym (+-assoc m n p))
             |       (+-comm m n)
             |       (+-assoc n m p)

AlecsFerra

;; Some proofs about pairs
;; ∀ a b c. a = b → (a, c) = (b, c)
(claim a=b→ac=bc
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [_ (= T a b)])
    (= (Pair T K) (cons a c) (cons b c))))

AlecsFerra

; last
(claim last
  (Π ((Of U)
      (many-1 Nat)
      (vec (Vec Of (add1 many-1))))
    Of))
(define last
  (λ (Of many-1 vec)
    ((ind-Nat many-1
      (λ (many-1)

AlecsFerra

Keybase proof

I hereby claim:

• I am alecsferra on github.
• I am alecsferra (https://keybase.io/alecsferra) on keybase.
• I have a public key ASAJE6eEkoGFeGf_LAF1ZhaduDhazfmJRUIMvemvGYDItQo

To claim this, I am signing this object:

AlecsFerra

print("""
main = do
    print "Welcome to my addition calculator :)"
    a <- getLine
    b <- getLine
    print $ add (read a) (read b)
""")

for i in range(1000):
    for j in range(1000):