Require Export Coq.Arith.EqNat.
Require Export Coq.Relations.Relations.

Require Export compcert.lib.Axioms.
Require Export compcert.lib.Coqlib.
Require Export compcert.lib.Integers.
Require Export compcert.lib.Floats.
Require Export compcert.lib.Maps.
Require Export compcert.common.AST.
Require Export compcert.common.Values.
Require Export compcert.common.Memdata.
Require Export compcert.common.Memtype.
Require Export compcert.common.Memory.
Require Export compcert.common.Globalenvs.


Require Export VST.msl.Coqlib2. 
Require Export VST.veric.coqlib4.

(* Lemmas about ident lists *)

Fixpoint id_in_list (id: ident) (ids: list ident) : bool :=
 match ids with i::ids' => orb (Pos.eqb id i) (id_in_list id ids') | _ => false end.

Fixpoint compute_list_norepet (ids: list ident) : bool :=
 match ids with
 | id :: ids' => if id_in_list id ids' then false else compute_list_norepet ids'
 | nil => true
 end.

Lemma id_in_list_true: forall i ids, id_in_list i ids = true -> In i ids.
Proof.
(* Goal: forall (ids : list ident) (_ : @eq bool (compute_list_norepet ids) true), @list_norepet ident ids *)
 induction ids; simpl; intros. inv H. apply orb_true_iff in H; destruct H; auto.
(* Goal: or (@eq ident a i) (@In ident i ids) *)
 apply Peqb_true_eq in H. subst; auto.
Qed.

Lemma id_in_list_false: forall i ids, id_in_list i ids = false -> ~In i ids.
Proof.
(* Goal: forall (i : ident) (ids : list ident) (_ : @eq bool (id_in_list i ids) false), not (@In ident i ids) *)
 induction ids; simpl; intros; auto.
(* Goal: not (or (@eq ident a i) (@In ident i ids)) *)
 apply orb_false_iff in H. destruct H.
(* Goal: not (or (@eq ident a i) (@In ident i ids)) *)
 intros [?|?]. subst.
(* Goal: and (@list_norepet A (@rev A l)) (and (@list_norepet A (@cons A a (@nil A))) (@list_disjoint A (@rev A l) (@cons A a (@nil A)))) *)
 rewrite Pos.eqb_refl in H; inv H.
(* Goal: False *)
 apply IHids; auto.
Qed.

Lemma compute_list_norepet_e: forall ids,
     compute_list_norepet ids = true -> list_norepet ids.
Proof.
(* Goal: forall (ids : list ident) (_ : @eq bool (compute_list_norepet ids) true), @list_norepet ident ids *)
 induction ids; simpl; intros.
(* Goal: @list_norepet ident (@nil ident) *)
(* Goal: @list_norepet ident (@cons ident a ids) *)
 constructor.
(* Goal: @list_norepet ident (@cons ident a ids) *)
 revert H; case_eq (id_in_list a ids); intros.
(* Goal: False *)
 inv H0.
(* Goal: @list_norepet A (@cons A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
 constructor; auto.
(* Goal: not (@In ident a ids) *)
 apply id_in_list_false in H.
(* Goal: False *)
 auto.
Qed.

Lemma list_norepet_rev:
  forall A (l: list A), list_norepet (rev l) = list_norepet l.
Proof.
(* Goal: False *)
induction l; simpl; auto.
(* Goal: @eq Prop (@list_norepet A (@app A (@rev A l) (@cons A a (@nil A)))) (@list_norepet A (@cons A a l)) *)
apply prop_ext; split; intros.
(* Goal: @list_norepet A (@cons A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
apply list_norepet_app in H.
(* Goal: @list_norepet A (@cons A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
destruct H as [? [? ?]].
(* Goal: @list_norepet A (@cons A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
rewrite IHl in H.
(* Goal: @list_norepet A (@cons A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
constructor; auto.
(* Goal: not (@In A a l) *)
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
eapply list_disjoint_notin with (a::nil).
(* Goal: False *)
apply list_disjoint_sym; auto.
(* Goal: False *)
(* Goal: False *)
intros x y ? ? ?; subst.
(* Goal: False *)
contradiction (H1 y y); auto.
(* Goal: False *)
rewrite <- In_rev; auto.
(* Goal: False *)
simpl; auto.
(* Goal: @list_norepet A (@app A (@rev A l) (@cons A a (@nil A))) *)
rewrite list_norepet_app.
(* Goal: and (@list_norepet A (@rev A l)) (and (@list_norepet A (@cons A a (@nil A))) (@list_disjoint A (@rev A l) (@cons A a (@nil A)))) *)
inv H.
(* Goal: False *)
split3; auto.
(* Goal: False *)
rewrite IHl; auto.
(* Goal: @list_norepet ident (@nil ident) *)
(* Goal: @list_norepet ident (@cons ident a ids) *)
repeat constructor.
(* Goal: not (@In A a (@nil A)) *)
(* Goal: @list_disjoint A (@rev A l) (@cons A a (@nil A)) *)
intro Hx. inv Hx.
(* Goal: False *)
(* Goal: False *)
intros x y ? ? ?; subst.
(* Goal: False *)
inv H0.
(* Goal: False *)
(* Goal: False *)
rewrite <- In_rev in H; contradiction.
(* Goal: False *)
auto.
Qed.

Lemma block_eq_dec: forall b1 b2: block, {b1 = b2} + {b1 <> b2}.
Proof. exact (Coqlib.peq). Qed.

Lemma rev_if_be_singleton:
  forall x, rev_if_be (x::nil) = (x::nil).
Proof. intro. unfold rev_if_be; destruct Archi.big_endian; auto. Qed.

Lemma rev_if_be_1: forall i, rev_if_be (i::nil) = (i::nil).
(* Goal: forall i : Byte.int, @eq (list Byte.int) (rev_if_be (@cons Byte.int i (@nil Byte.int))) (@cons Byte.int i (@nil Byte.int)) *)
Proof. unfold rev_if_be; intros. destruct Archi.big_endian; reflexivity.
Qed.

Lemma decode_byte_val:
  forall m, decode_val Mint8unsigned (Byte m :: nil) =
              Vint (Int.zero_ext 8 (Int.repr (Byte.unsigned m))).
Proof.
(* Goal: forall m : Byte.int, @eq val (decode_val Mint8unsigned (@cons memval (Byte m) (@nil memval))) (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Byte.unsigned m)))) *)
intros.
(* Goal: @eq val (decode_val Mint8unsigned (@cons memval (Byte m) (@nil memval))) (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Byte.unsigned m)))) *)
unfold decode_val. simpl.
(* Goal: @eq Int.int (Int.repr (Z.add (Byte.unsigned m) (Z.mul Z0 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Int.repr (Byte.unsigned m)) *)
f_equal.
(* Goal: @eq Int.int (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (decode_int (@cons Byte.int m (@nil Byte.int))))) (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Byte.unsigned m))) *)
unfold decode_int.
(* Goal: @eq Int.int (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (int_of_bytes (rev_if_be (@cons Byte.int m (@nil Byte.int)))))) (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Byte.unsigned m))) *)
rewrite rev_if_be_singleton.
(* Goal: @eq Int.int (Int.repr (Z.add (Byte.unsigned m) (Z.mul Z0 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Int.repr (Byte.unsigned m)) *)
unfold int_of_bytes. f_equal. f_equal. apply Z.add_0_r.
Qed.

Lemma Vint_inj: forall x y, Vint x = Vint y -> x=y.
Proof. congruence. Qed.

Definition nullval : val := 
  if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero.

Definition val_to_bool (v: val) : option bool :=
  match v with
    | Vint n => Some (negb (Int.eq n Int.zero))
    | Vptr _ _ => Some true
    | _ => None
  end.

Definition bool_of_valf (v: val): option bool :=
match v with
  | Vint i => Some (negb (Int.eq i Int.zero))
  | Vlong i => Some (negb (Int64.eq i Int64.zero))
  | Vfloat _ => None
  | Vsingle _ => None
  | Vptr _ _ => Some true
  | Vundef => None
end.