Theorem rev_exercise1 : forall (l l' : list nat), l = rev l' -> l' = rev l. Proof. intros l l' eq1. rewrite -> eq1. Search rev. symmetry. apply (rev_involutive nat). (* rev_involutive: forall (X : Type) (l : list X), rev (rev l) = l *) Qed.
上文第9行的 nat 可加可不加,coq 可以自动推断 Type 是 nat。
练习:3 星, standard, optional (apply_with_exercise)
1 2 3 4 5 6 7 8
Example trans_eq_exercise : forall (n m o p : nat), m = (minustwo o) -> (n + p) = m -> (n + p) = (minustwo o). Proof. intros n m o p eq1 eq2. apply trans_eq with (m). apply eq2. apply eq1. Qed.
练习:3 星, standard (injection_ex3)
1 2 3 4 5 6 7 8 9 10 11 12 13 14
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X), x :: y :: l = z :: j -> j = z :: l -> x = y. Proof. intros X x y z l j. intros H1 H2. injection H1 as H1' H1''. rewrite H1'. rewrite <- H1'' in H2. injection H2 as H2'. symmetry. apply H2'. Qed.
另一种实现(使用apply with(实际上写起来没什么差别):
1 2 3 4 5 6 7 8 9 10 11 12 13
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X), x :: y :: l = z :: j -> j = z :: l -> x = y. Proof. intros X x y z l j. intros H1 H2. injection H1 as H1' H1''. rewrite <- H1'' in H2. injection H2 as H2'. apply trans_eq with (z). apply H1'. symmetry. apply H2'. Qed.
练习:1 星, standard (discriminate_ex3)
1 2 3 4 5 6 7 8 9
Example discriminate_ex3 : forall (X : Type) (x y z : X) (l j : list X), x :: y :: l = [] -> x = z. Proof. intros X x y z l j. intros H. discriminate H. Qed.
练习:2 星, standard (eqb_true)
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Theorem eqb_true : forall n m, n =? m = true -> n = m. Proof. intros n. induction n as []. - destruct m as[]. ++ reflexivity. ++ discriminate. - destruct m as[|m']. ++ discriminate. ++ intros H. f_equal. simplin H. apply IHn in H. apply H. Qed.
主要是我一开始没看懂上面例题在做什么,intros m n 之后最后一个结论证不出来,应该只intro n,之后 m 是 forall m,所以可以随意取值(应该是这个道理?)。
Theorem plus_n_n_injective : forall n m, n + n = m + m -> n = m. Proof. intros n. induction n as [| n']. - destruct m as[]. simpl. reflexivity. discriminate. - destruct m as[]. discriminate. intros eq. simplin eq. apply S_injective' in eq. rewrite <-plus_n_Sm in eq. rewrite <-plus_n_Sm in eq. apply S_injective' in eq. f_equal. apply IHn' in eq. apply eq. Qed.
主要就是使用前面的S_injective证明 Sn 单射之后把 S (n' + S n') 转化为 n' + S n' 再用 plus_n_Sm 就行。
练习:3 星, standard, recommended (gen_dep_practice)
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X), length l = n -> nth_error l n = None. Proof. intros n X l. generalizedependent l. induction n as []. - destruct l. reflexivity. discriminate. - destruct l. discriminate. intros H. simpl. simplin H. apply S_injective in H. apply IHn in H. apply H. Qed.
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2, split l = (l1, l2) -> combine l1 l2 = l. Proof. intros X Y l. unfold combine. induction l as [| n l' IHl']. - simpl. intros. injection H as H1 H2. rewrite <- H1. reflexivity. - simpl. intros. destruct n as [x y]. destruct (split l') as [lx ly]. injection H as H1 H2. rewrite <- H1. rewrite <- H2. f_equal. apply IHl'. reflexivity. Qed.
# SSL configuration # # listen 443 ssl default_server; # listen [::]:443 ssl default_server; # # Note: You should disable gzip for SSL traffic. # See: https://bugs.debian.org/773332 # # Read up on ssl_ciphers to ensure a secure configuration. # See: https://bugs.debian.org/765782 # # Self signed certs generated by the ssl-cert package # Don't use them in a production server! # # include snippets/snakeoil.conf;
root /var/www/html;
# Add index.php to the list if you are using PHP index index.html index.htm index.nginx-debian.html;
server_name _;
location / { # First attempt to serve request as file, then # as directory, then fall back to displaying a 404. try_files $uri $uri/ =404; }
# pass PHP scripts to FastCGI server # #location ~ \.php$ { # include snippets/fastcgi-php.conf; # # # With php-fpm (or other unix sockets): # fastcgi_pass unix:/var/run/php/php7.4-fpm.sock; # # With php-cgi (or other tcp sockets): # fastcgi_pass 127.0.0.1:9000; #}
# deny access to .htaccess files, if Apache's document root # concurs with nginx's one # #location ~ /\.ht { # deny all; #} }
然后起服务,发现 403 forbidden,把 nginx.conf 第五行从 user xxxx 改成 user root 即可(root 权限关我锤子事,反正又不在我电脑上部署)