选项 Options 假设我们要编写一个函数，返回某个列表的第n个元素。如果我们给它类型nat→ natlist→ nat，那么当列表太短的时候，我们必须选择一些数字返回… Fixpoint nth_bad Fixpoint nth_bad (l:natlist) (n:nat) : nat := match l with | nil => 42 | a :: l' => match n with | 0 => a | S n' => nth_bad l' n' end end.  这个解决方案不太好：如果nth_bad返回42，我们无法在没有进一步处理的情况下判断该值...

1.  2. 把上面的函数maxPair改造成maxPair'，返回类型为option nat * option nat。当要找的数字不存在时用None而不是0替代。 Example test_maxPair‘1: maxPair’ [1;2;5;4;8;10;3] = (Some 5, Some 10). Proof. reflexivity. Qed. Example test_maxPair‘2: maxPair’ [2;4] = (None, Some 4). Proof. reflexivity. Qed.  3. Theorem rev_app_distr Theorem rev_...

关于列表的推理 Reasoning About Lists 与数字一样，关于列表处理函数的简单事实有时完全可以通过简化来证明。例如，对于这个定理来说，仅仅通过自反性进行简化就足够了。。。 Theorem nil_app : forall l : natlist, [] ++ l = l. Proof. reflexivity. Qed.  …因为在app的定义中，[]被替换为“scrutinee”（其值被匹配项“仔细检查”的表达式），从而简化了匹配项本身。 此外，与数字一样，对未知列表的可能形状（空或非空）执行案例分析有时也很有用。 Theorem tl_length_pred : foral...

1. 补充完整下面的定义，判断一个集合是否为另一个集合的子集。 Fixpoint subset (s1 : bag) (s2 : bag) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Example test_subset1: subset [1;2] [2;1;4;1] = true. (* FILL IN HERE *) Admitted. Example test_subset2: subset [1;2;2] [2;1;4;1] = false. (* FILL IN...

2.3 2.3-7   4 4.1 最大子数组问题 最大子数组 数组A的和最大的非空连续子数组 我们称这样的连续子数组为最大子数组 使用分治策略的解决方法  Find-Max-Crossing-Subarray(a,low,mid,high) left-sum = -∞ sun = 0 for i = mid downto low sum = sum + A[i] if sum > left-sum left sum = sum max-left = i right-sum = -∞ sun = 0 for j = mid + 1 to high sum = sum + A[j] if ...

知识 Conjunctive Normal Form Definitions： literal  conjunctive normal form (CNF)  Note:  Examples of CNFs:  Not in CNF:  Validity of a Disjunction of Literals Lemma:  Proof:  Satisfiability Definition: 公式ψ是可满足的，如果存在对其命题原子的真值赋值，使得Φ为真。 Proposition: 这是一个简单但非常有用的结果。 Proof:  Useful Identities (Boolean Alge...

数字表 Lists of Numbers 概括成对的定义，我们可以这样描述数字列表的类型：“一个列表要么是空列表，要么是一个数字和另一个列表的一对。” Inductive natlist Inductive natlist : Type := | nil | cons (n : nat) (l : natlist).  Definition mylist 例如，下面是一个三元素列表： Definition mylist := cons 1 (cons 2 (cons 3 nil)).  与pairs一样，用熟悉的编程符号编写列表更方便。下面的声明允许我们使用：：作为中缀cons运算符，方括号作...

在开始本章之前，我们需要从上一章中导入我们的所有定义： From Coq Require Export String. Theorem add_comm : forall n m : nat, n + m = m + n. Proof. induction n as [| n' IHn']. - induction m as [| m' IHm']. -- simpl. reflexivity. -- simpl. rewrite <- IHm'. simpl. reflexivity. - induction m as [| m' IHm']. -- simpl. rewrite -&...

更多练习 More Exercises 20: 3 stars, standard, especially useful (mul_comm) 使用[assert]帮助证明[add_shuffle3]。你还不需要使用归纳法。 Theorem add_shuffle Theorem add_shuffle3 : forall n m p : nat, n + (m + p) = m + (n + p). Proof. (* FILL IN HERE *) Admitted.  Coq代码 Theorem add_shuffle3 : forall n m p : nat, n + (m + p)...

证明中的证明 Proofs Within Proofs 在Coq中，就像在非正式数学中一样，大的证明常常被分解成一系列定理，后面的证明引用了前面的定理。但有时，一个证明将需要一些杂七杂八的事实，这些事实太琐碎，也没有太多的普遍兴趣，以至于懒得给它起自己的顶级名称。在这种情况下，可以方便地在使用“子定理”的地方简单地陈述和证明所需的“子定理”。断言策略允许我们这样做。 Theorem mult_0_plus' : ∀ n m : nat, (0 + n) × m = n × m. Proof. intros n m. assert (H: 0 + n = n). { reflexivity. }...

单独编译 Separate Compilation 在开始本章之前，我们需要从上一章中导入我们的所有定义： From Coq Require Export String. Fixpoint even (n:nat) : bool := match n with | O => true | S O => false | S (S n') => even n' end. Fixpoint leb (n m : nat) : bool := match n with | O => true | S n' => match m with | O => false |...

1.证明下列三条性质  Theorem plus_n_Sm Theorem plus_n_Sm : ∀ n m : nat, S (n + m) = n + (S m). Proof. (* FILL IN HERE *) Admitted.  Coq代码 Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m). Proof. intros n. induction n as [| n' IHn']. - intros m. induction m as [| m' IHm']. -- simpl. reflexivity. --...

知识 窗口函数语法 <窗口函数> over (partition by <用于分组的列名> order by <用于排序的列名>)  <窗口函数>的位置，可以放以下两种函数：  专用窗口函数，比如rank, dense_rank, row_number等   rank 如果有并列名次的行，会占用下一名次的位置 1 1 3 dense_rank 如果有并列名次的行，不占用下一名次的位置 1 1 2 row_number 如果有并列名次的行，也不考虑并列名次的情况 1 2 3   聚合函数，如sum. avg, count, max, min等   ...

知识 SQL 入门 32 #截取出年龄# https://blog.nowcoder.net/n/08a3a1df016d418daabd4a0870f7fb4e 题解 SELECT device_id,SUBSTRING_INDEX(blog_url,'/',-1) AS user_name FROM user_submit