Stream: Coq users

Topic: Using constructor injectivity


view this post on Zulip John Grosen (May 26 2021 at 14:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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 ;)

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC