roboguy13

(* NOTE: S means successor. So, "S a" means successor of a (aka a+1) *)
Lemma S_add_left :
  forall (a b : nat),
  S (a + b) = a + S b. (* This is the proposition, given as a type. This is the type signature for the lemma *)
Proof.
  (* I am using the tactic language here. Internally this generates an expression that has the type above *)
  intros. (* Bring the variables a and b into scope *)
  destruct a  (* "destruct" is similar to induction, but it does not give you an inductive hypothesis *)
    ; easy. (* "easy" is a builtin tactic that can solve very simple proof goals. The semicolon means to apply it to all subgoals generated by the previous command *)
Qed.

roboguy13

module ModalIntuitionistic
  where

data Prop
  = V String
  | Not Prop
  | And Prop Prop
  | Or Prop Prop
  | Prop :=> Prop
  | Box Prop

roboguy13

(* https://twitter.com/codydroux/status/1570158204243288066 *)

Section Iter_to_ind.

  Variable B : Prop.
  Variable F : Prop -> Prop.

  (* F is a monad *)
  Variable fmap : forall (a b : Prop), (a -> b) -> F a -> F b.
  Variable pure : forall (a : Prop),   a -> F a.

roboguy13

-- GHCi example:
--   ghci > mempty @(Permutation (Nx (Nx (Nx Zr))) Int)
--   Perm ((:++) 0 ((:++) 1 ((:++) 2 EmptyVec)))

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

roboguy13

class Budget {
    var days : array<int>
    var weeks : array<int>

    function valid() : bool
        reads this, weeks, days
    {
        days.Length == weeks.Length &&
            (forall i :: 0 <= i < days.Length ==> (weeks[i] == 7 * days[i]))
    }

roboguy13

Require Import Coq.Logic.FinFun.

Theorem the_theorem
  : ~ exists (f : unit -> bool), Surjective f.
Proof.
  intro H.
  destruct H.
  destruct (H true).
  destruct (H false).
  destruct x0, x1.

roboguy13

{-# LANGUAGE Strict #-}

{-# OPTIONS_GHC -O3 #-}

import           Data.Complex
import           Control.Applicative
import           Control.Arrow
import           Control.Monad

main :: IO ()

roboguy13

Inductive Eq : Type -> Type :=
  | MkEq : forall a, (a -> a -> bool) -> Eq a.

Definition my_equal {e b c : Type} {t : Type -> Type} (dict : Eq e) (f : forall a, t a -> e) (x : t b) (y : t c) : bool.
  destruct dict as [T eq].
  exact (eq (f b x) (f c y)).
Defined.

roboguy13

{-# LANGUAGE RankNTypes #-}

exampleA :: [a] -> [a]
exampleA = reverse

exampleB :: [Int] -> [Int]
exampleB = filter even

rank2 :: (forall a. [a] -> [a]) -> [Char]
rank2 f = f "abc"

roboguy13

-- This works
--   recoverF_CPS everyP (f (A 1)) B'
-- and so does
--   recoverF_CPS (Proxy :: Proxy ((~) Char)) (\x -> case x of A _ -> 'a'; B -> 'b') (A' 1)
-- But this isn't allowed to type check:
--   recoverF_CPS everyP (f B) B'

-- Also note this law holds:
--   recoverF_CPS everyP recoverF' = id