Blaisorblade

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Import GRing.Theory.
Open Scope ring_scope.

Section foo.
(* Variant of the same problem. *)
(* Variable R: numFieldType. *)

Blaisorblade

rom mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Import GRing.Theory.
Open Scope ring_scope.

Section foo.
Variable R: numFieldType.

Definition T:= R.

Blaisorblade

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Open Scope ring_scope.

Import  GRing.Theory.

Variable R: numFieldType.

Definition rt :

Blaisorblade

import scala.compiletime._
final case class Col[Key, Value](data: Array[Value])
object Frame {
  // Covariant version of Tuple.Elem
  /** Type of the element a position N in the tuple X */
  type Elem[+X <: Tuple, +N <: Int] = X match {
    case x *: xs =>
      N match {
        case 0 => x
        case S[n1] => Elem[xs, n1]

Blaisorblade

From iris.heap_lang Require Import proofmode.

(** * Superseded by stdpp master. *)
Instance set_unfold_copset_top x : SetUnfoldElemOf x (⊤ : coPset) True.
Proof. by constructor. Qed.

(** * More reusable building blocks *)
(** Support writing external hints for lemmas that must not be applied twice for a goal. *)
(* The usedLemma and un_usedLemma marker is taken from Crush.v (where they were called done and un_done). *)

Blaisorblade

//package test

import scala.language.higherKinds

object CT {
    trait Category[Obj[_],C[_,_]] { // Obj is the value representation of objects, C the type representation of morphisms
        def id[A:Obj]: C[A,A]
        def compose[X:Obj,Y:Obj,Z:Obj](f: C[Y,Z], g: C[X,Y]): C[X,Z]
    }

Blaisorblade

import scala.quoted._
import scala.quoted.staging.{run, Toolbox}

trait Lambda[Rep[_], Cons[_]] {
  def lam[A: Cons, B: Cons](f: Rep[A] => Rep[B]): Rep[A => B]
  def app[A: Cons, B: Cons](f: Rep[A => B], repA: Rep[A]): Rep[B]
}
// Boilerplate exposing Lambda's methods to the top-level, hopefully can be improved upon.
def lam[Rep[_], Cons[_], A: Cons, B: Cons](f: Rep[A] => Rep[B])(given l: Lambda[Rep, Cons]): Rep[A => B] = l.lam(f)
def app[Rep[_], Cons[_], A: Cons, B: Cons](f: Rep[A => B], repA: Rep[A])(given l: Lambda[Rep, Cons]): Rep[B] =

Blaisorblade

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool seq tuple.
Import EqNotations.

Lemma sig_bool_eq {A : Type} {P : A -> bool} (x y: {z | P z}): sval x = sval y -> x = y.
Proof.
  case: x y => [x Px] [y Py] /= Hxy; destruct Hxy.
  apply eq_exist_uncurried. exists (Logic.eq_refl _).
  apply bool_irrelevance.
Qed.

Blaisorblade

From stdpp Require Import tactics.

(** Create an [f_equiv] database, inspired by stdpp's [f_equal] database. We
don't restrict it to [(_ ≡ _)], because [f_equiv] can apply [Proper]
instances to any relation. Use with lots of care. *)
Hint Extern 998 => f_equiv : f_equiv.

(* Override stdpp's [f_equiv], raising maximum arity from 5 up to 7. *)
Ltac f_equiv ::=
  match goal with

Blaisorblade

How to deal with quotients or setoids?

Lean

Lean extends the Calculus of Inductive Constructions with quotient types, as discussed by Carneiro (2019, Sec 2.7.1). However, that and other choices break some metatheoretic properties of CIC (Carneiro, 2019, Sec. 3.1), properties that Coq developers care about; consistency is nevertheless preserved.

Coq

Coq does not add support for quotients; one must instead use setoids explicitly. By looking at Carneiro (2019), we can see the difference: unlike quotient A/R, a setoid (A, R) is not a standard type, and we must explicitly remember to use R instead of standard equality wherever needed. Both with setoids and quotients, we must ensure that functions respect the equivalence on their domain. However, when using quotients A/R, that must only be checked for functions that use A/R's eliminator, while with setoids we need more work. For example, take a function f : A/R -> B, and g : B -> C: we can