siraben

siraben

(* There are no surjections from {1} to {1,2} *)

Definition surjective {A B} (f : A -> B) := forall (b : B), exists (a : A), b = f a.

Definition One := unit.

Definition Two := bool.

Theorem no_surject_one_two : ~ exists (f : One -> Two), surjective f.
Proof.

siraben

(* P is a family of nat-indexed sets of nat such that:
   H: for all n, there is an m such that m ∈ P n
   -----------
   Then we show that there is a choice function f
*)
Theorem countable_choice_wikipedia
  (P : nat -> (nat -> Prop)) (H : forall n, { m | P n m }) : { f | forall n, (exists m, P n m /\ f n = m)}.
Proof.
  set (f := fun (n : nat) => let (m, Hm) := H n in m).
  exists f.

siraben

From Coq.Arith Require Import PeanoNat.
Import Nat.
Require Import Lia.

Definition add_mod n i j :=
  match i + j ?= n with
  | Lt => i + j
  | _ => i + j - n
  end.

siraben

Require Import ssreflect ssrfun.

Module Futamura.
  (* Program from a -> b written in L *)
  Inductive Program {a b language : Type} :=
  | mkProgram : (a -> b) -> Program.

  Definition runProgram {A B L} (p : @Program A B L) := match p with mkProgram f => f end.
  Notation "[ S | a >> b ]" := (@Program a b S) (at level 2) : type_scope.

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

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),