discriminate is weaker than injection;discriminate with impredicative set

[SkySkimmer]

(* -*- coq-prog-args: ("-impredicative-set"); -*- *)

Inductive X : Set := x : Type -> bool -> X.

Goal x bool true <> x bool false.
  red.
  Fail discriminate.

  injection.
  (* |- true = false -> False *)
  discriminate.
Qed.

Also injection;discriminate is weaker than it could be:

Inductive bb@{u} : Type@{u} := b1 | b2.

Inductive Y : Set := y : bb -> Y.

Definition y2b (a:Y) : bool := match a with y b => if b then true else false end.

Goal y b1 <> y b2.
  red.
  Fail discriminate.

  Fail injection.

  intros H.
  generalize (f_equal y2b H).
  simpl.
  discriminate.
Qed.

[herbelin]

[Edited] It is that the proof pattern used for discriminate expects all inductive types in the path going towards the distinct occurrences to be eliminable to Type. So, your detour via injection suggests that only the inductive type of the distinct occurrences needs to be eliminable to Type and that injection can otherwise be used to traverse the common part of the path. That is, for discriminable pat(c) and pat(c'), instead of building the proof as of today:

match H in _ = x
      return match x with
             | pat(c') => False
             | pat(c) => True
             end
with
| eq_refl => I
end

you are suggesting to use instead the following proof [Edited to fix the too quick writing noticed by @SkySkimmer]:

match f_equal (fun x => match x with pat(y) => y | _ => dummy end) H in _ = x
      return match x with
             | c' => False
             | c => True
             end
with
| eq_refl => I
end

which indeed is less demanding in terms of elimination strength.

That's a good idea.

In your second example, you are even suggesting that discriminate rely on bool (known to be in the lower sort Set and thus requiring no more than elimination to Set), building the following proof [Edited]:

match f_equal (fun x => match x with pat(c') => false | _ => true end) H with in _ = x
      return match x with
             | false => False
             | true => True
             end
with
| eq_refl => I
end

That's also an interesting remark.

---

Alternatively, we may wonder whether the restriction on elimination sorts is not too strong: isn't there a notion of commutation of match for which the proofs above can be considered equivalent, so, that, eventually, one could say that the restriction on the elimination should somehow depend also on whether the branches would really exploit the extra permissiveness?

[SkySkimmer]

match f_equal (fun x => match x with pat(y) => y | _ => dummy end) H with
| c' => False
| c => True
end

f_equal produces an equality so such a match would have a unique eq_refl branch

[herbelin]

@SkySkimmer: I'm very sorry, I wrote again too quickly. I edited and it looks now correct (I double-checked in Coq with a concrete example).

I left open the question of whether some well-defined notion of commutative cut would connect the three proofs together.