How can I prove `x <> C x`

, where `C`

is a constructor?

```
Inductive ind :=
| C : ind -> ind
| O : nat -> ind.
Fixpoint loop (x:ind) (e:x = C x) {struct x} : False.
Proof.
destruct x as [x'|n].
- apply (loop x');clear loop.
injection e. auto.
- discriminate.
Qed.
Print loop.
```

Otherwise if you already have an irreflexive order relation on your type you can use that lemma.

Without going the whole `Fixpoint`

path, you can just do an `induction`

over `x`

. (This is the same, but it stays closer to a standard pen-and-paper proof.)

Okay, thanks! For some reason I thought there was some easier way, but induction will work! (Now that I think about it, I guess it makes sense that there isn't really an easier way.)

Inspired by what Matthieu suggested, I think my lazy method will just be to define a size metric that's just # of constructors and then run lia.

That's one way indeed. You need some induction, because for coinductive types this would not hold in general ;)

If you have equations around, it can derive the subterm order and show that it is wellfounded, so irreflexive.

Last updated: Sep 30 2023 at 06:01 UTC