gpt4 book ai didi

coq - 在 Ltac 中匹配一元数据构造函数

转载 作者:行者123 更新时间:2023-12-04 23:36:51 25 4
gpt4 key购买 nike

我正在做一些关于在 Coq 中形式化简单类型的 lambda 演算的练习,并且想使用 Ltac 自动化我的证明。在证明进步定理时:

Theorem progress : forall t T,
empty |-- t \in T -> value t \/ exists t', t ==> t'.

我想出了这段 Ltac 代码:

Ltac progress_when_stepping :=
(* right, because progress statement places stepping on the right of \/ *)
right;
(* use induction hypotheses *)
repeat
match goal with
| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 _ ==> _ ] =>
induction H; auto
| [ H : _ -> value _ \/ exists _, ?t2 ==> _, H0 : value ?t1 |-
exists _, ?C ?t1 ?t2 ==> _ ] =>
induction H; auto
| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] =>
induction H; auto
end.

==> 表示单步评估(通过小步语义)。每个匹配案例的意图是:

  1. 当我们有一个假设表明构造函数步骤中的第一项时,匹配任何二元构造函数。
  2. 当我们假设构造函数步骤中的第二项和构造函数中的第一项已经是一个值时,匹配任何二元构造函数
  3. 当我们有一个假设表明构造函数步骤中的项时,匹配任何一元构造函数。

但是,从这段代码的行为来看,第三种情况似乎也匹配二进制 构造函数。我如何将其限制为仅实际匹配一元构造函数?

最佳答案

问题是 ?C 匹配 ?C0 ?t0 形式的术语。你可以做一些二次匹配来排除这种情况。

match goal with

| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] =>
match C with
| ?C0 ?t0 => fail
| _ => induction H; auto
end
end.

关于coq - 在 Ltac 中匹配一元数据构造函数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/37067923/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com