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

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? *)


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.


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.

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.

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.

• Inductive datatypes need not have finite depth, consider the countably branching wel-founded trees. You need to be more precise in your statement. (Meven gives a depth-based argument in his argument, where it is essential that the datatype in question only has finite branching.) Commented Mar 14 at 12:38
• @MevenLennon-Bertrand: Sure; but I think Andrej’s point is, there’s no need for an auxiliary notion like numbers or ordinals in this sort of argument — any inductive datatype is its own measure of “size”. Commented Mar 14 at 21:20
• I am whining because I hear again and again the falacy that the elements of inductive types are "finite" or have "finite depth", which is only true under special conditions that ought to qualify such claims. I am just going to continue whining. Commented Mar 14 at 22:06
• From teaching perspective, I very much dislike explaining general inductive types using words such as "finite", "natural number" (or even "ordinal") because that gives the wrong idea that finiteness and natural numbers are prior to notion of inductive datatype. Commented Mar 14 at 22:43
• Depending on what the students know, there will be several ways to explain inductive datatypes: (1) show how the elements of an inductive datatype are generated, in analogy with |, ||, |||, ||||, |||||, ... for numbers (and remarks this is a premathematical way of understanding), (2) compare inductive datatypes to initial free algebras, if students know about them, (3) for philosophers, try to get through them by discussing the fact that the induction principle associated with a datatype is the explanation of what "inductive" means. Commented Mar 14 at 22:47

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.