可参考 官网。 内容 可以将类型的一些属性作为类型的编号，这样在递归定义类型时就可以将属性直接计算出来。 例如，以下是定长数组的定义： type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)  规定只能用长度为 n 的定长数组构造出长度为 n + 1 的定长数组， 因此长度可以直接依据类型定义计算出来。 个人理解编号本质上也是一种类型参数。 习题一：合并定长数组 思路 由于隐式参数的大小关系可以被 SMT Prover...

概要 这一小节讲述了如何用 F* 实现快排算法，并且证明其确实有排序的功能。 铺垫：快排实现 递归计算 list 长度： let rec length #a (l:list a) : nat = match l with | [] -> 0 | _ :: tl -> 1 + length tl  递归实现将一个 list 与另一个 list 合并： let rec append #a (l1 l2:list a) : list a = match l1 with | [] -> l2 | hd :: tl -> hd :: append tl l2  递归实现将列表根据...

P3372 【模板】线段树 1 使用最基本的线段树即可。 遇到的坑  内存要开够，考虑直接采用 N << 2 build 和 add 的时候都要 push_up add 和 query 的时候都要 push_down r - l == 1 不要写成 l - r == 1  P3373 【模板】线段树 2 将 tag 的使用顺序规定为先乘后加， 那么先加 a，后乘 b 等效于先乘 b，后加 a * b。 这一规则意味着：  push_down 时，先应用乘标记，再运用加标记 push_down 时，乘标记应用时会影响子代加标记 当前节点已有加标记时，乘操作会影响加标记  由于时间宽裕...

FStar 是什么？ F* 是一种面向证明的编程语言，运用大量奇技淫巧实现程序自证明，例如：  依值类型，Dependent Type，简而言之就是允许类型依赖于具体的值 函数式编程，Functional Programming，函数是一等公民，能像值一样作为参数和返回值 元语言，Meta Language，模糊程序与数据的边界，允许程序生成程序 提纯类型（瞎翻），Refinement Type，给已存在的类型加上限制，获得新的类型  推荐从 官网 了解 F*。 FStar 练习：Part 1, Lemmas and proofs by induction 证明递归实现的阶乘在 x>2x...

A. Medium Number 题意 给三个不相等的数，找中位数。 思路 三个数的大小关系总共有六种情况，枚举即可。 但如果追求快速，考虑对数组进行排序。 代码 #include <bits/stdc++.h> using namespace std; #define ll long long // #define TEST #ifdef TEST #define sep cout << "---------\n" #define say(n) cout << n << ' '; #define sayln(n) cout << n...

声明 本人不会 Lisp，以下内容纯属娱乐。 目标 使用包含依值类型的 Lisp 方言将 Codeforces 上的算法题形式化。 力求保留题意，不在形式化时进行算法优化。这样可以解耦形式化和计算。 语言特性 nat 表示自然数，lambda，vec，eq 都是类型构造函数。 nth 是由 vec 实例和 nat 实例构造 nat 实例的构造函数。 same 是构造 eq 实例的构造函数，(: i nat) 用于标注 i 的类型是 nat。 map 的使用较为灵活，例如以下函数的值是 (tuple (eq i i) ... (eq i i))，类别是 type： (tupleMap (: di...

A. Parallel Projection 题面大意 长方体盒子里天花板和地上选定两点，找连接这两点的最短线。要求：  线必须与长方体的轴平行 线必须贴着长方体的边  两点水平面坐标为 (f,g),(a,b)(f, g), (a, b)(f,g),(a,b)，矩形大小为 (w,d)(w, d)(w,d)，其中 www 是宽度。 分析 考虑布线的以下阶段：  在天花板上的点 到顶上矩形的边上 到底部矩形的边上 到地上的点  容易发现，如果在第 2, 3 步选取了平行于 ddd 的边，则在平行于 ddd 的线可以去到最小值 ∣g−b∣|g - b|∣g−b∣平行于 hhh 的线可以从左边下，也可...