msakai

import numpy as np
import scipy.linalg

import pivots


def factor(A, B, C):
    """
    factor(A, B, C)(D) compute LU factorization of
    X = (A B)

msakai

# numpy/scipy translation of https://github.com/locuslab/qpth/blob/5485219028a7687b76107c8431625aaedfd7bc36/qpth/solvers/pdipm/single.py

import numpy as np
import scipy
import scipy.linalg

# TODO: Add more comments describing the math here.
# https://stanford.edu/~boyd/papers/pdf/code_gen_impl.pdf

msakai

{-# OPTIONS --with-K #-}
module JM where

open import Level

infix 4 _≅_

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
  ≅-refl : x ≅ x

msakai

diff --git a/cmake/MKL.cmake b/cmake/MKL.cmake
index 57acaab..b7fc063 100644
--- a/cmake/MKL.cmake
+++ b/cmake/MKL.cmake
@@ -169,7 +169,7 @@ detect_mkl("mkl_rt")
 if(HAVE_MKL)
     add_definitions(-DUSE_MKL -DUSE_CBLAS)
     include_directories(AFTER ${MKLINC})
-    list(APPEND mkldnn_LINKER_LIBS ${MKLLIB})
+#    list(APPEND mkldnn_LINKER_LIBS ${MKLLIB})

msakai

module ImplyL2 where

{-
B→C,Γ ⊢ A→B    C,Γ ⊢ G
---------------------- (→L2)
(A→B)→C,Γ ⊢ G

c.f.
https://www.slideshare.net/qnighy/proving-decidability-of-intuitionistic-propositional-calculus-on-coq
-}

msakai

module TerminatingLJ where

import Data.Set (Set)
import qualified Data.Set as Set
import Debug.Trace

data Expr a
  = Atom a
  | Bottom
  | Expr a :-> Expr a

msakai

From mathcomp Require Import eqtype ssreflect seq ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Definition disj (xs : seq bool) := true \in xs.

Theorem disj_split (xs : seq bool) (ys : seq bool)
  :   disj (xs ++ ys)

msakai

From mathcomp Require Import ssreflect fintype finset seq ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(******************************************************************************

Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.

Checked with Coq 8.8.0 and MathComp 1.7.0.

msakai

module DeMorgan where

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Function
open import Relation.Nullary

¬¬-elim⇒call/cc
  : (∀ {p} {P : Set p} → ¬ ¬ P → P)

msakai

(* infotheo Extension for Capacities of Channels
   (c) Chiba Univ. K. Nakano, M. Hagiwara.
   GNU GPLv3. *)
From mathcomp
Require Import ssreflect ssrbool eqtype fintype bigop.
Require Import Fourier.
(*
From Infotheo
Require Import Reals_ext ssr_ext Rssr proba entropy Rbigop
               log2 binary_entropy_function.