Library eq_id_comm

A proof that isweq A B is equivalent to being in bijection

Set Implicit Arguments.

Theorem eq_trans_refl_l : forall A (a b:A) (e:a =b), eq_trans eq_refl e = e.
destruct e. reflexivity.
Defined.

Theorem eq_trans_sym_l : forall A (a b:A) (H:a =b), eq_trans (eq_sym H) H = eq_refl.
Proof.
  destruct H; reflexivity.
Defined.

Theorem eq_trans_sym_r : forall A (a b:A) (H:a =b), eq_trans H (eq_sym H) = eq_refl.
Proof.
  destruct H; reflexivity.
Defined.

Theorem eq_id_comm : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a).
Proof.
  intros.
  unfold f_equal.
  rewrite <- (eq_trans_sym_l (Hf a)).

8.4beta still needs the following line but 8.4 is planned to support the combination of "at" clause with automatic computation of occurrences to abstract over

  pattern (f a) at 1 2 3 4 5 7 8, (Hf a) at 1 2.
  destruct (Hf a).
  destruct (Hf a).
  reflexivity.
Defined.

Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a).
Proof.
  intros.
  unfold f_equal.
  rewrite <- (eq_trans_sym_l (Hf (f (f a)))).
  set (Hfsymf := fun a => eq_sym (Hf a)).
  change (eq_sym (Hf (f (f a)))) with (Hfsymf (f (f a))).
  pattern (Hfsymf (f (f a))).
  destruct (eq_id_comm f Hfsymf (f a)).
  destruct (eq_id_comm f Hfsymf a).
  unfold Hfsymf.

8.3 would need the next line because a occurs in the type of Hf a

pattern a at -1 5 8 9 11 13 14 16, (Hf a).

  destruct (Hf a). simpl. unfold a0; clear a0.
  rewrite eq_trans_refl_l.
  reflexivity.
Defined.