Initial commit

Changes

4 changed files (+647/-0)

• .gitignore (new)
  • @@ -0,0 +1,45 @@
    + .*.aux + .*.d + *.a + *.cma + *.cmi + *.cmo + *.cmx + *.cmxa + *.cmxs + *.glob + *.ml.d + *.ml4.d + *.mlg.d + *.mli.d + *.mllib.d + *.mlpack.d + *.native + *.o + *.v.d + *.vio + *.vo + *.vok + *.vos + .coq-native + .csdp.cache + .lia.cache + .nia.cache + .nlia.cache + .nra.cache + csdp.cache + lia.cache + nia.cache + nlia.cache + nra.cache + native_compute_profile_*.data + + # generated timing files + *.timing.diff + *.v.after-timing + *.v.before-timing + *.v.timing + time-of-build-after.log + time-of-build-before.log + time-of-build-both.log + time-of-build-pretty.log
• sort.v (new)
  • @@ -0,0 +1,156 @@
    + (** * Proving insertion sort correct, easily *) + + (** This is a PDF rendering of the gist by siraben at + $\href{https://gist.github.com/siraben/3fedfc2c5a242136a9bc6725064e9b7d}{\text{this + URL}}$. I give an example of how to prove insertion sort correct + easily with $\href{https://coqhammer.github.io/}{\text{CoqHammer}}$. + CoqHammer is a proof automation tool, more details can be found from + the website. What matters for us is that we can use it as an oracle + of sorts, just supplying it with the correct lemmas and letting it + finish the proof. Whenever you see a call to a tactic such as + [sauto], [sfirstorder] and so on, those were found interactively by + running the [best] command first (possibly with some lemmas), then + copy/pasting the output. While we could use [sauto] in most places, + these more restricted tactics help with performance. + + From the standard library we will just import natural numbers and + lists. *) + + From Stdlib Require Import Nat List. + (** The secret sauce: CoqHammer. *) + + From Hammer Require Import Tactics. + + Import ListNotations. + Open Scope nat. + + (** * Sorted predicate *) + (** [Sorted] is a predicate on lists of natural numbers that expresses + sortedness. It is defined as follows: + - [sorted_nil]: the empty list is sorted + - [sorted_singleton]: the list containing one element is sorted + - [sorted_cons]: let [n], [m], [p] be natural numbers such that $n\le m$ and [m::p] is sorted, then [n::m::p] is sorted *) + + 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). + + (** * Inserting an element *) + (** Insert [n] into [l] just before the first number that is larger + than [n]. *) + + Fixpoint insert n l := + match l with + | [] => [n] + | (x :: y) => if n <=? x then n :: x :: y else x :: insert n y + end. + + (** * Insert preserves sortedness *) + (** Let [l] be a sorted list, then [insert x l] is a sorted list. We + proceed by induction on [l]. The base case is trivial. For the + inductive case, we just perform case analysis on the tail again to + expose another element and use CoqHammer to finish the proof. *) + + Lemma sorted_insert : forall x l, Sorted l -> Sorted (insert x l). + Proof. + induction l. + - sfirstorder. + - destruct l; sblast. + Qed. + + (** * Insertion sort *) + (** The definition of insertion sort, [sort], is straightforward. For + the nil case, return nil, otherwise for [x :: l], recursively sort [l] + then insert [x] into the sorted tail. *) + + Fixpoint sort l := + match l with + | [] => [] + | x :: l => insert x (sort l) + end. + + (** * Correctness of [sort] *) + (** Let [l] be an arbitrary list. Then [sort l] is sorted. The proof + proceeds by induction on [l] and the use of the [sorted_insert] + lemma. *) + + Lemma sort_sorts : forall l, Sorted (sort l). + Proof. + induction l; sfirstorder use: sorted_insert. + Qed. + + (** * Definition of permutation *) + (** Unlike a usual mathematical definition, we define permutations + inductively. We have: + - nil is a permutation of nil + - if [l] is a permutation of [l'], then [x::l] is a permutation of [x::l'] + - [x::y::l] is a permutation of [y::x::l] + - permutations are transitive + *) + + Inductive permutation {A} : list A -> list A -> Prop := + | perm_nil : permutation [] [] + | perm_cons : forall l l' x, permutation l l' -> permutation (x :: l) (x :: l') + | perm_swap : forall l x y, permutation (x :: y :: l) (y :: x :: l) + | perm_trans : forall a b c, permutation a b -> permutation b c -> permutation a c. + + (** As an example, we can show that the list $[1,2]$ is a permutation of $[2,1]$ *) + + Example permutation_ex1 : permutation [1;2] [2;1]. + Proof. sfirstorder. Qed. + + (** ** Symmetry of [permutation] *) + + Lemma permutation_sym {A} : forall (a b : list A), permutation a b -> permutation b a. + Proof. + intros a b Ha. + induction Ha; sauto lq: on. + Qed. + + (** ** [permutation] is respected by prepending with a list *) + (** If [tl] is a permutation of [tl'] then any list prepended to both + respects the relation. *) + + Lemma permutation_app_head {A} : forall (l tl tl' : list A), + permutation tl tl' -> permutation (l ++ tl) (l ++ tl'). + Proof. + intros l tl tl' H. + induction l; sauto lq: on. + Qed. + + (** ** [x::l] is a permutation of [insert x l] *) + + Lemma insert_perm : forall x l, permutation (x :: l) (insert x l). + Proof. + induction l; sauto q: on. + Qed. + + (** ** [sort] produces a permutation of the input *) + (** For any list [l], sorting the list produces a permutation of [l]. + The base case is trivial. For the inductive case, we have to prove + that [permutation l (sort l)] implies [permutation (a :: l) (insert a + (sort l))]. We perform case analysis on l then use transitivity of + [permutation] and some other lemmas to finish the proof. *) + + Lemma sort_perm : forall l, permutation l (sort l). + Proof. + induction l. + - sfirstorder. + - simpl. + sauto lq: on use: @perm_cons, @perm_trans, @permutation_sym, insert_perm. + Qed. + + (** * General definition of a sorting algorithm *) + (** More generally, [f] is a sorting algorithm if the output is sorted + and a permutation of the original list. *) + + Definition is_sorting_algorithm f := forall l, permutation l (f l) /\ Sorted (f l). + + (** ** [sort] is a sorting algorithm *) + (** Finally, we can combine our lemmas to show that [sort] is a sorting algorithm. *) + + Theorem insert_sort_is_sorting_algorithm : is_sorting_algorithm sort. + Proof. + sfirstorder use: sort_perm, sort_sorts unfold: is_sorting_algorithm. + Qed.
• stlc_slop.v (new)
  • @@ -0,0 +1,224 @@
    + (** Simply typed lambda calculus in Rocq! + Ported from https://git.unnamed.website/miscelleaneous/tree/STLC.lean *) + + From Stdlib Require Import Arith Bool Lia List Unicode.Utf8. + Import ListNotations. + + (** We use Greek letters for variables with type [Typ] *) + Inductive Typ : Type := + (** New named type *) + | new : nat → Typ + (** Function type *) + | fn : Typ → Typ → Typ. + + Fixpoint Typ_eqb (a b : Typ) : bool := + match a, b with + | new x, new y => Nat.eqb x y + | fn a1 b1, fn a2 b2 => Typ_eqb a1 a2 && Typ_eqb b1 b2 + | _, _ => false + end. + + Lemma Typ_eqb_refl : ∀ t, Typ_eqb t t = true. + Proof. + induction t. + - apply Nat.eqb_refl. + - apply andb_true_iff. + split; assumption. + Qed. + + Lemma Typ_eqb_eq : ∀ a b, Typ_eqb a b = true ↔ a = b. + Proof. + induction a as [x | a1 IHa1 a2 IHa2]; destruct b as [y | b1 b2]; simpl; + split; intro H; try discriminate. + - f_equal. apply Nat.eqb_eq. exact H. + - injection H; intro Heq; subst. apply Nat.eqb_refl. + - apply andb_true_iff in H. destruct H as [H1 H2]. + apply IHa1 in H1. apply IHa2 in H2. subst. reflexivity. + - injection H; intros; subst. rewrite !Typ_eqb_refl. reflexivity. + Qed. + + Inductive Term : Type := + (** variable *) + | var : nat → Term + (** lambda with de Bruijn indices *) + | lam : Term → Term + (** Function application *) + | app : Term → Term → Typ → Term. + + (** The type checker! *) + Fixpoint check (env : list Typ) (t : Term) (τ : Typ) : bool := + match t with + | var x => + match nth_error env x with + | Some t' => Typ_eqb t' τ + | None => false + end + | lam b => + match τ with + | fn α β => check (α :: env) b β + | _ => false + end + | app f a α => + check env f (fn α τ) && check env a α + end. + + (** Increment free variables by [k] *) + Fixpoint incr (k d : nat) (t : Term) : Term := + match t with + | var x => var (if Nat.leb d x then x + k else x) + | lam b => lam (incr k (S d) b) + | app f a α => app (incr k d f) (incr k d a) α + end. + + (** [incr] preserves type *) + Theorem check_incr : ∀ t env' env env'' τ k, + check (env' ++ env) t τ = true → + length env'' = k → + check (env' ++ env'' ++ env) (incr k (length env') t) τ = true. + Proof. + induction t as [x | b IHb | f IHf a IHa α]; + intros env' env env'' τ k H Hk. + - simpl in H. + simpl. + destruct (Nat.leb (length env') x) eqn:E; simpl. + + apply Nat.leb_le in E. + rewrite nth_error_app2 in H by lia. + rewrite nth_error_app2 by lia. + rewrite nth_error_app2 by lia. + replace (x + k - length env' - length env'') with (x - length env') by lia. + exact H. + + apply Nat.leb_gt in E. + rewrite nth_error_app1 in H by lia. + rewrite nth_error_app1 by lia. + exact H. + - destruct τ as [|τ1 τ2]; [discriminate|]. + simpl in H. + exact (IHb (τ1 :: env') env env'' τ2 k H Hk). + - simpl in H. + apply andb_true_iff in H. + destruct H as [H1 H2]. + simpl. + apply andb_true_iff. + auto. + Qed. + + (** [incr 0] does nothing *) + Theorem incr_zero : ∀ t d, incr 0 d t = t. + Proof. + induction t as [n | b IHb | f IHf a IHa α]; intros d; simpl. + - f_equal. + destruct (Nat.leb d n); lia. + - f_equal. + apply IHb. + - rewrite IHf, IHa. + reflexivity. + Qed. + + (** Substitute [s] at index [n] in a term *) + Fixpoint sub (n : nat) (s : Term) (t : Term) : Term := + match t with + | var x => + if Nat.eqb x n then incr n 0 s + else var (if Nat.ltb n x then x - 1 else x) + | lam b => lam (sub (S n) s b) + | app f a α => app (sub n s f) (sub n s a) α + end. + + (** [sub] preserves type *) + Theorem check_sub : ∀ t env' env σ s τ, + check (env' ++ σ :: env) t τ = true → + check env s σ = true → + check (env' ++ env) (incr (length env') 0 s) σ = true → + check (env' ++ env) (sub (length env') s t) τ = true. + Proof. + induction t as [x | b IHb | f IHf a IHa α]; + intros env' env σ s' τ H Hs Hs'. + - simpl in H. simpl. + destruct (Nat.eqb x (length env')) eqn:E; simpl. + + apply Nat.eqb_eq in E. subst x. + rewrite nth_error_app2 in H by lia. + replace (length env' - length env') with 0 in H by lia. + simpl in H. + apply Typ_eqb_eq in H. subst τ. + exact Hs'. + + apply Nat.eqb_neq in E. + destruct (Nat.ltb (length env') x) eqn:E2; simpl. + * apply Nat.ltb_lt in E2. + rewrite nth_error_app2 in H by lia. + rewrite nth_error_app2 by lia. + replace (x - length env') with (S (x - length env' - 1)) in H by lia. + simpl in H. + replace (x - 1 - length env') with (x - length env' - 1) by lia. + exact H. + * apply Nat.ltb_ge in E2. + assert (x < length env') by lia. + rewrite nth_error_app1 in H by lia. + rewrite nth_error_app1 by lia. + exact H. + - destruct τ as [|τ1 τ2]; [simpl in H; discriminate|]. + simpl in H. simpl. + apply (IHb (τ1 :: env') env σ s' τ2 H Hs). + apply (check_incr s' [] env (τ1 :: env') σ (S (length env'))). + + exact Hs. + + reflexivity. + - simpl in H. apply andb_true_iff in H. destruct H as [H1 H2]. + simpl. apply andb_true_iff. split. + + apply (IHf env' env σ s' (fn α τ)); assumption. + + apply (IHa env' env σ s' α); assumption. + Qed. + + (** Eval without worrying about types. + Rocq doesn't have [partial def], so we use a fuel parameter. *) + Fixpoint eval_untyped (fuel : nat) (t : Term) : Term := + match fuel with + | 0 => t + | S fuel' => + match t with + | var x => var x + | lam b => lam (eval_untyped fuel' b) + | app f a α => + let a' := eval_untyped fuel' a in + match eval_untyped fuel' f with + | lam b => eval_untyped fuel' (sub 0 a' b) + | x => app x a' α + end + end + end. + + (** Eval a well-typed expression. + Like the Lean version this admits termination; we use a fuel + parameter so the function is structurally recursive in Rocq. + TODO: prove termination via a logical-relations argument + (see https://cecchetti.sites.cs.wisc.edu/cs704/2025fa/notes/lec23-normalization.pdf). *) + Fixpoint eval (fuel : nat) (env : list Typ) (t : Term) (τ : Typ) + (h : check env t τ = true) {struct fuel} + : { t' : Term | check env t' τ = true }. + Proof. + destruct fuel as [|fuel']. + - exact (exist _ t h). + - destruct t as [x | b | f0 a0 α0]. + + (* var *) exact (exist _ (var x) h). + + (* lam *) + destruct τ as [|α β]; [discriminate|]. + simpl in h. + destruct (eval fuel' (α :: env) b β h) as [b' hb]. + exists (lam b'). simpl. exact hb. + + (* app *) + simpl in h. apply andb_true_iff in h. destruct h as [hf ha]. + destruct (eval fuel' env a0 α0 ha) as [a' ha']. + destruct (eval fuel' env f0 (fn α0 τ) hf) as [f' hf']. + destruct f' as [x' | b | g c β]. + * (* var: stuck *) + exists (app (var x') a' α0). simpl. + apply andb_true_iff. + auto. + * (* lam: β-reduce *) + simpl in hf'. + apply (eval fuel' env (sub 0 a' b) τ). + apply (check_sub b [] env α0 a' τ hf' ha'). + simpl. rewrite incr_zero. exact ha'. + * (* app: stuck *) + exists (app (app g c β) a' α0). simpl. + apply andb_true_iff. + auto. + Defined.
• stlc_slop2.v (new)
  • @@ -0,0 +1,222 @@
    + (** Simply typed lambda calculus in Rocq! + Ported from https://git.unnamed.website/miscelleaneous/tree/STLC.lean *) + + From Stdlib Require Import Arith Bool Lia List Unicode.Utf8. + Import ListNotations. + From Hammer Require Import Tactics Hammer. + + (** We use Greek letters for variables with type [Typ] *) + Inductive Typ : Type := + (** New named type *) + | new : nat → Typ + (** Function type *) + | fn : Typ → Typ → Typ. + + Fixpoint Typ_eqb (a b : Typ) : bool := + match a, b with + | new x, new y => Nat.eqb x y + | fn a1 b1, fn a2 b2 => Typ_eqb a1 a2 && Typ_eqb b1 b2 + | _, _ => false + end. + + Lemma Typ_eqb_refl : ∀ t, Typ_eqb t t = true. + Proof. + induction t. + - apply Nat.eqb_refl. + - hauto lq: on. + Qed. + + Lemma Typ_eqb_eq : ∀ a b, Typ_eqb a b = true ↔ a = b. + Proof. + induction a as [x | a1 IHa1 a2 IHa2]; destruct b as [y | b1 b2]; split; try discriminate. + - sfirstorder use: Nat.eqb_eq. + - sfirstorder use: Nat.eqb_refl. + - intro H. + apply andb_true_iff in H. + sfirstorder. + - hauto lq: on use: Typ_eqb_refl. + Qed. + + Inductive Term : Type := + (** variable *) + | var : nat → Term + (** lambda with de Bruijn indices *) + | lam : Term → Term + (** Function application *) + | app : Term → Term → Typ → Term. + + (** The type checker! *) + Fixpoint check (env : list Typ) (t : Term) (τ : Typ) : bool := + match t with + | var x => + match nth_error env x with + | Some t' => Typ_eqb t' τ + | None => false + end + | lam b => + match τ with + | fn α β => check (α :: env) b β + | _ => false + end + | app f a α => + check env f (fn α τ) && check env a α + end. + + (** Increment free variables by [k] *) + Fixpoint incr (k d : nat) (t : Term) : Term := + match t with + | var x => var (if Nat.leb d x then x + k else x) + | lam b => lam (incr k (S d) b) + | app f a α => app (incr k d f) (incr k d a) α + end. + + (** [incr] preserves type *) + Theorem check_incr : ∀ t env' env env'' τ k, + check (env' ++ env) t τ = true → + length env'' = k → + check (env' ++ env'' ++ env) (incr k (length env') t) τ = true. + Proof. + induction t as [x | b IHb | f IHf a IHa α]; intros env' env env'' τ k H Hk. + - simpl in H. + simpl. + destruct (Nat.leb (length env') x) eqn:E; simpl. + + apply Nat.leb_le in E. + rewrite nth_error_app2 in H by lia. + rewrite nth_error_app2 by lia. + rewrite nth_error_app2 by lia. + replace (x + k - length env' - length env'') with (x - length env') by lia. + exact H. + + apply Nat.leb_gt in E. + rewrite nth_error_app1 in H by lia. + rewrite nth_error_app1 by lia. + exact H. + - destruct τ as [|τ1 τ2]; [discriminate|]. + simpl in H. + exact (IHb (τ1 :: env') env env'' τ2 k H Hk). + - simpl in H. + apply andb_true_iff in H. + destruct H as [H1 H2]. + hauto lq: on. + Qed. + + (** [incr 0] does nothing *) + Theorem incr_zero : ∀ t d, incr 0 d t = t. + Proof. + induction t. + - hauto l: on. + - sfirstorder. + - sfirstorder. + Qed. + + (** Substitute [s] at index [n] in a term *) + Fixpoint sub (n : nat) (s : Term) (t : Term) : Term := + match t with + | var x => + if Nat.eqb x n then incr n 0 s + else var (if Nat.ltb n x then x - 1 else x) + | lam b => + lam (sub (S n) s b) + | app f a α => + app (sub n s f) (sub n s a) α + end. + + (** [sub] preserves type *) + Theorem check_sub : ∀ t env' env σ s τ, + check (env' ++ σ :: env) t τ = true → + check env s σ = true → + check (env' ++ env) (incr (length env') 0 s) σ = true → + check (env' ++ env) (sub (length env') s t) τ = true. + Proof. + induction t as [x | b IHb | f IHf a IHa α]; + intros env' env σ s' τ H Hs Hs'. + - simpl in H. simpl. + destruct (Nat.eqb x (length env')) eqn:E; simpl. + + apply Nat.eqb_eq in E. subst x. + rewrite nth_error_app2 in H by lia. + replace (length env' - length env') with 0 in H by lia. + simpl in H. + apply Typ_eqb_eq in H. subst τ. + exact Hs'. + + apply Nat.eqb_neq in E. + destruct (Nat.ltb (length env') x) eqn:E2; simpl. + * apply Nat.ltb_lt in E2. + rewrite nth_error_app2 in H by lia. + rewrite nth_error_app2 by lia. + replace (x - length env') with (S (x - length env' - 1)) in H by lia. + simpl in H. + replace (x - 1 - length env') with (x - length env' - 1) by lia. + exact H. + * apply Nat.ltb_ge in E2. + assert (x < length env') by lia. + rewrite nth_error_app1 in H by lia. + rewrite nth_error_app1 by lia. + exact H. + - destruct τ as [|τ1 τ2]; [simpl in H; discriminate|]. + simpl in H. simpl. + apply (IHb (τ1 :: env') env σ s' τ2 H Hs). + apply (check_incr s' [] env (τ1 :: env') σ (S (length env'))). + + exact Hs. + + reflexivity. + - simpl in H. apply andb_true_iff in H. destruct H as [H1 H2]. + simpl. + apply andb_true_iff. + sfirstorder. + Qed. + + (** Eval without worrying about types. + Rocq doesn't have [partial def], so we use a fuel parameter. *) + Fixpoint eval_untyped (fuel : nat) (t : Term) : Term := + match fuel with + | 0 => + t + | S fuel' => + match t with + | var x => + var x + | lam b => + lam (eval_untyped fuel' b) + | app f a α => + let a' := eval_untyped fuel' a in + match eval_untyped fuel' f with + | lam b => eval_untyped fuel' (sub 0 a' b) + | x => app x a' α + end + end + end. + + (** Eval a well-typed expression. + Like the Lean version this admits termination; we use a fuel + parameter so the function is structurally recursive in Rocq. + TODO: prove termination via a logical-relations argument + (see https://cecchetti.sites.cs.wisc.edu/cs704/2025fa/notes/lec23-normalization.pdf). *) + Fixpoint eval (fuel : nat) (env : list Typ) (t : Term) (τ : Typ) + (h : check env t τ = true) {struct fuel} + : { t' : Term | check env t' τ = true }. + Proof. + destruct fuel as [|fuel']. + - exact (exist _ t h). + - destruct t as [x | b | f0 a0 α0]. + + exact (exist _ (var x) h). + + destruct τ as [|α β]; [discriminate|]. + simpl in h. + destruct (eval fuel' (α :: env) b β h) as [b' hb]. + exists (lam b'). + simpl. + exact hb. + + simpl in h. apply andb_true_iff in h. destruct h as [hf ha]. + destruct (eval fuel' env a0 α0 ha) as [a' ha']. + destruct (eval fuel' env f0 (fn α0 τ) hf) as [f' hf']. + destruct f' as [x' | b | g c β]. + * exists (app (var x') a' α0). + apply andb_true_iff. + auto. + * simpl in hf'. + apply (eval fuel' env (sub 0 a' b) τ). + apply (check_sub b [] env α0 a' τ hf' ha'). + simpl. + rewrite incr_zero. + exact ha'. + * exists (app (app g c β) a' α0). simpl. + apply andb_true_iff. + auto. + Defined.