John Grosen (May 26 2021 at 14:39): 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.
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: Oct 13 2024 at 01:02 UTC