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
View dep_pair_eq.v
Require Import ProofIrrelevance.
Section dep_pair.
Context {A : Type} {P : A -> Prop}.
Definition dep_pair := ex_intro P.
Lemma dep_pair_eq (a1 a2 : A) p1 p2: a1 = a2 -> dep_pair a1 p1 = dep_pair a2 p2.
Proof.
intros ->.
(* Now f_equal can reduce the equality to a homogeneous one, so it works. *)
@Blaisorblade
Blaisorblade / flambda-vs-not.md
Last active Oct 22, 2019
Comparing ocaml.4.07.1, without and with flambda+no-flat-float-array
View flambda-vs-not.md

So, here's a data point. On my 4-core MacBookPro (Intel Core i7 3,1GHz, 16GB RAM), flambda is slower than vanilla on coq-stdpp, which does not use native-compute AFAIK (and comes from many of the same authors as lambda-rust).

To install this coq-stdpp version, you'll have to run first:

opam repo add iris-dev git+https://gitlab.mpi-sws.org/iris/opam.git

With ocaml-base-compiler.4.07.1:

@Blaisorblade
Blaisorblade / bugLtacSsreflect.v
Last active Oct 20, 2019
Using ssreflect fancy `rewrite` `r_pattern` conflicts with Ltac (found on #coq)
View bugLtacSsreflect.v
(* Based on example from
https://coq.github.io/doc/V8.10.0/refman/proof-engine/ssreflect-proof-language.html#contextual-patterns-in-rewrite *)
(* Find `Fail` to see the error *)
From Coq Require Import ssreflect.
Notation "n .+1" := (Datatypes.S n) (at level 2, left associativity,
format "n .+1") : nat_scope.
Axiom addSn : forall m n, m.+1 + n = (m + n).+1.
(* addSn is declared *)
Axiom addn0 : forall m, m + 0 = m.
View ForallT.v
Require Import List.
Import ListNotations.
Inductive ForallT {A : Type} (P : A -> Type) : list A -> Type :=
| ForallT_nil : ForallT P []
| ForallT_cons (x : A) (l : list A) : P x -> ForallT P l -> ForallT P (x :: l).
Hint Constructors ForallT : core.
Definition fold_ForallT {A R : Type} {P: A -> Type}
(hnil : R) (hcons : forall (a : A), P a -> R -> R)
View errorlog.txt
Coq Language Server: process.version: v10.11.0, process.arch: x64}
Loaded project at /Users/pgiarrusso/git/Coq/dot-iris
Changed path to: /Users/pgiarrusso/.opam/coq-8.8.2/bin/
starting coqtop
exec: /Users/pgiarrusso/.opam/coq-8.8.2/bin/coqtop -v
Listening at 127.0.0.1:50060
Listening at 127.0.0.1:50061
Listening at 127.0.0.1:50062
Listening at 127.0.0.1:50063
Detected coqtop version 8.8.2
View log.txt
$ brew cask upgrade --verbose --debug
==> Casks with `auto_updates` or `version :latest` will not be upgraded
==> Upgrading 1 outdated package:
intel-power-gadget 3.5.5,828382 -> 3.6.1,833853
==> Started upgrade process for Cask intel-power-gadget
==> Upgrading intel-power-gadget
==> Printing caveats
==> Printing caveats
==> Caveats
To install and/or use intel-power-gadget you may need to enable its kernel extension in:
View omega-works-here.v
Require Import Omega.
Lemma foo (n n0 n1 n2 n3 n4: nat):
n + (n0 + n1) = 0 ->
n2 + (n3 + n4) = 0 ->
n0 + n3 + n + n2 + (n1 + n4) = 0.
Proof. omega. Qed.
View zipVector.v
Require Coq.Vectors.Vector.
Definition splitVec {A n} (xs : Vector.t A (S n)): A * Vector.t A n :=
match xs with
(* | Vector.nil _ => _ (* fun A (a: A) => a *) *)
| Vector.cons _ x n0 xs => (x, xs)
end.
(* Alternative version. *)
Definition splitVec2 {A n} (xs : Vector.t A (S n)): A * Vector.t A n.
View formatting2.v
Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@ T1 }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
(and T1 (and T2 .. (and Tn True)..))
(format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'") : dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.
Check {@ True ; True -> False ; False } % dms.
View formatting.v
Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@ T1 }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
(and T1 (and T2 .. (and Tn True)..))
(* (format "'[v' {@ '[' T1 ']' ; '//' T2 ; '//' .. ; '//' Tn } ']'") *)
: dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.
You can’t perform that action at this time.