Search code examples
coqcoq-tactic

Show that a term is not equal to a strictly larger term

Consider the following toy development:

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

Is this truly the most straightforward way to determine that this holds? Do I need to perform an induction every time I want to do something like this?

Solution

  • For types this simple, you could also define a size function that computes the height of the tree defining the type. Then A = amp A B would reduce to something like

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

    which you should be able to discharge with lia.