如何使用默认或或子句之类的东西在COQ中使用COQ中的比赛？

发布于 2025-01-23 13:29:00 字数 863 浏览 3 评论 0原文

如何在Coq中编写类似于此的开关状态（Rust）？特别是我是Curios如何合并Coq中的分支以产生相同的输出，并通过一些默认实现来耗尽其余分支。

type Voltages = u32; // in coq is similar to Definition Voltages := R.
type Timestamp = u32; // in coq is similar to Definition Timestamp := R.

const TD: Timestamp = 2; // dummy value cuz rust, in coq would be Variable TD : Timestamp.

enum Pin {
    Ground(bool),
    VoltageIn(bool),
    Threshold,
    Discharge,
    Output,
    Trigger,
    Reset,
    CtrlVoltage
}

impl Pin {
    fn evaluate() -> bool { // dummy for some other functions and predicates
        true
    }
}

fn is_high(p: Pin) -> bool {
    match p {
        Pin::Ground(value) | Pin::VoltageIn(value) => value, // how to grab 2 options in one match in coq?
        _ => Pin.evaluate() // how to exhaust the options in coq?
    }
}

原文

How can i write a switch state similar to this one (in rust), in coq?
In particular I'm curios how to merge branches in coq to produce same output, and exhaust the remaining branches via some default implementation.

type Voltages = u32; // in coq is similar to Definition Voltages := R.
type Timestamp = u32; // in coq is similar to Definition Timestamp := R.

const TD: Timestamp = 2; // dummy value cuz rust, in coq would be Variable TD : Timestamp.

enum Pin {
    Ground(bool),
    VoltageIn(bool),
    Threshold,
    Discharge,
    Output,
    Trigger,
    Reset,
    CtrlVoltage
}

impl Pin {
    fn evaluate() -> bool { // dummy for some other functions and predicates
        true
    }
}

fn is_high(p: Pin) -> bool {
    match p {
        Pin::Ground(value) | Pin::VoltageIn(value) => value, // how to grab 2 options in one match in coq?
        _ => Pin.evaluate() // how to exhaust the options in coq?
    }
}

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

傲性难收 2025-01-30 13:29:00

在COQ中，您可以分开几个通过管道绑定相同变量的分支，并且仅使用一个右侧值。
您也可以将下划线作为通配符来捕获所有剩余案例。

Inductive t :=
| A (x : nat)
| B (x : nat) (y : bool)
| C (x : unit).

Definition foo (c : t) :=
  match c with
  | A x | B x _ => x
  | _ => 0
  end.

In coq you can separate several branches that bind the same variables by a pipe and use only one right-hand side value.
You can also use the underscore as a wildcard to catch all remaining cases.

Inductive t :=
| A (x : nat)
| B (x : nat) (y : bool)
| C (x : unit).

Definition foo (c : t) :=
  match c with
  | A x | B x _ => x
  | _ => 0
  end.

回复收藏 0 原文

~没有更多了~