siraben

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import xor_swap.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

(* Specification of xor swap. In words:

   Let a and b be unsigned int pointers to values n and m
   respectively, with respective writable shares sh1 and sh2, and

siraben

(* Coq code for https://siraben.github.io/2021/06/27/classical-math-coq.html *)

Definition left_inverse {A B} (f : A -> B) g := forall a, g (f a) = a.

Definition right_inverse {A B} (f : A -> B) g := forall b, f (g b) = b.

Module NaiveInjective.

Definition injective {A B} (f : A -> B) :=
  forall a' a'', a' <> a'' -> f a' <> f a''.

siraben

Require Import Arith.PeanoNat.
Require Import List.
Import Nat.
Import ListNotations.

(** * Reflexive transitive closure of a relation *)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),

siraben

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import factorial.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

(* First we right down a specification of factorial in Coq that
   operates on integers. We need to prove that it terminates as well. *)
Function factorial (n: Z) { measure Z.to_nat n } :=
 if Z_gt_dec n 0 then n * factorial (n-1) else 1.

siraben

Note: due to volume, this has been moved to https://github.com/siraben/freenode-exodus

Projects and channels that have left Freenode

This is a (necessarily incomplete) list of projects and channels that have decided to permanently move out of Freenode to https://libera.chat (unless stated otherwise). Please reach out below or on IRC if there's additions or corrections.

Sources are mostly comments I've seen on HN, various IRC channels and web searches.

• ADIIRC
• Alpine (to oftc)
• Anbox

siraben

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
Require Import Arith.
Import Nat.
Require Import Lia.

(** * Reflexive transitive closure of a relation *)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),

siraben

(* Showing how to create new tactics only using refine *)

Inductive equal {A : Type} (x : A) : A -> Prop := equal_refl : equal x x.

Check equal_refl.

(* equal_refl *)
(*      : forall x : ?A, equal x x *)
(* where *)
(* ?A : [ |- Type] *)

siraben

Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Init.Nat.
From Coq Require Import Lia.
From Coq Require Import Lists.List.
Import ListNotations.
From PLF Require Import Maps.
From PLF Require Import Smallstep.
Import Nat.

siraben

(** Originally written when I was in high school so many things are not ideal here **)
Section Sets.
Variable set : Type.
Variable element : set -> set -> Prop.

Definition subset (x:set) (y:set) :=
  forall z:set, element z x -> element z y.

Axiom equality : forall x y:set, x = y <-> forall z:set, element z x <-> element z y.

siraben

(* For the proof idea see https://math.stackexchange.com/a/894767 *)
Require Import Psatz.
From Coq.Arith Require Import PeanoNat.
Import Nat.

Fixpoint fib n :=
  match n with
  | 0 => 1
  | S n =>
    match n with