nkaretnikov

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0 
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

nkaretnikov

This query

INSERT INTO "event_user_notification_sent" (
    "id", "ts", "notification"
) (
    SELECT "id", "ts", "notification"
	FROM "event_notification_sent"
	WHERE "id" IN (
        SELECT "id"

nkaretnikov

(** One more quick digression, for adventurous souls: if we can define
    parameterized propositions using [Definition], then can we also
    define them using [Fixpoint]?  Of course we can!  However, this
    kind of "recursive parameterization" doesn't correspond to
    anything very familiar from everyday mathematics.  The following
    exercise gives a slightly contrived example. *)

(** **** Exercise: 4 stars, optional (true_upto_n__true_everywhere) *)
(** Define a recursive function
    [true_upto_n__true_everywhere] that makes

nkaretnikov

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  intros.
  unfold excluded_middle in H.
  unfold "~" in H0.
  unfold "~" in H.
(* 1 subgoals, subgoal 1 (ID 72) *)

nkaretnikov

(** **** Exercise: 3 stars (all_forallb) *)
(** Inductively define a property [all] of lists, parameterized by a
    type [X] and a property [P : X -> Prop], such that [all X P l]
    asserts that [P] is true for every element of the list [l]. *)

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=
  | all_nil : all X P []
  | all_cons : forall (x : X) (xs : list X),
                 P x -> all X P xs -> all X P (x :: xs).

nkaretnikov

(** Recall the function [forallb], from the exercise
    [forall_exists_challenge] in chapter [Poly]: *)

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
    | [] => true
    | x :: l' => andb (test x) (forallb test l')
  end.

(** Using the property [all], write down a specification for [forallb],

nkaretnikov

# Part of configuration.nix

  # Mix left and right channels.
  sound.extraConfig =
    ''
    pcm.!default {
        type plug
        slave.pcm {
            type asym
            playback.pcm {

nkaretnikov

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
  intros. apply beq_nat_true. apply H. Qed.

Fixpoint elem {X : Type} {eq : Eq X} (x : X) (xs : list X) : bool :=

nkaretnikov

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y ;
  leibniz_eqb : forall x y, x = y -> eqb x y = true }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
(* eqb_leibniz *)
  intros. apply beq_nat_true. apply H.

nkaretnikov

Inductive in_order_merge {X : Type} : (list X) -> (list X) -> (list X) -> Prop :=
  | iom_nil : forall (xs : list X),
                in_order_merge [] xs xs
  | iom_seq_l : forall (x : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge (x::xs) ys (x::zs)
  | iom_seq_r : forall (y : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge xs (y::ys) (y::zs).

Theorem iom_seq_l_inverse  :
  forall {X : Type} (x : X) (xs ys zs : list X),