jespercockx

open import Haskell.Prelude hiding (coerce; a; b; c; _,_; _,_,_)
open import Haskell.Extra.Erase
open import Haskell.Extra.Refinement
open import Scope
open import Utils

module STLC {@0 name : Set} where

private variable

jespercockx

/* Canonical Dedukti in LambdaPi

   An encoding of (my interpretation of) "Canonical Dedukti" by Thiago Felicissimo in LambdaPi

   All credit goes to Thiago, all blame goes to me
   -- Jesper, 2022-10-19
*/

/* syntactic classes */

jespercockx

-- This is an alternative solution to the problem discussed in the video https://www.youtube.com/watch?v=WplTbki3gCg

{-# LANGUAGE RankNTypes, StandaloneDeriving, DeriveAnyClass, TypeApplications, ScopedTypeVariables, GADTs #-}

import Data.Scientific
import Type.Reflection

data AnyRealFloat = AnyRealFloat (forall a. RealFloat a => a)

instance Eq AnyRealFloat where

jespercockx

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Unit

open import Function

open import Reflection
open import Reflection.TypeChecking.Monad.Syntax

jespercockx

open import Data.List.Base

open import Data.Bool
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Unit

jespercockx

--{-# OPTIONS -v any-auto:10 #-}

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties using
  (singleton⁺; map⁺; mapMaybe⁺; ++⁺ˡ; ++⁺ʳ; concat⁺)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
open import Data.Nat using (ℕ; zero; suc; _+_)

jespercockx

{-# OPTIONS --rewriting #-}

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Product using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality

Π : (A : Set) (B : A → Set) → Set
Π A B = (x : A) → B x

jespercockx

open import Agda.Primitive

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.List.Base
open import Data.Product using (_×_; _,_; proj₁; proj₂)
import Data.String.Base as String
open import Data.Unit.Base
open import Function using (id; _∘_)

jespercockx

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Equality

_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
    → (f : {x : A} (y : B x) → C y) (g : (x : A) → B x)
    → (x : A) → C (g x)
(f ∘ g) x = f (g x)

_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x

jespercockx

How to formalize stuff in Agda

Preliminaries

For this presentation, we keep the dependencies to a minimum.