如何在 Coq 中使用面向对象的概念证明属性答案

【问题标题】：How to prove properties with Object Oriented concepts in Coq如何在 Coq 中使用面向对象的概念证明属性
【发布时间】：2023-03-11 13:10:01
【问题描述】：

有时我有基于 O.O. 的代码。类和接口等概念。例如，一个学生对象有两个 nat 数字，一个是他的学号，一个是他的 GPA。

 public class Student {
    // The private instance variables
    private int studentNumber;
    private int GPA;             
    }

有没有办法在 Coq 中对这些概念进行编码？感谢您的指导。

【问题讨论】：

标签： coq

【解决方案1】：

Coq 具有对字段集建模的记录：

Record student : Set := mkStudent {
  studentNumber : string;
  gpa           : string
}.

您可以使用归纳类型对替代方案和子分类进行建模：

Inductive person : Set :=
  | Student : student -> person
  | Teacher : teacher -> person.

当然，方法可以建模为函数：

Definition age (p: person) : nat :=
  match p with
  | Student s => ..
  | Teacher t => ..

虽然这不是最干净的方式，而且就地修改（可变性）需要通过 monad 来处理；它可以工作。

请记住，要获得完整的证明，您需要提供到 OOP 模型的映射并证明映射是正确/合理的。

【讨论】：

另外，相关问题：stackoverflow.com/questions/32796264/…
谢谢你，mpetruska。您能否就就地修改（可变性）和映射到我的 OOP 模型的含义写下或为我提供参考。我很感激。
例如，在 java 中，此方法修改当前对象中的字段值：public void setNumber(string newValue) { this.studentNumber = newValue }。在纯函数式编程中，所有值都是不可变的，相反，您可以创建一个函数，使用更新的字段生成新记录：withNumber : student -> string -> student