(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Section RewriteFacilities.

  Lemma diseq:
    ∀ {X : Type} (p : X → Prop) (x y : X),
      ¬ p x → p y → x ≠ y.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 20)
  
  ============================
  forall (X : Type) (p : X -> Prop) (x y : X), ~ p x -> p y -> x <> y

----------------------------------------------------------------------------- *)

  Proof. intros ? ? ? ? NP P EQ; subst; auto.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.


  Lemma eqprop_to_eqbool {X : eqType} {a b : X}: a = b → a == b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 27)
  
  X : eqType
  a, b : X
  ============================
  a = b -> a == b

----------------------------------------------------------------------------- *)

  Proof. by intros; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma eqbool_true {X : eqType} {a b : X}: a == b → a == b = true.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 35)
  
  X : eqType
  a, b : X
  ============================
  a == b -> (a == b) = true

----------------------------------------------------------------------------- *)

  Proof. by move =>/eqP EQ; subst b; rewrite eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma eqbool_false {X : eqType} {a b : X}: a != b → a == b = false.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  X : eqType
  a, b : X
  ============================
  a != b -> (a == b) = false

----------------------------------------------------------------------------- *)

  Proof. by apply negbTE.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.


  Lemma eqbool_to_eqprop {X : eqType} {a b : X}: a == b → a = b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  X : eqType
  a, b : X
  ============================
  a == b -> a = b

----------------------------------------------------------------------------- *)

  Proof. by intros; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma neqprop_to_neqbool {X : eqType} {a b : X}: a ≠ b → a != b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  X : eqType
  a, b : X
  ============================
  a <> b -> a != b

----------------------------------------------------------------------------- *)

  Proof. by intros; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma neqbool_to_neqprop {X : eqType} {a b : X}: a != b → a ≠ b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  X : eqType
  a, b : X
  ============================
  a != b -> a <> b

----------------------------------------------------------------------------- *)

  Proof. by intros; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma neq_sym {X : eqType} {a b : X}:
    a != b → b != a.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 70)
  
  X : eqType
  a, b : X
  ============================
  a != b -> b != a

----------------------------------------------------------------------------- *)

  Proof.
    intros NEQ; apply/eqP; intros EQ;
      subst b; move: NEQ ⇒ /eqP NEQ; auto.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma neq_antirefl {X : eqType} {a : X}:
    (a != a) = false.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  X : eqType
  a : X
  ============================
  (a != a) = false

----------------------------------------------------------------------------- *)

  Proof. by apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.


  Lemma option_inj_eq {X : eqType} {a b : X}:
    a == b → Some a == Some b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  X : eqType
  a, b : X
  ============================
  a == b -> Some a == Some b

----------------------------------------------------------------------------- *)

  Proof. by move ⇒ /eqP EQ; apply/eqP; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  Lemma option_inj_neq {X : eqType} {a b : X}:
    a != b → Some a != Some b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 94)
  
  X : eqType
  a, b : X
  ============================
  a != b -> Some a != Some b

----------------------------------------------------------------------------- *)

  Proof.
    by move ⇒ /eqP NEQ;
     apply/eqP; intros CONTR;
       apply: NEQ; inversion_clear CONTR.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  (* As a motivation for this file, we consider the following example. *)
  Section Example.

    (* Let X  be an arbitrary type ... *)
    Context {X : eqType}.

    (* ... f be an arbitrary function [bool -> bool] ... *)
    Variable f : bool → bool.

    (* ... p be an arbitrary predicate on X ... *)
    Variable p : X → Prop.

    (* ... and let a and b be two elements of X such that ... *)
    Variables a b : X.

    (* ... p holds for a and doesn't hold for b. *)
    Hypothesis H_pa : p a.
    Hypothesis H_npb : ¬ p b.

    (* The following examples are commented out
       to expose the insides of the proofs. *)

    (*
    (* Simplifying some relatively sophisticated 
       expressions can be quite tedious. *)
    [Goal f ((a == b) && f false) = f false.]
    [Proof.]
      (* Things like [simpl/compute] make no sense here. *)
      (* One can use [replace] to generate a new goal. *)
      [replace (a == b) with false; last first.]
      (* However, this leads to a "loss of focus". Moreover, 
         the resulting goal is not so trivial to prove. *)
      [{ apply/eqP; rewrite eq_sym eqbF_neg.]
      [    by apply/eqP; intros EQ; subst b; apply H_npb. }]
      [  by rewrite Bool.andb_false_l.]
    [Abort.]
     *)

    (*
    (* The second attempt. *)
    [Goal f ((a == b) && f false) = f false.]
      (* With the lemmas above one can compose multiple 
         transformations in a single rewrite. *)
      [  by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))]
      [        Bool.andb_false_l.]
    [Qed.]
    *)

  End Example.

End RewriteFacilities.