(*
 * Copyright (c) 2009-2011, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

(* This file contains the class of decidable equality and associated theory
    of updateable functions. *)

Require Import VST.msl.base.

(* Class of decidable equality *)
Class EqDec (A : Type) : Type :=
  eq_dec : forall a a' : A, {a = a'} + {a <> a'}.

#[global] Instance EqDec_nat : EqDec nat := Peano_dec.eq_nat_dec.

(* Theory of updateable functions, defined over decideable domain *)
Definition upd {A} `{EqDec A} (B : Type) (f : A -> B) (a : A) (b : B) : A -> B :=
  fun a' => if eq_dec a a' then b else f a'.
Arguments upd [A H B] _ _ _ _.

Lemma upd_eq {A} `{EqDec A} : forall B (f : A -> B) a b,
  upd f a b a = b.
Proof with auto.
  intros.
  unfold upd.
  case (eq_dec a a)...
  intro.
  destruct n...
Qed.
Arguments upd_eq [A H B] _ _ _.

Lemma upd_eq' {A} `{EqDec A} : forall B (f : A -> B) a b a',
  a = a' ->
  upd f a b a' = b.
Proof.
  intros. subst a'. apply upd_eq.
Qed.
Arguments upd_eq' [A H B] _ _ _ _ _.

Lemma upd_neq {A} `{EqDec A} : forall B (f : A -> B) a b a',
  a <> a' ->
  upd f a b a' = f a'.
Proof with auto.
  intros.
  unfold upd.
  case (eq_dec a a')...
  intros.
  subst a'.
  destruct H0...
Qed.
Arguments upd_neq [A H B] _ _ _ _ _.

#[global] Instance nat_eq_dec: EqDec nat.
Proof.
  repeat intro.
 destruct (Compare_dec.lt_eq_lt_dec a a') as [[?|?]| ?]; auto;
  right; intro; subst; eapply PeanoNat.Nat.lt_irrefl; eauto.
Defined.

#[global] Instance EqDec_prod (A: Type) (EA: EqDec A) (B: Type) (EB: EqDec B) : EqDec (A*B).
Proof.
 hnf. decide equality; try apply eq_dec.
Defined.

#[global] Instance EqDec_list (A: Type) (EA: EqDec A) : EqDec (list A).
Proof.
 hnf. apply list_eq_dec; intros; apply EA.
Defined.

#[global] Instance EqDec_option (A: Type) (EA: EqDec A) : EqDec (option A).
Proof.
  hnf; decide equality.
Defined.

Lemma eq_dec_refl : forall {A B} {A_eq : EqDec A} (a : A) (b c : B), (if eq_dec a a then b else c) = b.
Proof.
  intros; destruct (eq_dec a a); [|contradiction n]; auto.
Qed.
