Stream: Coq users

Topic: Using constructor injectivity

John Grosen (May 26 2021 at 14:39):

How can I prove `x <> C x`, where `C` is a constructor?

Gaëtan Gilbert (May 26 2021 at 14:51):

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

Matthieu Sozeau (May 26 2021 at 14:52):

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

Guillaume Melquiond (May 26 2021 at 14:53):

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

John Grosen (May 26 2021 at 15:06):

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

John Grosen (May 26 2021 at 15:10):

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.

Matthieu Sozeau (May 26 2021 at 15:11):

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

Matthieu Sozeau (May 26 2021 at 15:13):

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

Last updated: Jun 14 2024 at 19:02 UTC