2

Would anyone explain to me why the same tactics (destruct) applied to the same hypothesis (bijective f) works in the first lemma and not in the second? Also, what should I do in order to fix it? I guess it has to do with mixing Prop and Type in the statement of the second lemma, but I don´t understand exactly what is happening here. Thank you in advance.

Require Import Setoid.

Definition injective {A B: Type} (f: A->B) :=
forall x y: A, f x = f y -> x = y.

Definition bijective {A B: Type} (f: A->B) :=
exists g: B->A, (forall x: A, g (f x) = x) /\ (forall y: B, f (g y) = y).

Definition decidable (t: Type): Type:=
(forall x y: t, {x=y}+{x<>y}).

Lemma bijective_to_injective:
forall t1 t2: Type,
forall f: t1 -> t2,
bijective f -> injective f.
Proof.
intros t1 t2 f H1.
destruct H1 as [g [H1 H2]]. (* <--- WORKS HERE *)
intros x y H3.
rewrite <- H1.
rewrite <- H1 at 1.
rewrite H3.
reflexivity.
Qed.

Lemma bijective_dec:
forall t1 t2: Type,
forall f: t1 -> t2,
bijective f ->
decidable t1 ->
decidable t2.
Proof.
intros t1 t2 f H1 H2 x y.
destruct H1 as [g [H1 H2]]. (* <--- DOESN´T WORK HERE *)
Qed.
Marcus
  • 437
  • 2
  • 11
  • 1
    Searching for your particular error message (`Case analysis on sort Set is not allowed for inductive definition ex`) helps a lot: see [here](http://stackoverflow.com/questions/28765188/)(your question imo is a duplicate of this one) and [here](http://stackoverflow.com/questions/28253726/). If you feel brave enough you might want to look also at [this](http://stackoverflow.com/questions/27322979/) great question/answer pair. – Anton Trunov Apr 13 '17 at 15:42

1 Answers1

3

Indeed your problem is that you need a so-called "informative definition" for bijective that is to say, one where you can extract the actual witness such as:

{ g: B -> A | cancel f g /\ cancel g f }
ejgallego
  • 6,709
  • 1
  • 14
  • 29