How to prove non-existence of terms that contain themselves in Coq

Question

Why can't inversion figure out that it isn't structurally possible for a term to contain itself? Here's a basic example:

Inductive test_type : Type :=
| Base 
| Arrow (i o : test_type).

Theorem should_be_easy : forall T,
  T <> Arrow T T.
Proof.
  intros T contra. inversion contra. (* why doesn't this solve the goal? *)
Admitted.

How would I go about solving this proof? The only evidence I have, contra, is just an equality, so I can't induct on it. Additionally, induction on T results in a similarly-recursive set of evidence in the inductive case that doesn't let me make progress on the goal.

I thought the tactic existed to deal with matters of constructor equivalence to some degree. For example, it solves this trivial constructor inequality:

Theorem xyz : true <> false.
Proof. intro contra. inversion contra. Qed.

Answer 1

The way to prove such a thing is by induction. For a warm-up, let us show that there is no natural number n equal to its successor.

Theorem: For all $n \in \mathbb{N}$, $n \neq n + 1$.

Proof. By induction on $n$:

• Base case: $0 \neq 1$ is obvious.
• Induction step: assume $n \neq n + 1$. If we had $n + 1 = n + 2$ then we would get $n = n + 1$, which contradicts the induction hypothesis. $\Box$.

Here is the Coq transcript:

Lemma cow : forall n, n <> S n.
Proof.
  induction n as [|n IH].
  - auto.
  - intro E ; injection E.
    exact IH.
Qed.

Your example is dealt with in the same fashion:

Inductive test_type : Type :=
| Base
| Arrow (i o : test_type).

Theorem should_be_easy : forall T,
  T <> Arrow T T.
Proof.
  induction T as [|T1 IH1 T2 IH2].
  - discriminate.
  - intro E ; injection E ; intros.
    apply IH1.
    congruence.
Qed.

The tactics discriminate and injection were used to take into account the fact that constructors are injective.

Answer 2

Basically, because inversion is not able to do induction, which is necessary to deduce the kind of contradictions you are after. However, you can prove your goal with an easy induction.

Theorem should_be_easy : forall T T',
  T <> Arrow T T'.
Proof.
  intros T T' contra.
  induction T in T', contra |- *.
  - inversion contra.
  - inversion contra ; subst ; eauto.
Qed.

If you end up encountering this and similar kind of goals often, it might be useful to automate it. One way is to deduce "size problems" with such hypothesis, like this:

Require Import Lia.

Fixpoint size (t : test_type) : nat :=
  match t with
  | Base => 1
  | Arrow i o => 1 + size i + size o
  end.

Ltac absurd_self_contain :=
  exfalso ;
  match goal with
    | H : @eq test_type _ _ |- _ => apply (f_equal size) in H; cbn in H ; lia
  end.

Theorem should_be_easy' T : T <> Arrow T T.
Proof.
  intros ?.
  absurd_self_contain.
Qed.

The tactic will try and derive an inconsistency from equalities between types in your context, by turning them in size equalities, and using the arithmetic solver lia to deduce that these equalities are absurd.

Answer 3

This is only true because inductive data "has no infinite descending chains." (i.e. for simple inductive types, it has finite depth). If test_type was co-inductive, such a type (containing itself) would be able to exist. So to show this, we need to reason about this property of test_type, which means we need to do an induction. And proving this by induction is routine:

Lemma one_recursive_occurance_is_easier T T2 :
  T <> Arrow T T2.
Proof.
  induction T as [|T1L IHL T1R _] in T2|-*.
  - intros [=].
  - intros [= Heq1 _].
    eapply IHL, Heq1.
Qed.

Theorem should_be_easy T :
  T <> Arrow T T.
Proof.
  apply one_recursive_occurance_is_easier.
Qed.

Inversion only destructs (but in a way that keeps equalities of indices), so it can not do inductive reasoning.

Answer 4

Below is such a result for an inductive type, that of nat-indexed well founded trees that does not have a notion of height (in the natural numbers).

Inductive wft : Type :=
  | leaf : wft
  | node : (nat -> wft) -> wft.

Lemma wft_neq_rec t : 
  match t with 
  | leaf => True
  | node f => forall n, f n = t -> False
  end.
Proof.
  induction t as [ | f IHf ]; trivial.
  intros n Hn.
  specialize (IHf n).
  case_eq (f n); rewrite Hn in *; [ easy | ].
  intros g; inversion 1; subst g; eauto.
Qed.

Theorem wft_neq f n : f n <> node f.
Proof. exact (wft_neq_rec (node _) _). Qed.

Now you can get more properties of inequality using the well foundedness of the sub-term order, and hence the irreflexivity of its transitive closure:

Require Import Wellfounded Relations.

Inductive wft : Type :=
  | leaf : wft
  | node : (nat -> wft) -> wft.

Inductive sub_wft : wft -> wft -> Prop :=
  | swft_intro n f : sub_wft (f n) (node f).

Fact sub_wft_inv s t :
     sub_wft s t 
  -> match t with
     | leaf => False
     | node f => exists n, s = f n
     end.
Proof. intros []; eauto. Qed.

Fact wf_sub_wft : well_founded sub_wft.
Proof.
  intro t.
  induction t; constructor;
    intros ? []%sub_wft_inv; subst; trivial.
Qed.

Fact wf_irrefl {X} {R : X -> X -> Prop} : 
  well_founded R -> forall x, ~ R x x.

Proof.
  intros H x.
  induction x as [ x IHx ] using (well_founded_induction H).
  intro; now apply (IHx x).
Qed.

Fact wf_ct_swft : well_founded (clos_trans _ sub_wft).
Proof. apply wf_clos_trans, wf_sub_wft. Qed.

Theorem wft_neq_node2 f g n m: 
   f n = node g -> g m = node f -> False.
Proof. 
  intros E1 E2.
  apply (wf_irrefl wf_ct_swft (node f)).
  constructor 2 with (node g); constructor 1.
  + rewrite <- E2; constructor.
  + rewrite <- E1; constructor.
Qed.