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.

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

?

(If you had a hypothesis `H : forall n, S n = n`

, you'd probably feed in `0`

and then discriminate.)

No I have hypothesis `Constructor x1 x2 x3 = x3`

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

.

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.

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

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.

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

Like, we should have `S n ≻ n`

and `x ≻ y → x <> y`

.

I am not sure I understand.

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.

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

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

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