表示一项不等于严格更大的一项

Question

考虑以下玩具开发：

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).

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

Answer 1

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

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

您应该可以用lia放电。