Stream: Coq users

Topic: Is there a tactice that disprove constructors are equal

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.

James Wood (Aug 11 2022 at 06:44):

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

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

walker (Aug 11 2022 at 06:48):

No I have hypothesis Constructor x1 x2 x3 = x3

walker (Aug 11 2022 at 06:48):

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

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.

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

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.

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?

James Wood (Aug 11 2022 at 06:54):

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

walker (Aug 11 2022 at 06:58):

I am not sure I understand.

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 z ≻ y. 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.

walker (Aug 11 2022 at 08:33):

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

Gaëtan Gilbert (Aug 11 2022 at 09:10):

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

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: Sep 30 2023 at 06:01 UTC