Skip to content

Instantly share code, notes, and snippets.

View palmskog's full-sized avatar

Karl Palmskog palmskog

83 followers · 0 following
View GitHub Profile
@palmskog
palmskog / pos-neg.md
Last active July 23, 2023 21:17
Positive vs. negative coinductive finiteness in Coq

Positive vs. negative coinductive finiteness in Coq

Positive

@palmskog
palmskog / gfp_leq_Chain.v
Created July 21, 2023 09:55
gfp_leq_Chain example
From Coq Require Import RelationClasses Program.Basics.
From Coinduction Require Import all.
Import CoindNotations.
Lemma gfp_leq_Chain {X} {L : CompleteLattice X} (b : mon X) (R : Chain b) :
gfp b <= b ` R.
Proof.
rewrite <- (gfp_fp b).
apply b.
eapply gfp_chain.
Qed.
@palmskog
palmskog / sort_stdpp_itauto.v
Created July 13, 2022 11:34
From Cdcl Require Import Itauto.
From stdpp Require Import prelude.
Inductive Sorted : list nat -> Prop :=
| sorted_nil : Sorted []
| sorted_singleton : forall n, Sorted [n]
| sorted_cons : forall n m p, n <= m -> Sorted (m :: p) -> Sorted (n :: m :: p).
#[local] Hint Constructors Sorted : core.
@palmskog
palmskog / regexp.v
Created March 24, 2022 21:57
(* generated by Ott 0.32 from: regexp.ott *)
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Ott.ott_list_core.
Import ListNotations.
Section RegExp.
@palmskog
palmskog / sqrt2.v
Last active September 18, 2021 16:51
From Coq Require Import Arith Lia.
Lemma monotonic_inverse :
forall f : nat -> nat,
(forall x y : nat, x < y -> f x < f y) ->
forall x y : nat, f x < f y -> x < y.
Proof.
intros f Hmon x y Hlt; case (le_gt_dec y x); auto.
intros Hle; elim (le_lt_or_eq _ _ Hle).
intros Hlt'; elim (lt_asym _ _ Hlt); apply Hmon; auto.
@palmskog
palmskog / elmo.v
Last active April 28, 2021 14:57
Induction priniciple for Elmo
Require Import Arith.
Require Import Bool.
Require Import List.
Definition n : Set := nat.
Definition k : Set := nat.
Inductive Label : Set :=
| Receive : Label
@palmskog
palmskog / alternate_refine.v
Created September 28, 2020 10:20
Require Import List.
Require Import Sorting.Permutation.
Require Import Arith.
Require Import Wf_nat.
Require Import ssreflect.
Section Alternate.
Variable A : Type.
@palmskog
palmskog / follows_assoc_set.v
Created August 4, 2020 16:28
(** SSReflect boilerplate. *)
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
Set Asymmetric Patterns.
Set Bullet Behavior "None".
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(** Traces as lazy lists of booleans. *)
@palmskog
palmskog / follows_assoc.v
Created August 4, 2020 12:17
(** SSReflect boilerplate. *)
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
Set Asymmetric Patterns.
Set Bullet Behavior "None".
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(** Traces as lazy lists of booleans. *)
@palmskog
palmskog / fitch_system.ml
Created March 30, 2020 01:16
Verified Fitch-style proof checker extracted from Coq to OCaml
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b
(** val fst : ('a1 * 'a2) -> 'a1 **)