Показать, что термин не равен строго большему

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.