(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*                Xavier Leroy, INRIA Paris                            *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** This library provides type classes and tactics to decide logical
  propositions by reflection into computable Boolean equalities.
  It extends the [DecidableClass] module from the standard library
  of Coq 8.5 with more instances of decidable properties, including
  universal and existential quantification over finite types. *)

Require Export DecidableClass.
Require Import Coqlib.

Ltac decide_goal := eapply Decidable_sound; reflexivity.

(** Deciding logical connectives *)

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
  Decidable_witness := negb (@Decidable_witness P dP)
}.
Next Obligation.
(* Goal: iff (@eq bool (negb (@Decidable_witness P dP)) true) (not P) *)
  rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt.
Qed.

Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
  Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
}.
Next Obligation.
(* Goal: iff (@eq bool (eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)) true) (iff P Q) *)
  rewrite eqb_true_iff.
(* Goal: iff (forall (x : T) (_ : @In T x (@Finite_elements T fT)), @eq bool (@Decidable_witness (P x) (dP x)) true) (forall x : T, P x) *)
  split; intros.
(* Goal: iff P Q *)
(* Goal: @eq bool (@Decidable_witness P dP) (@Decidable_witness Q dQ) *)
  split; intros; eapply Decidable_sound; [rewrite <- H | rewrite H]; eapply Decidable_complete; eauto.
(* Goal: @eq bool (@Decidable_witness P dP) (@Decidable_witness Q dQ) *)
  destruct (@Decidable_witness Q dQ) eqn:D.
(* Goal: @eq bool (@Decidable_witness P dP) true *)
(* Goal: @eq bool (@Decidable_witness P dP) false *)
  eapply Decidable_complete; rewrite H; eapply Decidable_sound; eauto.
(* Goal: @eq bool (@Decidable_witness P dP) false *)
  eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
  Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
}.
Next Obligation.
(* Goal: iff (@eq bool (andb (@Decidable_witness P dP) (@Decidable_witness Q dQ)) true) (and P Q) *)
  rewrite andb_true_iff. rewrite ! Decidable_spec. tauto.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
  Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
}.
Next Obligation.
(* Goal: iff (or (@eq bool (@Decidable_witness P dP) true) (@eq bool (@Decidable_witness Q dQ) true)) (or P Q) *)
  rewrite orb_true_iff. rewrite ! Decidable_spec. tauto.
Qed.

Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
  Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
}.
Next Obligation.
(* Goal: iff (@ex T (fun x : T => and (@In T x (@Finite_elements T fT)) (@eq bool (@Decidable_witness (P x) (dP x)) true))) (@ex T (fun x : T => P x)) *)
  split.
- intros. rewrite Decidable_complete in H by auto. eapply Decidable_sound; eauto.
- intros. destruct (@Decidable_witness P dP) eqn:WP; auto.
(* Goal: P x *)
  eapply Decidable_complete. apply H. eapply Decidable_sound; eauto.
Qed.

(** Deciding equalities. *)

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y}) (x y: A) : Decidable (eq x y) := {|
  Decidable_witness := proj_sumbool (eqdec x y)
|}.
Next Obligation.
(* Goal: iff (forall (x : T) (_ : @In T x (@Finite_elements T fT)), @eq bool (@Decidable_witness (P x) (dP x)) true) (forall x : T, P x) *)
  split; intros. InvBooleans. auto. subst y. apply dec_eq_true.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
  Decidable_witness := Bool.eqb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (eqb x y) true) (@eq bool x y) *)
  apply eqb_true_iff.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
  Decidable_witness := Nat.eqb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (Nat.eqb x y) true) (@eq nat x y) *)
  apply Nat.eqb_eq.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
  Decidable_witness := Pos.eqb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (Pos.eqb x y) true) (@eq positive x y) *)
  apply Pos.eqb_eq.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
  Decidable_witness := Z.eqb x y
}.
Next Obligation.
(* Goal: @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true *)
  apply Z.eqb_eq.
Qed.

(** Deciding order on Z *)

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
  Decidable_witness := Z.leb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (Z.leb x y) true) (Z.le x y) *)
  apply Z.leb_le.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
  Decidable_witness := Z.ltb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (Z.ltb x y) true) (Z.lt x y) *)
  apply Z.ltb_lt.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
  Decidable_witness := Z.geb x y
}.
Next Obligation.
(* Goal: iff (@eq bool (Z.geb x y) true) (Z.ge x y) *)
  rewrite Z.geb_le. intuition omega.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
  Decidable_witness := Z.gtb x y
}.
Next Obligation.
(* Goal: iff (Z.lt y x) (Z.gt x y) *)
  rewrite Z.gtb_lt. intuition omega.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
  Decidable_witness := Z.eqb y ((y / x) * x)%Z
}.
Next Obligation.
(* Goal: iff (@ex T (fun x : T => and (@In T x (@Finite_elements T fT)) (@eq bool (@Decidable_witness (P x) (dP x)) true))) (@ex T (fun x : T => P x)) *)
  split.
(* Goal: forall _ : @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true, Z.divide x y *)
(* Goal: forall _ : Z.divide x y, @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true *)
  intros. apply Z.eqb_eq in H. exists (y / x). auto.
(* Goal: @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true *)
  intros [k EQ]. apply Z.eqb_eq.
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
  destruct (Z.eq_dec x 0).
(* Goal: @eq Z y (Z.mul (Z.div y Z0) Z0) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
  subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity.
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
  assert (k = y / x).
(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
  { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. }
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
  congruence.
Qed.

(** Deciding properties over lists *)

Program Instance Decidable_forall_in_list :
      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
      Decidable (forall x:A, In x l -> P x) := {
  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
}.
Next Obligation.
(* Goal: iff (forall (x : T) (_ : @In T x (@Finite_elements T fT)), @eq bool (@Decidable_witness (P x) (dP x)) true) (forall x : T, P x) *)
  rewrite List.forallb_forall. split; intros.
- eapply Decidable_sound; eauto.
- eapply Decidable_complete; eauto.
Qed.

Program Instance Decidable_exists_in_list :
      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
      Decidable (exists x:A, In x l /\ P x) := {
  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
}.
Next Obligation.
(* Goal: iff (@ex T (fun x : T => and (@In T x (@Finite_elements T fT)) (@eq bool (@Decidable_witness (P x) (dP x)) true))) (@ex T (fun x : T => P x)) *)
  rewrite List.existsb_exists. split.
- intros (x & U & V). exists x; split; auto. eapply Decidable_sound; eauto.
- intros (x & U & V). exists x; split; auto. eapply Decidable_complete; eauto.
Qed.

(** Types with finitely many elements. *)

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Class Finite (T: Type) := {
  Finite_elements: list T;
  Finite_elements_spec: forall x:T, In x Finite_elements
}.

(** Deciding forall and exists quantification over finite types. *)

Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
}.
Next Obligation.
(* Goal: iff (forall (x : T) (_ : @In T x (@Finite_elements T fT)), @eq bool (@Decidable_witness (P x) (dP x)) true) (forall x : T, P x) *)
  rewrite List.forallb_forall. split; intros.
- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec.
- eapply Decidable_complete; eauto.
Qed.

Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
}.
Next Obligation.
(* Goal: iff (@ex T (fun x : T => and (@In T x (@Finite_elements T fT)) (@eq bool (@Decidable_witness (P x) (dP x)) true))) (@ex T (fun x : T => P x)) *)
  rewrite List.existsb_exists. split.
- intros (x & A & B). exists x. eapply Decidable_sound; eauto.
(* Goal: iff (@ex T (fun x : T => and (@In T x (@Finite_elements T fT)) (@eq bool (@Decidable_witness (P x) (dP x)) true))) (@ex T (fun x : T => P x)) *)
- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto.
Qed.

(** Some examples of finite types. *)

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Finite_bool : Finite bool := {
  Finite_elements := false :: true :: nil
}.
Next Obligation.
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
(* Goal: forall _ : Z.divide x y, @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true *)
  destruct x; auto.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
  Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
}.
Next Obligation.
(* Goal: @In T x (@Finite_elements T fT) *)
  apply List.in_prod; eapply Finite_elements_spec.
Qed.

(* Goal: @eq Z k (Z.div y x) *)
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
  Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
}.
Next Obligation.
(* Goal: @eq Z y (Z.mul (Z.div y x) x) *)
(* Goal: forall _ : Z.divide x y, @eq bool (Z.eqb y (Z.mul (Z.div y x) x)) true *)
  destruct x; auto. right; apply List.in_map; eapply Finite_elements_spec.
Qed.
