lengyijun

Step 1 - Install and Configure dnscrypt-proxy

sudo su
pacman -S dnscrypt-proxy

cd /etc/dnscrypt-proxy/

lengyijun

Require Import
  Coq.FSets.FMapAVL
  Coq.FSets.FMapFacts
  Coq.Structures.OrderedTypeEx
  PeanoNat.

Module Import M := FMapAVL.Make(Nat_as_OT).
Print Module M.
Check (M.t (list nat)).

lengyijun

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <=? y1
        then x1::(merge xs y)

lengyijun

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <? y1
        then x1::(merge xs y)

lengyijun

open import Data.String as String using (String; fromList)
open import Data.Nat              using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
open import Data.Nat.Properties  
open import Data.Bool             using (Bool; true; false; if_then_else_)
open import Data.List   hiding (merge; partition)
open import Data.List.Properties  using (map-id; map-compose)
open import Data.Product          using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
open import Data.Sum   as Sum     using (_⊎_; inj₁; inj₂; map)
open import Data.Unit             using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)

lengyijun

(** * Merge:  Merge Sort, With Specification and Proof of Correctness*)

From VFA Require Import Perm.
From VFA Require Import Sort.
From Coq Require Import Recdef.  (* needed for [Function] feature *)

(** Mergesort is a well-known sorting algorithm, normally presented
    as an imperative algorithm on arrays, that has worst-case
    O(n log n) execution time and requires O(n) auxiliary space.

lengyijun

(** * Merge:  Merge Sort, With Specification and Proof of Correctness*)

From VFA Require Import Perm.
From VFA Require Import Sort.
From Coq Require Import Recdef.  (* needed for [Function] feature *)

(** Mergesort is a well-known sorting algorithm, normally presented
    as an imperative algorithm on arrays, that has worst-case
    O(n log n) execution time and requires O(n) auxiliary space.

lengyijun

open import Data.String as String using (String; fromList)
open import Data.Nat              using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
open import Data.Nat.Properties  
open import Data.Bool             using (Bool; true; false; if_then_else_)
open import Data.List   hiding (merge; partition)
open import Data.List.Properties  using (map-id; map-compose)
open import Data.Product          using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
open import Data.Sum   as Sum     using (_⊎_; inj₁; inj₂; map)
open import Data.Unit             using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)

lengyijun

open import Data.Nat         using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_; _≤_; _<_; _⊔_ )
open import Data.Fin         using (Fin; zero; suc; toℕ; fromℕ;  fromℕ<) renaming (splitAt to FinSplitAt)
open import Data.Maybe as Maybe
open import Relation.Binary.PropositionalEquality
open import Data.Unit        using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)
open import Relation.Nullary      using (¬_; Dec; yes; no)
open import Induction.WellFounded
open import Relation.Binary hiding (_⇒_)
open import Data.Nat.Induction

lengyijun

不要用rar压缩.用zip或者tar.gz

不要把编译后的文件传上来,节省网络中心的压力.一般写一个cpp就够了,很难想象需要.h和其他cpp

想办法降低复杂度.prime复杂度不到 根号n  的都扣了2分 
O(n/2)=O(n),只循环一半没用的

求个阶乘的事情,不要用递归,效率会很差的.用循环写.随机扣了分