Skip to content

Instantly share code, notes, and snippets.

Paolo G. Giarrusso Blaisorblade

Block or report user

Report or block Blaisorblade

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@Blaisorblade
Blaisorblade / stagingHoas.scala
Last active Jan 30, 2020
Abstracting over Type[_] constraints needed for staging in Dotty (answering https://gitter.im/lampepfl/dotty?at=5e33235c3aca1e4c5f4d2aec)
View stagingHoas.scala
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
Blaisorblade / int_eq.v
Last active Jan 28, 2020
How to prove equality of sigma types with decidable predicates
View int_eq.v
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.
View flip_proper.v
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
View Lean-vs-Coq-setoids-quotients.md

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

View mwe-lmodern-fontenc.tex
\documentclass{article}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\title{Hi}
\begin{document}
\maketitle
\end{document}
@Blaisorblade
Blaisorblade / try_once.v
Last active Dec 4, 2019
How to add Coq automation hints that can't be applied twice (for e.g. transitivity)
View try_once.v
(** 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). *)
(** Devious marker predicate to use for encoding state within proof goals *)
Definition usedLemma {T : Type} (x : T) := True.
(** After a round of application with the above, we will have a lot of junk [usedLemma] markers to clean up; hence this tactic. *)
Ltac un_usedLemma :=
repeat match goal with
| [ H : usedLemma _ |- _ ] => clear H
View iModMasks.v
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Global Instance elim_modal_fupd_fupd_mask_frame_empty `{BiFUpd PROP} p E1 E1' E3 P Q :
ElimModal (E1 ⊆ E1') p false (|={E1,∅}=> P) P
(|={E1',E3}=> Q) (|={E1'∖E1,E3}=> Q) | 2.
Proof.
@Blaisorblade
Blaisorblade / foo.scala
Last active Jan 3, 2020
Running showExtractors in Dotty 0.20.0-RC1 REPL
View foo.scala
scala> import scala.quoted._
scala> import scala.quoted.staging._
scala> run[Int]{(given qctx) => { import qctx.tasty.{_, given}; println(('{1}).unseal.showExtractors); '{1}}}
1 |run[Int]{(given qctx) => { import qctx.tasty.{_, given}; println(('{1}).unseal.showExtractors); '{1}}}
| ^
|Could not find implicit scala.quoted.staging.Toolbox.
|
|Default toolbox can be instantiated with:
View Crash from locally-built coqide
Process: coqide [26881]
Path: /Users/USER/*/coqide
Identifier: coqide
Version: 0
Code Type: X86-64 (Native)
Parent Process: bash [42527]
Responsible: coqide [26881]
User ID: 501
Date/Time: 2019-11-29 17:12:42.397 +0100
View exp_filter_s.v
Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f.
Section str_def.
Variable A : Set.
CoInductive str (A: Set) : Set :=
SCons: A -> str A -> str A.
You can’t perform that action at this time.