时间戳

首页 > 解决方案 > 表明一个术语不等于一个严格更大的术语

coq - 表明一个术语不等于一个严格更大的术语

问题描述

考虑以下玩具开发：

Require Import Coq.Strings.String.

Inductive SingProp: Set :=
| Var: string -> SingProp
| plus: SingProp -> SingProp -> SingProp
| amp: SingProp -> SingProp -> SingProp.

Goal forall A B, A <> amp A B.
Proof.
  intros A. induction A.
  - intros B H. inversion H.
  - intros B H. inversion H.
  - intros B H. inversion H. apply (IHA1 _ H1).

这真的是确定这是否成立的最直接的方法吗？每次我想做这样的事情时都需要进行归纳吗？

标签： coqcoq-tactic

解决方案

对于这种简单的类型，您还可以定义一个size函数来计算定义该类型的树的高度。然后A = amp A B会减少到类似的东西

size A = 1 + max (size A) (size B)

你应该能够用lia.

推荐阅读