Code Snippets Coq

Short texts Coq 🧑‍💻 Code snippets Coq ✍️ Reading lists Coq 👀

Rewritefail.v

up: N Hacc: ∀ y : N, y < up → Acc (λ x y0 : N, x < y0) y IHup: ∀ y : N, y < up → length (length_byte_list y) = N.to_nat (y / 256 + 1) Hnp: (up

Ring.v

Before using the tactic ring, field, we need to add the instance https://coq.inria.fr/refman/addendum/ring.html#coq:cmd.Add-Ring Require Import Ring Field ZArith. Open Scope Z_scope. Example tx : forall x y : Z, (x + y) * (x + y) = x * x + y * y + 2 * x * y. Proof. intros. ring. Qed.

rfc7539.v

Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String. Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations. Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope. Require Import coqutil.Word.LittleEndianList. (* reference: https://datatracker.ietf.org/doc/html/rfc7539 *) (* perl -ne ‘BEGIN{$/=””} print unless /^Example /’ < rfc7539.v *) Definition poly1305 (p:=2^130-5) (k : list byte) (m : list byte) : list byte := let […]

Futamura Projections in Coq

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 […]