Variant of discriminate that refutes statements such as "S n <= 0"

[herbelin]

Is your feature request related to a problem?

Tactic discriminate is able to refutes S n = 0 and it does it by mapping S n to True and 0 to False in the one-constructor inductive family eq. Somehow, it could do the same for inductive families with more than one constructor.

Proposed solution

Assume an inductive family I with parameters γ:Γ and dependent arity forall δ:Δ, sort. Assume a proof of I params args. Assume constructor Ci of I to instantiate the arity with argsi(γ).

The idea is to build an elimination F(δ) of the following form:

match δ with
| args => False
| argsi(params) => True (* for each i *)
end

If the pattern structure underlying args is distinct from the pattern structure underlying each argsi(params), we are done (this is the direct generalization of discriminate to more than one constructor). For instance, for:

Inductive le (n : nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m.

the pattern-matching F(m) associated to S p <= 0 is:

match m with
| 0 => False
| S _ => True (* le_n *)
| S _ => True (* le_S *)
end

and dependent destruction of the proof of S p <= 0 using the clause in _ <= m return F m proves False.

So, basically, the algorithm should pass over all Ci, check that args is disjoint from each argsi(params) and, if so, build the eliminator.

Alternative solutions

No response

Additional context

See the Zulip discussion reporting that using inversion to refute this kind of statement is slow. The above algorithm would provide a more direct way to do it as "fast" as discriminate works.

[silene]

With discriminate, one can disprove S (S n) = S O using match m with S O => False | _ => True end. But with your generalization to other predicates, it does not seem like one can disprove S (S n) <= S O. So, the approach seems a bit too adhoc, but perhaps I am missing something?

[herbelin]

Right, this does not apply directly to S (S n) <= S O. Maybe an induction on the proof of le would be necessary for the general case?

Or do the transit via Nat.leb?

More generally, I'd be curious of the "metatheory" of injectivity, discimination, and decidability for predicates such as le, and of the mechanisability that could result of it.

[herbelin]

@silene: I continued thinking to your question, and, the case S (S n) <= S O should actually work by induction. Here is a proof for S (S n) <= S 0 which can be canonically extended to S (S n) <= 0 , S (S (S n)) <= S (S 0), etc.:

Definition le2 m :=
  match m with
  | S 0 => False (* main arg *)
  | 0  => False (* main arg reverted by le_S *)
  | S (S _) => True (* le_n *)
  end.

Lemma le2_lift {m} : le2 m -> le2 (S m).
Proof.
now destruct m.
Defined.

Lemma discr n : S (S n) <= S O -> False.
Proof.
refine ((fix f m (H: S (S n) <= m) : le2 m :=
  match H in _ <= m return le2 m with
  | le_n _ => I
  | le_S _ p H => le2_lift (f p H)
  end) (S 0)).
Defined.

For the general algorithm, it seems that for a recursive constructor Ci : ... I argsi'1(γ) ... I argsi'p(γ) ... -> I argsi(γ), when argsi(γ) unifies with args, one should continue the inversion by replacing argsi by one of the argsi'j (under the condition that argsi'j is "smaller" in its number of constructors, so that the recursive search ends). Then, I suspect that an equivalent to le2_lift can always be defined to take care of the smallerness of the recursive step in the proof (to be studied further...).