【实践】haskell、coq基本语法

一、注释

--单行注释
{-多行注释-}

二、输入输出（略）

三、运算符（略）

四、表达式

haskell无语句。

3::Float--其中::符号说明类型，这句的意思就是表示了一个浮点数3
sort[3,8,1,4]--函数不必带括号，sort表排序
--多参数不要加逗号
--在其他语言中的语句，在haskell中也只是表达式，例如let in表达式可以跨行写成下面这样
let x=3*a
    y=4*a
in sqrt(x^2+y^2)

条件表达式

情况分析表达式

守卫表达式

匹配模式

五、声明

由于haskell无变量，因此用绑定代替。

addOne::Int->Int
addOne x=x+1--这句addOne是函数，第一个x是参数的模式
welcomeMsg::String--welcomeMsg的类型是String
welcomeMsg='hello world'--等号表示绑定，当要用helloworld时使用welcomMsg即可
module Main where--模块声明
import Data.list--导入声明

作用域：能够看见x的区域叫x的作用域。一个绑定的作用域可通过词法分析得出。

let x=1
in let y=x*2--x可见
    in x+y--x、y可见

六、函数

普通函数与中缀函数：

函数分为普通函数和中缀函数。也就是说运算符也是函数。

优先级：普通函数优先级高于中缀函数。

结合性：不结合、左结合、右结合。分0-9级。不结合的中缀函数不能连写。

函数的格式：

--函数名::参数1的类型->参数2的类型->结果的类型
--函数名 参数1 参数2=函数体
add,sub::Int->Int->Int
add a b = a+b
sub a b = a-b

库函数：

预加载库prelude

字符与位运算的库函数

parsec库

quickCheck库

递归函数：

扩展递归

尾递归

互调递归

不动点递归

无基本条件递归

高阶函数：指以其他函数参数或者返回其他函数为结果的函数。

复合函数：

七、数据类型

haskell是强类型语言。

布尔Bool

字符Char：有字符、ASCII码值两种表示。

字符串类型String：是Char的列表。

有符号整数Int：正负符号，有基于编译的取值范围。

无符号整数Word：有基于编译的取值范围，相当于C或java的unsign int。

任意精度整数Integer：可表示大数，它的取值范围由硬件决定。

小数Float、Double：单双精度。

有理数Rational：例如，分数是有理数，分数用%隔开分子和分母。

元组Tuple：元组中的元素叫元组的元件component。类型和数量都不可变。

列表List：元素类型唯一，即类型不可变，存了字符就不能存数。

还可以自行定义数据类型。

枚举类型：

构造类型：

参数化类型：

递归类型：

杂合定义类型：

拉链类型zipper

空类型

八、类型类

类型类就是类型间的共性。例如布尔型和数值型都可以比较是否相等。

相等类型类Eq

有序类型类Ord

枚举类型类Emum

有界类型类Bounded

数字类型类Num

可显示类型类Show

可以自主定义类型类。

函子类型类Functor

应用函子类型类Applicative

选择类型类Alternative

读类型类Read

折叠类型类Foldable

幺半群类型类Monoid

单子类型类Monad

九、算法与问题（略）

十、惰性求值（略）

十一、范畴论（略）

❤

既然是GPT写的代码，那么不保证代码正确性。

一、归谬法

AI：嗨，我可以教您如何使用Coq来证明归谬法。首先，您需要定义要证明的定理。然后，您需要假设它是错误的，并且证明这个假设会导致一个矛盾。最后，您可以证明这个矛盾的结论是不可能的，因此证明了定理的正确性。以下是一个证明归谬法的示例：

Theorem MyTheorem: forall n : nat, n > 0 -> n + 1 > 0.

Proof. 
  intros n H.
  (* Make an assumption that the theorem is false *)
  assume H_false : n + 1 ≤ 0.
  (* Deduce a contradiction from the assumption *)
  apply le_n_S in H_false.
  rewrite -> H in H_false.
  inversion H_false.
Qed.

二、反证法

如何证明反证法

AI：嗨，我可以教您如何使用Coq来证明反证法。首先，您需要在Coq中定义要证明的定理。然后，您将需要做出一个假设，即假定要证明的定理是错误的。接下来，您将需要证明根据这个假设，可以得出一个矛盾的结论。最后，您可以证明这个矛盾的结论是不可能的，因此证明了定理的正确性。

以下是一个证明反证法的示例：

Theorem MyTheorem: forall n : nat, n + 1 = 0 -> False.

Proof. 
  intros n H.
  (* Make an assumption that the theorem is false *)
  assume H_false : n + 1 ≠ 0.
  (* Deduce a contradiction from the assumption *)
  rewrite -> H in H_false.
  (*

三、三段论

嗨，我可以帮助你写一段Coq证明三段论代码。首先，您需要定义您要证明的定理。然后，您将需要分为三个部分来证明它：基本情况，归纳假设，以及归纳步骤。这是一个示例：

Theorem MyTheorem: forall n : nat, n + 0 = n.
Proof.
  induction n.
  - (* Base *)
    reflexivity.
  - (* Induction Hypothesis *)
    intros.
  - (* Induction Step *)
    simpl. rewrite -> IHn. reflexivity.
Qed.

四、谓词演算

嗨，我可以教您如何使用Coq来证明谓词演算。首先，您需要定义要证明的定理。然后，您需要假设它是正确的，并且证明这个假设会导致一个结论。最后，您可以证明这个结论是正确的，因此证明了定理的正确性。以下是一个证明谓词演算的示例：

Theorem MyTheorem: forall P Q : Prop, (P -> Q) -> P -> Q.

Proof. 
  intros P Q H1 H2.
  (* Make an assumption that the theorem is true *)
  assume H : P -> Q.
  (* Deduce a conclusion from the assumption *)
  apply H in H2.
  exact H2.
Qed.

五、真值表

嗨，我可以教您如何使用Coq来证明真值表法。首先，您需要定义要证明的定理。然后，您需要分析真值表，并证明每一种情况都与定理结论相一致。最后，您可以证明每一种情况都是正确的，因此证明了定理的正确性。以下是一个证明真值表法的示例：

Theorem MyTheorem: forall P Q : Prop, (P -> Q) <-> (~Q -> ~P).

Proof. 
  intros P Q. split.
  - intros H1. intros H2.
    (* Make an assumption that the theorem is true *)
    assume H3 : P.
    (* Deduce a conclusion from the assumption *)
    apply H1 in H3.
    contradiction. 
  - intros H1. intros H2.
    (* Make an assumption that the theorem is true *)
    assume H3 : ~Q.
    (* Deduce a conclusion from the assumption *)
    apply H1 in H3.
    exact H

六、coq与python对比

# Coq代码
Definition Contains_rum_and_lemon (cocktail : list (string * nat)) 
: Prop := 
  (exists l : string, l = "朗姆酒" /\ In l (map fst cocktail)) /\ 
  (exists l : string, l = "柠檬" /\ In l (map fst cocktail)).

Definition Contains_rum_no_lemon (cocktail : list (string * nat)) 
: Prop := 
  (exists l : string, l = "朗姆酒" /\ In l (map fst cocktail)) /\ 
  ~(exists l : string, l = "柠檬" /\ In l (map fst cocktail)).

# Python代码
def contains_rum_and_lemon(cocktail):
    for i in range(len(cocktail)):
        if cocktail[i][0] == '朗姆酒' and cocktail[i][1] == '柠檬':
            return True
    return False

def contains_rum_no_lemon(cocktail):
    has_rum = False
    has_lemon = False
    for i in range(len(cocktail)):
        if cocktail[i][0] == '朗姆酒':
            has_rum = True
        if cocktail[i][1] == '柠檬':
            has_lemon = True
    return has_rum and not has_lemon

七、带注释的coq

Coq是一种面向数学证明的函数式编程语言，它使用类型检查来确保正确性。Coq中有多种数据类型，包括整数、布尔值、元组、列表、记录以及自定义的类型。

Coq没有专门的循环语句，但可以使用递归函数来实现循环。例如，可以使用“fix”关键字定义一个递归函数，它将会重复执行指定的操作，直到数据满足某种条件为止。

这是一段带注释的Coq代码：

 
(*这是一段注释*)
Fixpoint add (n m : nat) : nat :=
  match n with#检查n的值
  | 0 => m#如果n为0返回m
  | S p => S (add p m)#如果n不为0返回s，p为n-1，减完再算m
  end.

(* 函数将两个自然数相加 *)

这段代码使用“Fixpoint”关键字定义一个名为“add”的递归函数，它接受两个自然数n和m作为参数。然后使用“match”语句来检查n的值，如果n为0，则返回m。如果n不为0，则返回S(add p m)，其中p为n减1的结果。

这不是循环语句，而是一个递归函数。S函数会根据n的值来决定执行的次数。nat是Coq中的自然数类型，用于表示非负整数。