时间戳

首页 > 解决方案 > 编码有序集

coq - 编码有序集

问题描述

标签： coq

解决方案

(* The definition of mydata again, for completeness *)
Inductive mydata : Set :=
| part1 : mydata
| part2 : mydata
| part3 : mydata.

您可以将比较定义为布尔函数mydata -> mydata -> bool：

Definition le_mydata_dec (d1 d2 : mydata) : bool :=
  match d1, d2 with
  | part1, _ => true
  | part2, (part2 | part3) => true
  | part3, part3 => true
  | _, _ => false
  end.

并由此推导出比较关系mydata -> mydata -> Prop（这只是一种方式，有时将其定义le_mydata为Inductive命题更方便）。

Definition le_mydata (d1 d2 : mydata) : Prop :=
  le_mydata_dec d1 d2 = true.

映射函数是相同的（f为简洁起见重命名）：

(* a sample function from nat to mydata which is always increasing or not changing*)
Definition f
  (a1:nat): mydata :=
        match a1 with 
           |0=> part1
           |S(0) => part2
           |_ => part3
         end.

现在这是单调性：

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> le_mydata (f a1) (f a2).
Proof.
Abort.

您可以使用符号来替换le_mydata更漂亮的<=. 在这里，我们注意不要隐藏预先存在的符号<=进行比较nat，通过将这个新符号分配给一个新的范围mydata_scope，用 key 分隔mydata。

Infix "<=" := le_mydata : mydata_scope.
Delimit Scope mydata_scope with mydata.
(* now we can write  (x <= y)%mydata  instead of  le_mydata x y *)

再次使用该符号的单调性定理：

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> (f a1 <= f a2)%mydata.
Proof.
Abort.

推荐阅读