Stream: Coq users

Topic: Is there a tactice that disprove constructors are equal


view this post on Zulip walker (Aug 11 2022 at 06:41):

Is there a tactic that automatically solve Something like

forall n, S n = n

I am not strictly focused on natural numbers, but the idea that a symbolic parameter to the constructor cannot equal the constructor with parameters if they are the same type.

view this post on Zulip James Wood (Aug 11 2022 at 06:44):

Do you mean something like forall n, S n = n -> ...?

view this post on Zulip James Wood (Aug 11 2022 at 06:46):

(If you had a hypothesis H : forall n, S n = n, you'd probably feed in 0 and then discriminate.)

view this post on Zulip walker (Aug 11 2022 at 06:48):

No I have hypothesis Constructor x1 x2 x3 = x3

view this post on Zulip walker (Aug 11 2022 at 06:48):

now this is obviosly false, regardless of what are the details of Constructor.

view this post on Zulip Guillaume Melquiond (Aug 11 2022 at 06:48):

Proving S n <> n is eventually an induction proof, since it critically relies on n being "finite". So, I don't think you can make a shorter proof than using the whole induction + discriminate + injection machinery.

view this post on Zulip walker (Aug 11 2022 at 06:49):

Alright, that is going to be lots of pain because there are lots of cases here. but thanks. I will do proofs manually

view this post on Zulip Guillaume Melquiond (Aug 11 2022 at 06:53):

You can presumably reduce the number of cases by defining a projection function f x := match x with Constructor x1 x2 x3 => Some x3 | _ => None end, so that you have only two constructors left.

view this post on Zulip James Wood (Aug 11 2022 at 06:53):

I've never looked into it, but doesn't the general machinery for generating syntactic accessibility relations give us something usable for this case?

view this post on Zulip James Wood (Aug 11 2022 at 06:54):

Like, we should have S n ≻ n and x ≻ y → x <> y.

view this post on Zulip walker (Aug 11 2022 at 06:58):

I am not sure I understand.

view this post on Zulip James Wood (Aug 11 2022 at 08:18):

As I say, I've never looked into it, so maybe what I'm talking about only exists in the metatheoretic analysis rather than internally in the implementation. But at some level, Coq (specifically, its termination checker) knows of a well founded relation ≻ for each inductive type such that C x y zy. This justifies taking a least fixed point when there's an argument such that all recursive calls are on smaller terms. But also, such a relation is always irreflexive, so it gives you what you wanted.

view this post on Zulip walker (Aug 11 2022 at 08:33):

I see, In any case I just finished the manual implementation ;)

view this post on Zulip Gaëtan Gilbert (Aug 11 2022 at 09:10):

Derive Subterm from equations may be helpful for this sort of thing

view this post on Zulip Matthieu Sozeau (Sep 19 2022 at 14:29):

Indeed, that’s how Equations solves such goals (from the unification viewpoint they are occur-check failures). The subterm relation being well founded is the only induction proof you need.


Last updated: Feb 06 2023 at 13:03 UTC