Skip to content

Instantly share code, notes, and snippets.

View Blaisorblade's full-sized avatar

Paolo G. Giarrusso Blaisorblade

View GitHub Profile
@Blaisorblade
Blaisorblade / proof_by_ctrl_c.v
Last active October 14, 2022 00:18
SIGINT as Prolog cut
(*
* Copyright (C) BedRock Systems Inc. 2020-22
*
* This software is distributed under the terms of the BedRock Open-Source License.
* See the LICENSE-BedRock file in the repository root for details.
*)
Require Export stdpp.fin_sets.
Require Export iris.prelude.prelude.
(** * Small extensions to [stdpp.fin_sets]. *)
@Blaisorblade
Blaisorblade / rewrite_drops_hyps.v
Created October 11, 2022 01:32
Demonstrate strange rewrite behavior
Require Import List.
Import ListNotations.
Lemma test1 :
length ([1] ++ [2]) = 2 ->
2 = 4.
Proof.
intros HA.
evar (N : nat).
```
$ git rev-parse HEAD
e31304d4d76d616130bc635457f12d5a6878b3d8
$ dune test --display verbose test/blackbox-tests/test-cases/promote/
Shared cache: enabled
Workspace root: /Users/pgiarrusso1/git-bedrock/dune
Running[0]: /Users/pgiarrusso1/git-bedrock/dune/_opam/bin/ocamlc.opt -config > /var/folders/6q/2ycxnczj1qsgwsk7lg3yd4bh0000gn/T/dune_f0778e_output
Dune context:
{ name = "default"
; kind = "default"
@Blaisorblade
Blaisorblade / leaky_strings.v
Last active July 19, 2022 21:43
Coq strings are so logical, they're literally built on truth
Require Import iris.proofmode.proofmode.
Lemma string_fun (PROP : bi) (X : PROP) : X ⊢ X.
Proof.
iIntros "X".
generalize true; intros.
Show.
(*
1 goal
@Blaisorblade
Blaisorblade / finite.v
Created May 19, 2022 16:32
bedrock.prelude.finite
(*
* Copyright (c) 2021 BedRock Systems, Inc.
*
* This software is distributed under the terms of the BedRock Open-Source License.
* See the LICENSE-BedRock file in the repository root for details.
*)
From stdpp Require Export finite.
From bedrock.prelude Require Import base bool numbers list_numbers gmap list fin_sets.
@Blaisorblade
Blaisorblade / elpi-5488-6af0b5.out
Created March 27, 2022 13:33
Elpi 1.14.3 vs OCaml 4.14.0 trunk — compile errors
dune build -p elpi -j 11 @all
(cd _build/default && /Users/pgiarrusso1/.opam/4.14.0+trunk/bin/ocamlc.opt -linkall -g -bin-annot -I src/.elpi.objs/byte -I src/.elpi.objs/public_cmi -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/camlp5 -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/ppx_deriving/runtime -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re/str -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/result -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/seq -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/stdlib-shims -I trace/runtime/.trace_ppx_runtime.objs/byte -no-alias-deps -open Elpi__ -o src/.elpi.objs/byte/elpi__Parser.cmi -c -intf src/parser.pp.mli)
File "src/parser.mli", line 34, characters 89-102:
34 | val parse_program_from_stream : parser_state -> print_accumulated_files:bool -> Loc.t -> char Stream.t -> Program.t
^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Stream
Use th
@Blaisorblade
Blaisorblade / decide_True_broke.v
Last active December 16, 2022 08:05
Minimized problem with `rewrite decide_True` and ssreflect
(*
Tested with:
Coq 8.15.0, Iris dev.2022-01-24.0.72a4bd62.
Coq 8.16.0, Iris 4.0.0
*)
From iris.prelude Require Import prelude.
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
@Blaisorblade
Blaisorblade / hide_global_hints.v
Created February 26, 2022 00:51
Coq: Opaque module ascription already hides global hints
Require Import stdpp.base.
Module Type FOO.
Definition number : Set := nat.
End FOO.
Module Import foo : FOO.
Definition number : Set := nat.
Fail #[global] Instance number_inh : Inhabited number := _.
@Blaisorblade
Blaisorblade / modules_instances.v
Last active January 31, 2022 09:44
Demonstrate how opaque ascription takes hints from the interface, while transparent ascription takes them from bodies
Require Import stdpp.base.
Require Import NArith.
(* We omit [Require Import stdpp.numbers.], which already has the [Inhabited]
instances we test here. *)
Module Type X.
#[global] Instance a : Inhabited nat.
Proof.
Fail apply _.
(* Distributed under the terms of the MIT license. *)
From Coq Require Import CMorphisms.
From MetaCoq.Template Require Import config utils Reflect Ast AstUtils Induction LiftSubst Reflect.
Require Import ssreflect.
From Equations.Prop Require Import DepElim.
Set Equations With UIP.
Definition R_universe_instance R :=
fun u u' => Forall2 R (List.map Universe.make u) (List.map Universe.make u').