Require Import LogicalRelations.
Require Export Coq.Bool.Bool.


(** * Relations for [sumbool] *)

(** ** Symmetric relation *)

(** NB: With proof irrelevance this is the same as [eq]. *)

Inductive sumbool_rel {P1 P2 Q1 Q2}: rel (sumbool P1 Q1) (sumbool P2 Q2):=
  | left_rel_def H1 H2: sumbool_rel (left H1) (left H2)
  | right_rel_def H1 H2: sumbool_rel (right H1) (right H2).

Global Instance left_rel:
  Monotonic (@left) (forallr _ _ : ⊤, forallr _ _ : ⊤, ⊤ ++> sumbool_rel).
Proof.
(* Goal: @Related (forall (A B : Prop) (_ : B), sumbool A B) (forall (A B : Prop) (_ : B), sumbool A B) (@right) (@right) (@forallp_rel Prop Prop (@rel_top Prop Prop) (fun H : Prop => forall v1 : Prop, (fun H0 : Prop => forall _ : H0, sumbool H H0) v1) (fun H : Prop => forall v2 : Prop, (fun H0 : Prop => forall _ : H0, sumbool H H0) v2) (fun v1 v2 : Prop => @forallp_rel Prop Prop (@rel_top Prop Prop) (fun H : Prop => forall _ : H, sumbool v1 H) (fun H : Prop => forall _ : H, sumbool v2 H) (fun v3 v4 : Prop => @arrow_rel v3 v4 (sumbool v1 v3) (sumbool v2 v4) (@rel_top v3 v4) (@sumbool_rel v1 v2 v3 v4)))) *)
  constructor; eauto.
Qed.

Global Instance right_rel:
  Monotonic (@right) (forallr _ _ : ⊤, forallr _ _ : ⊤, ⊤ ++> sumbool_rel).
Proof.
(* Goal: @Related (forall (A B : Prop) (_ : B), sumbool A B) (forall (A B : Prop) (_ : B), sumbool A B) (@right) (@right) (@forallp_rel Prop Prop (@rel_top Prop Prop) (fun H : Prop => forall v1 : Prop, (fun H0 : Prop => forall _ : H0, sumbool H H0) v1) (fun H : Prop => forall v2 : Prop, (fun H0 : Prop => forall _ : H0, sumbool H H0) v2) (fun v1 v2 : Prop => @forallp_rel Prop Prop (@rel_top Prop Prop) (fun H : Prop => forall _ : H, sumbool v1 H) (fun H : Prop => forall _ : H, sumbool v2 H) (fun v3 v4 : Prop => @arrow_rel v3 v4 (sumbool v1 v3) (sumbool v2 v4) (@rel_top v3 v4) (@sumbool_rel v1 v2 v3 v4)))) *)
  constructor; eauto.
Qed.

(** ** Directed relation *)

Inductive sumbool_le {P1 P2 Q1 Q2}: rel (sumbool P1 Q1) (sumbool P2 Q2):=
  | left_le b1 H2: Related b1 (left H2) sumbool_le
  | right_le H1 b2: Related (right H1) b2 sumbool_le.

Global Existing Instance left_le.
Global Existing Instance right_le.


(** * Definitions for [leb] *)

(** ** Properties *)

Global Instance leb_preo:
  PreOrder leb.
Proof.
(* Goal: @PreOrder bool leb *)
  split.
  - intros [|]; simpl; eauto.
  - intros [|]; simpl; eauto.
(* Goal: forall (y z : bool) (_ : @eq bool y true) (_ : leb y z), @eq bool z true *)
    intros [|]; simpl; eauto.
(* Goal: forall (z : bool) (_ : @eq bool false true) (_ : True), @eq bool z true *)
    discriminate.
Qed.

Lemma leb_rdestruct:
  RDestruct leb (fun P => P false false /\ P true true /\ P false true).
Proof.
(* Goal: @RDestruct bool bool leb (fun P : rel bool bool => and (P false false) (and (P true true) (P false true))) *)
  intros b1 b2 Hb P (HPff & HPtt & HPft).
(* Goal: forall (z : bool) (_ : @eq bool false true) (_ : True), @eq bool z true *)
  destruct b1, b2; eauto; discriminate.
Qed.

Hint Extern 0 (RDestruct leb _) =>
  eapply leb_rdestruct : typeclass_instances.

Global Instance leb_transport_eq_true x y:
  Transport Bool.leb x y (x = true) (y = true).
Proof.
(* Goal: @Transport bool bool leb x y (@eq bool x true) (@eq bool y true) *)
  clear.
(* Goal: @Transport bool bool leb x y (@eq bool x true) (@eq bool y true) *)
  destruct x, y; firstorder.
Qed.

(** ** Monotonicity of various definitions *)

Lemma true_leb b:
  Related b true leb.
Proof.
(* Goal: @Related bool bool false b leb *)
  destruct b; reflexivity.
Qed.

Hint Extern 0 (Related _ true _) =>
  eapply true_leb : typeclass_instances.

Lemma false_leb b:
  Related false b leb.
Proof.
(* Goal: @Related bool bool false b leb *)
  destruct b; reflexivity.
Qed.

Hint Extern 0 (Related false _ _) =>
  eapply false_leb : typeclass_instances.

Global Instance negb_leb:
  Monotonic negb (leb --> leb).
Proof.
(* Goal: @Related (forall _ : bool, bool) (forall _ : bool, bool) negb negb (@arrow_rel bool bool bool bool (@flip bool bool Prop leb) leb) *)
  unfold negb.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) (fun b1 b2 : bool => if b1 then b2 else true) (fun b1 b2 : bool => if b1 then b2 else true) (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) (@flip bool bool Prop leb) (@arrow_rel bool bool bool bool leb leb)) *)
  rauto.
Qed.

Global Instance andb_leb:
  Monotonic andb (leb ++> leb ++> leb).
Proof.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) andb andb (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) leb (@arrow_rel bool bool bool bool leb leb)) *)
  unfold andb.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) (fun b1 b2 : bool => if b1 then b2 else true) (fun b1 b2 : bool => if b1 then b2 else true) (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) (@flip bool bool Prop leb) (@arrow_rel bool bool bool bool leb leb)) *)
  rauto.
Qed.

Global Instance orb_leb:
  Monotonic orb (leb ++> leb ++> leb).
Proof.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) orb orb (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) leb (@arrow_rel bool bool bool bool leb leb)) *)
  unfold orb.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) (fun b1 b2 : bool => if b1 then b2 else true) (fun b1 b2 : bool => if b1 then b2 else true) (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) (@flip bool bool Prop leb) (@arrow_rel bool bool bool bool leb leb)) *)
  rauto.
Qed.

Global Instance implb_leb:
  Monotonic implb (leb --> leb ++> leb).
Proof.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) implb implb (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) (@flip bool bool Prop leb) (@arrow_rel bool bool bool bool leb leb)) *)
  unfold implb.
(* Goal: @Related (forall (_ : bool) (_ : bool), bool) (forall (_ : bool) (_ : bool), bool) (fun b1 b2 : bool => if b1 then b2 else true) (fun b1 b2 : bool => if b1 then b2 else true) (@arrow_rel bool bool (forall _ : bool, bool) (forall _ : bool, bool) (@flip bool bool Prop leb) (@arrow_rel bool bool bool bool leb leb)) *)
  rauto.
Qed.
