wiki:Cog

Coq学习笔记 - Functional Programming Language

源代码文件似乎都是以'.v'为扩展名,每条语句以'.'结束

even偶数,odd奇数,exponential function指数函数 power幂,factorial function阶乘函数

Example Theorem Lemma Fact Remark 含义差不多都表示定义一个定理

forall n : nat表示条件,对于所有的自然数

intros simpl reflexivity is used between [Proof] and [Qed]表示证明的策略tactics. intros H.(H表示假设条件),rewrite -> H.将假设条件H代入目标等式重写等式。 destruct n as [| n'].?

  • 定义类型:将一组数值Inductive(归纳)为一个类型
Inductive type_name : Type := 
  | value1 : type_name
  | ...
  | valueN : type_name.
  • 定义函数:admit空语句;Fixpoint代替Definition 表示定义一个递归函数
Definition function_name(参数d:类型名day) : 返回值类型day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.
多个参数的函数
Definition function_name(参数d1:类型名day) (参数d2:类型名day) : 返回值类型day :=
   admit.
也可以同类型参数写在一起,如:
Fixpoint mult (n m : nat) : nat :=
  match n with
    | O => O
    | S n' => plus m (mult n' m)
  end.
  • 执行函数:(函数可以嵌套调用)
  1. 评估计算方式执行函数
Eval compute in (函数名 参数).
Eval compute in (next_weekday friday).
Eval compute in (函数名(函数名 参数)).
Eval compute in (next_weekday (next_weekday saturday)).
  1. 证明函数是否等于预期结果:Example, simpl,reflexivity(反射性)都是什么含义?
Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
其中Proof(证明开始)Qed(证明完毕)
  1. 什么意思?we can ask Coq to "extract," from a Definition, a program in some other, more conventional, programming language (OCaml, Scheme, or Haskell) with a high-performance compiler. This facility is very interesting, since it gives us a way to construct fully certified programs in mainstream languages. Indeed, this is one of the main uses for which Coq was developed.
  1. 模块定义
Module Playground1.
Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.
Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.
End Playground1.

参考资料

Last modified 4 years ago Last modified on 03/03/14 16:06:52