text:
(* Here we consider indexed valuations that can be interpreted as probability
   distributions; that is, those in which the sum of the weights is equal to 0 *)

From discprob.basic Require Import base sval order monad.
Require Import Reals Psatz.

Require ClassicalEpsilon.
From mathcomp Require Import ssrfun ssreflect eqtype ssrbool seq fintype choice.
Global Set Bullet Behavior "Strict Subproofs".
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finset finfun bigop.

Local Open Scope R_scope.
From discprob.idxval Require Import fin_ival.
From discprob.prob Require Import prob countable finite stochastic_order.

Record ivdist X :=
  { ivd_ival :> ival X;
    val_sum1: \big[Rplus/0]_(i : idx ivd_ival) val ivd_ival i = R1
  }.

Arguments ivd_ival {_}.
Arguments val_sum1 {_}.

Definition eq_ivd {X} (I1 I2: ivdist X) :=
  eq_ival I1 I2.

Global Instance eq_ivd_Transitivite {X}: Transitive (@eq_ivd X).
Proof. intros ???. apply eq_ival_trans. Qed.
Global Instance eq_ivd_Reflexive {X}: Reflexive (@eq_ivd X).
Proof. intros ?. apply eq_ival_refl. Qed.
Global Instance eq_ivd_Symmetry {X}: Symmetric (@eq_ivd X).
Proof. intros ??. apply eq_ival_sym. Qed.
Global Instance eq_ival_Equivalence {X}: Equivalence (@eq_ivd X).
Proof. split; apply _. Qed.

Definition ivdplus {X} (p: R) (Hrange: 0 <= p <= 1) (I1 I2: ivdist X) : ivdist X.
Proof.
  refine {| ivd_ival := iplus (iscale p I1) (iscale (1 - p) I2) |}.
  abstract (rewrite //=;
  rewrite /index_enum {1}[@Finite.enum]unlock /sum_enum big_cat ?big_map //=;
  rewrite -?big_distrr //= ?val_sum1;
  rewrite ?Rabs_right; nra).
Defined.

Global Instance ivdist_plus_proper:
  ∀ (X : Type) r Hpf, Proper (@eq_ivd X ==> @eq_ivd X ==> @eq_ivd X) (ivdplus r Hpf).
Proof.
  intros X r Hpf Is1 Is1' Hle1 Is2 Is2' Hle2.
  rewrite /eq_ivd/ivdplus//=.
  rewrite /eq_ivd in Hle1, Hle2.
  setoid_rewrite Hle1. setoid_rewrite Hle2.
  reflexivity.
Qed.

Lemma ivdplus_comm {X} (p: R) Hpf Hpf' (I1 I2: ivdist X) :
  eq_ivd (ivdplus p Hpf I1 I2) (ivdplus (1 - p) Hpf' I2 I1).
Proof.
  rewrite /eq_ivd/ivdplus//=.
  replace (1 - (1 - p)) with p by nra.
  apply iplus_comm.
Qed.

Lemma ivdplus_eq_ival {X} p Hpf (I1 I1' I2 I2': ivdist X):
  eq_ivd I1 I1' →
  eq_ivd I2 I2' →
  eq_ival (ivdplus p Hpf I1 I2) (ivdplus p Hpf I1' I2').
Proof.
  rewrite /eq_ivd/ivdplus => Heq1 Heq2 //=.
  setoid_rewrite Heq1.
  setoid_rewrite Heq2.
  reflexivity.
Qed.

Global Instance ivd_ret: MRet ivdist.
refine(λ A x, {| ivd_ival := mret x;
                 val_sum1 := _ |}).
{ abstract (rewrite /index_enum {1}[@Finite.enum]unlock //= big_seq1 //). }
Defined.

Global Instance ivd_bind: MBind ivdist.
refine(λ A B f I, {| ivd_ival := mbind (λ x, ivd_ival (f x)) (ivd_ival I);
                     val_sum1 := _ |}).
{ abstract (rewrite /index_enum {1}[@Finite.enum]unlock //=;
  rewrite /tag_enum big_flatten //= big_map;
  rewrite -(val_sum1 I); apply eq_bigr => i _;
  rewrite big_map //= -big_distrr val_sum1 /= Rmult_1_r //=).
}
Defined.

Global Instance ivd_bind_proper X Y :
  Proper (pointwise_relation X (@eq_ivd Y) ==> @eq_ivd X ==> @eq_ivd Y) (ivd_bind X Y).
Proof. intros ?? ? ?? ?. eapply ibind_proper; eauto. Qed.

Lemma ivd_assoc {A B C} (m: ivdist A) (f: A → ivdist B) (g: B → ivdist C) :
  eq_ivd (mbind g (mbind f m)) (mbind (λ x, mbind g (f x)) m).
Proof.
  rewrite /eq_ivd. setoid_rewrite ival_assoc. reflexivity.
Qed.

Lemma ivd_left_id {A B: Type} (x: A) (f: A → ivdist B):
  eq_ivd (mbind f (mret x)) (f x).
Proof.
  rewrite /eq_ivd. setoid_rewrite ival_left_id. reflexivity.
Qed.

Lemma ivd_right_id {A: Type} (m: ivdist A):
  eq_ivd (mbind mret m) m.
Proof.
  rewrite /eq_ivd. setoid_rewrite ival_right_id. reflexivity.
Qed.

Lemma ivd_bind_congr {A B} (m1 m2: ivdist A) (f1 f2: A → ivdist B) :
  eq_ivd m1 m2 →
  (∀ a, eq_ivd (f1 a) (f2 a)) →
  eq_ivd (x ← m1; f1 x) (x ← m2; f2 x).
Proof.
  intros Hlem Hlef.
  rewrite /eq_ivd.
  apply ival_bind_congr; eauto.
Qed.

Lemma ivd_plus_bind:
  ∀ (A B : Type) p Hpf (m1 m2 : ivdist A) (f : A → ivdist B),
    eq_ivd (x ← ivdplus p Hpf m1 m2; f x) (ivdplus p Hpf (x ← m1; f x) (x ← m2; f x)).
Proof.
  intros A B p Hpf m1 m2 f.
  rewrite /eq_ivd. rewrite /ivdplus/ivd_bind.
  setoid_rewrite ival_plus_bind.
  setoid_rewrite ival_scale_bind.
  reflexivity.
Qed.

Lemma eq_ival_sum {X} (I1 I2: ival X) P:
  eq_ival I1 I2 →
  \big[Rplus/0]_(i | P (ind I1 i)) (val I1 i) =
  \big[Rplus/0]_(i | P (ind I2 i)) (val I2 i).
Proof.
  intros Heq.
  transitivity (\big[Rplus/0]_(i : support (val I1) | P (ind I1 (sval i))) (val I1 (sval i))).
  - symmetry.  rewrite /index_enum. apply sum_reidx_map with (h := sval) => //=.
    * intros (a&Hgt) ?? => //=. rewrite -enumT mem_enum //=.
    * intros b _ HP Hneq. specialize (val_nonneg I1 b).
      destruct 1 as [Hgt|Heq0]; auto.
      exfalso. apply Hneq.
      exists (coerce_supp _ _ Hgt); repeat split; auto.
      rewrite -enumT mem_enum //=.
    * rewrite -enumT. apply enum_uniq.
    * rewrite -enumT. apply enum_uniq.
    * intros. by apply sval_inj_pred.
  - destruct Heq as (h1&h2&Hh12&Hh21&Hind&Hval).
    rewrite /index_enum. apply sum_reidx_map with (h := λ x, sval (h1 x)).
    * intros (a&Hgt) ? => //=. rewrite Hval. done.
    * intros (a&Hgt) ?? => //=. split; first by rewrite -enumT mem_enum //=.
      rewrite Hind. done.
    * intros b _ HP Hneq. specialize (val_nonneg I2 b).
      destruct 1 as [Hgt|Heq0]; auto.
      exfalso. apply Hneq.
      exists (h2 (coerce_supp _ _ Hgt)); repeat split; auto.
      ** rewrite -enumT mem_enum //=.
      ** rewrite -Hind Hh21. done.
      ** rewrite Hh21 //=.
    * rewrite -enumT. apply enum_uniq.
    * rewrite -enumT. apply enum_uniq.
    * intros x x' _ ?%sval_inj_pred.
      rewrite -(Hh12 x).
      rewrite -(Hh12 x').
      congruence.
Qed.

(*
Lemma img_rvar_of_ivdist {A: eqType} (h: ivdist A):
  map sval (Finite.enum [finType of (imgT (rvar_of_ivdist h))]) = undup [seq i.2 | i <- h].
Proof.
  rewrite {1}[@Finite.enum]unlock //=. rewrite img_fin_enum_sval.
  assert (a: A).
  { destruct h as (l, pf1, pf2). destruct l.
    - rewrite big_nil in pf2. move /eqP in pf2. exfalso.
      rewrite //= in pf2. fourier.
    - exact (snd p).
  }
  f_equal.
  etransitivity.
  - apply (@eq_map _ _ _ (λ n, nth a [seq i.2 | i <- h] (nat_of_ord n))).
    { intro i. erewrite set_nth_default; auto. rewrite size_map. done. }
  - rewrite -enumT. rewrite (nat_of_ord_map_iota (size h) (λ n, nth a [seq (snd i) | i <- h] n)).
  destruct h as (l, pf1, pf2) => //=; clear pf1 pf2.
  rewrite -(size_map snd l) map_nth_iota //.
Qed.
*)

Lemma primitive_ivdplus {X} p HPf (I1 I2: ivdist X):
  ival_primitive I1 →
  ival_primitive I2 →
  ¬ (∃ i1 i2, ind I1 i1 = ind I2 i2) →
  ival_primitive (ivdplus p HPf I1 I2).
Proof.
  intros Hprim1 Hprim2 Hdisj ia ib.
  destruct ia, ib => //=.
  - intros Heq. f_equal. apply Hprim1; eauto.
  - intros Heq. exfalso; eapply Hdisj; eauto.
  - intros Heq. exfalso; eapply Hdisj; eauto.
  - intros Heq. f_equal. apply Hprim2; eauto.
Qed.

Lemma primitive_ivdplus_mret {X} p HPf (x1 x2: X):
  x1 ≠ x2 →
  ival_primitive (ivdplus p HPf (mret x1) (mret x2)).
Proof. intros ? [[]|[]] [[]|[]] => //=; intros; try f_equal; try congruence. Qed.

Lemma ivd_isupport_inhabited {X} (I: ivdist X) : isupport I.
Proof.
  destruct I as [I Hsum].
  destruct I as [idx ind val].
  rewrite //= in Hsum *.
  rewrite //=/index_enum//= in Hsum *.
  assert (0 < \big[Rplus/0]_(i <- Finite.enum idx) val i) as Hlt0.
  { nra.  }
  edestruct (ClassicalEpsilon.constructive_indefinite_description _
              (Rlt_0_big_inv val (Finite.enum idx) (λ x, true) Hlt0)) as (i&?&?&?).
  exists (ind i) => //=.
  exists i; split; auto.
Qed.

author: jtassarotti

repo: polaris

save_path: github-repos/coq/jtassarotti-polaris


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, Collège de France and 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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Additional operations and proofs about binary integers,
    on top of the ZArith standard library. *)

Require Import Psatz Zquot.
Require Import Coqlib.

(** ** Modulo arithmetic *)

(** We define and state properties of equality and arithmetic modulo a
  positive integer. *)

Section EQ_MODULO.

Variable modul: Z.
Hypothesis modul_pos: modul > 0.

Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.

Lemma eqmod_refl: forall x, eqmod x x.
Proof.
  intros; red. exists 0. omega.
Qed.

Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
Proof.
  intros. subst y. apply eqmod_refl.
Qed.

Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
Proof.
  intros x y [k EQ]; red. exists (-k). subst x. ring.
Qed.

Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
Proof.
  intros x y z [k1 EQ1] [k2 EQ2]; red.
  exists (k1 + k2). subst x; subst y. ring.
Qed.

Lemma eqmod_small_eq:
  forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
Proof.
  intros x y [k EQ] I1 I2.
  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
  rewrite (Z.div_small x modul I1) in H. subst k. omega.
Qed.

Lemma eqmod_mod_eq:
  forall x y, eqmod x y -> x mod modul = y mod modul.
Proof.
  intros x y [k EQ]. subst x.
  rewrite Z.add_comm. apply Z_mod_plus. auto.
Qed.

Lemma eqmod_mod:
  forall x, eqmod x (x mod modul).
Proof.
  intros; red. exists (x / modul).
  rewrite Z.mul_comm. apply Z_div_mod_eq. auto.
Qed.

Lemma eqmod_add:
  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst c. exists (k1 + k2). ring.
Qed.

Lemma eqmod_neg:
  forall x y, eqmod x y -> eqmod (-x) (-y).
Proof.
  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
Qed.

Lemma eqmod_sub:
  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst c. exists (k1 - k2). ring.
Qed.

Lemma eqmod_mult:
  forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst b.
  exists (k1 * k2 * modul + c * k2 + k1 * d).
  ring.
Qed.

End EQ_MODULO.

Lemma eqmod_divides:
  forall n m x y, eqmod n x y -> Z.divide m n -> eqmod m x y.
Proof.
  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
  exists (k1*k2). rewrite <- Z.mul_assoc. rewrite <- EQ2. auto.
Qed.

(** ** Fast normalization modulo [2^n] *)

Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z :=
  match n with
  | O => 0
  | S m =>
      match p with
      | xH => 1
      | xO q => Z.double (P_mod_two_p q m)
      | xI q => Z.succ_double (P_mod_two_p q m)
      end
  end.

Definition Z_mod_two_p (x: Z) (n: nat) : Z :=
  match x with
  | Z0 => 0
  | Zpos p => P_mod_two_p p n
  | Zneg p => let r := P_mod_two_p p n in if zeq r 0 then 0 else two_power_nat n - r
  end.

Lemma P_mod_two_p_range:
  forall n p, 0 <= P_mod_two_p p n < two_power_nat n.
Proof.
  induction n; simpl; intros.
  - rewrite two_power_nat_O. omega.
  - rewrite two_power_nat_S. destruct p.
    + generalize (IHn p). rewrite Z.succ_double_spec. omega.
    + generalize (IHn p). rewrite Z.double_spec. omega.
    + generalize (two_power_nat_pos n). omega.
Qed.

Lemma P_mod_two_p_eq:
  forall n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).
Proof.
  assert (forall n p, exists y, Zpos p = y * two_power_nat n + P_mod_two_p p n).
  {
    induction n; simpl; intros.
    - rewrite two_power_nat_O. exists (Zpos p). ring.
    - rewrite two_power_nat_S. destruct p.
      + destruct (IHn p) as [y EQ]. exists y.
        change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ.
        rewrite Z.succ_double_spec. ring.
      + destruct (IHn p) as [y EQ]. exists y.
        change (Zpos p~0) with (2 * Zpos p). rewrite EQ.
        rewrite (Z.double_spec (P_mod_two_p p n)). ring.
      + exists 0; omega.
  }
  intros.
  destruct (H n p) as [y EQ].
  symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range.
Qed.

Lemma Z_mod_two_p_range:
  forall n x, 0 <= Z_mod_two_p x n < two_power_nat n.
Proof.
  intros; unfold Z_mod_two_p. generalize (two_power_nat_pos n); intros.
  destruct x.
  - intuition.
  - apply P_mod_two_p_range.
  - set (r := P_mod_two_p p n).
    assert (0 <= r < two_power_nat n) by apply P_mod_two_p_range.
    destruct (zeq r 0).
    + intuition.
    + Psatz.lia.
Qed.

Lemma Z_mod_two_p_eq:
  forall n x, Z_mod_two_p x n = x mod (two_power_nat n).
Proof.
  intros. unfold Z_mod_two_p. generalize (two_power_nat_pos n); intros.
  destruct x.
  - rewrite Zmod_0_l. auto.
  - apply P_mod_two_p_eq.
  - generalize (P_mod_two_p_range n p) (P_mod_two_p_eq n p). intros A B.
    exploit (Z_div_mod_eq (Zpos p) (two_power_nat n)); auto. intros C.
    set (q := Zpos p / two_power_nat n) in *.
    set (r := P_mod_two_p p n) in *.
    rewrite <- B in C.
    change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0).
    + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia.
      intuition.
    + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia.
      intuition.
Qed.

(** ** Bit-level operations and properties *)

(** Shift [x] left by one and insert [b] as the low bit of the result. *)

Definition Zshiftin (b: bool) (x: Z) : Z :=
  if b then Z.succ_double x else Z.double x.

Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
Proof Z.testbit_0_l.

Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
Proof.
  intros. destruct n; simpl; auto.
Qed.

Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
Proof.
  intros. destruct n; simpl; auto.
Qed.

Remark Zshiftin_spec:
  forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0).
Proof.
  unfold Zshiftin; intros. destruct b.
  - rewrite Z.succ_double_spec. omega.
  - rewrite Z.double_spec. omega.
Qed.

Remark Zshiftin_inj:
  forall b1 x1 b2 x2,
  Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2.
Proof.
  intros. rewrite !Zshiftin_spec in H.
  destruct b1; destruct b2.
  split; [auto|omega].
  omegaContradiction.
  omegaContradiction.
  split; [auto|omega].
Qed.

Remark Zdecomp:
  forall x, x = Zshiftin (Z.odd x) (Z.div2 x).
Proof.
  intros. destruct x; simpl.
  - auto.
  - destruct p; auto.
  - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto.
Qed.

Remark Ztestbit_shiftin:
  forall b x n,
  0 <= n ->
  Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n).
Proof.
  intros. rewrite Zshiftin_spec. destruct (zeq n 0).
  - subst n. destruct b.
    + apply Z.testbit_odd_0.
    + rewrite Z.add_0_r. apply Z.testbit_even_0.
  - assert (0 <= Z.pred n) by omega.
    set (n' := Z.pred n) in *.
    replace n with (Z.succ n') by (unfold n'; omega).
    destruct b.
    + apply Z.testbit_odd_succ; auto.
    + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto.
Qed.

Remark Ztestbit_shiftin_base:
  forall b x, Z.testbit (Zshiftin b x) 0 = b.
Proof.
  intros. rewrite Ztestbit_shiftin. apply zeq_true. omega.
Qed.

Remark Ztestbit_shiftin_succ:
  forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.
Proof.
  intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto.
  omega. omega.
Qed.

Lemma Zshiftin_ind:
  forall (P: Z -> Prop),
  P 0 ->
  (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) ->
  forall x, 0 <= x -> P x.
Proof.
  intros. destruct x.
  - auto.
  - induction p.
    + change (P (Zshiftin true (Z.pos p))). auto.
    + change (P (Zshiftin false (Z.pos p))). auto.
    + change (P (Zshiftin true 0)). apply H0. omega. auto.
  - compute in H1. intuition congruence.
Qed.

Lemma Zshiftin_pos_ind:
  forall (P: Z -> Prop),
  P 1 ->
  (forall b x, 0 < x -> P x -> P (Zshiftin b x)) ->
  forall x, 0 < x -> P x.
Proof.
  intros. destruct x; simpl in H1; try discriminate.
  induction p.
    + change (P (Zshiftin true (Z.pos p))). auto.
    + change (P (Zshiftin false (Z.pos p))). auto.
    + auto.
Qed.

(** ** Bit-wise decomposition ([Z.testbit]) *)

Remark Ztestbit_eq:
  forall n x, 0 <= n ->
  Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n).
Proof.
  intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto.
Qed.

Remark Ztestbit_base:
  forall x, Z.testbit x 0 = Z.odd x.
Proof.
  intros. rewrite Ztestbit_eq. apply zeq_true. omega.
Qed.

Remark Ztestbit_succ:
  forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.
Proof.
  intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto.
  omega. omega.
Qed.

Lemma eqmod_same_bits:
  forall n x y,
  (forall i, 0 <= i < Z.of_nat n -> Z.testbit x i = Z.testbit y i) ->
  eqmod (two_power_nat n) x y.
Proof.
  induction n; intros.
  - change (two_power_nat 0) with 1. exists (x-y); ring.
  - rewrite two_power_nat_S.
    assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)).
      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega.
      omega. omega.
  destruct H0 as [k EQ].
  exists k. rewrite (Zdecomp x). rewrite (Zdecomp y).
  replace (Z.odd y) with (Z.odd x).
  rewrite EQ. rewrite !Zshiftin_spec. ring.
  exploit (H 0). rewrite Nat2Z.inj_succ; omega.
  rewrite !Ztestbit_base. auto.
Qed.

Lemma same_bits_eqmod:
  forall n x y i,
  eqmod (two_power_nat n) x y -> 0 <= i < Z.of_nat n ->
  Z.testbit x i = Z.testbit y i.
Proof.
  induction n; intros.
  - simpl in H0. omegaContradiction.
  - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H.
    rewrite !(Ztestbit_eq i); intuition.
    destruct H as [k EQ].
    assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) =
                 Zshiftin (Z.odd y) (k * two_power_nat n + Z.div2 y)).
    {
      rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ.
      rewrite EQ. rewrite !Zshiftin_spec. ring.
    }
    exploit Zshiftin_inj; eauto. intros [A B].
    destruct (zeq i 0).
    + auto.
    + apply IHn. exists k; auto. omega.
Qed.

Lemma equal_same_bits:
  forall x y,
  (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
  x = y.
Proof Z.bits_inj'.

Lemma Z_one_complement:
  forall i, 0 <= i ->
  forall x, Z.testbit (-x-1) i = negb (Z.testbit x i).
Proof.
  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
  intros i IND POS x.
  rewrite (Zdecomp x). set (y := Z.div2 x).
  replace (- Zshiftin (Z.odd x) y - 1)
     with (Zshiftin (negb (Z.odd x)) (- y - 1)).
  rewrite !Ztestbit_shiftin; auto.
  destruct (zeq i 0). auto. apply IND. omega.
  rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring.
Qed.

Lemma Ztestbit_above:
  forall n x i,
  0 <= x < two_power_nat n ->
  i >= Z.of_nat n ->
  Z.testbit x i = false.
Proof.
  induction n; intros.
  - change (two_power_nat 0) with 1 in H.
    replace x with 0 by omega.
    apply Z.testbit_0_l.
  - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false.
    apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H.
    rewrite Zshiftin_spec in H. destruct (Z.odd x); omega.
    omega. omega. omega.
Qed.

Lemma Ztestbit_above_neg:
  forall n x i,
  -two_power_nat n <= x < 0 ->
  i >= Z.of_nat n ->
  Z.testbit x i = true.
Proof.
  intros. set (y := -x-1).
  assert (Z.testbit y i = false).
    apply Ztestbit_above with n.
    unfold y; omega. auto.
  unfold y in H1. rewrite Z_one_complement in H1.
  change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto.
  omega.
Qed.

Lemma Zsign_bit:
  forall n x,
  0 <= x < two_power_nat (S n) ->
  Z.testbit x (Z.of_nat n) = if zlt x (two_power_nat n) then false else true.
Proof.
  induction n; intros.
  - change (two_power_nat 1) with 2 in H.
    assert (x = 0 \/ x = 1) by omega.
    destruct H0; subst x; reflexivity.
  - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
    rewrite IHn. rewrite two_power_nat_S.
    destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec.
    rewrite zlt_true. auto. destruct (Z.odd x); omega.
    rewrite zlt_false. auto. destruct (Z.odd x); omega.
    rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H.
    rewrite two_power_nat_S in H. destruct (Z.odd x); omega.
    omega. omega.
Qed.

Lemma Ztestbit_le:
  forall x y,
  0 <= y ->
  (forall i, 0 <= i -> Z.testbit x i = true -> Z.testbit y i = true) ->
  x <= y.
Proof.
  intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros.
  - replace x with 0. omega. apply equal_same_bits; intros.
    rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto.
    exploit H; eauto. rewrite Ztestbit_0. auto.
  - assert (Z.div2 x0 <= x).
    { apply H0. intros. exploit (H1 (Z.succ i)).
        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
    }
    rewrite (Zdecomp x0). rewrite !Zshiftin_spec.
    destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega.
    exploit (H1 0). omega. rewrite Ztestbit_base; auto.
    rewrite Ztestbit_shiftin_base. congruence.
Qed.

Lemma Ztestbit_mod_two_p:
  forall n x i,
  0 <= n -> 0 <= i ->
  Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false.
Proof.
  intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto.
  - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l.
    rewrite zlt_false; auto. omega.
  - intros. rewrite two_p_S; auto.
    replace (x0 mod (2 * two_p x))
       with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)).
    rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0).
    + rewrite zlt_true; auto. omega.
    + rewrite H0. destruct (zlt (Z.pred i) x).
      * rewrite zlt_true; auto. omega.
      * rewrite zlt_false; auto. omega.
      * omega.
    + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry.
      apply Zmod_unique with (x1 / two_p x).
      rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal.
      transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)).
      f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto.
      ring.
      rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto.
      destruct (Z.odd x0); omega.
Qed.

Corollary Ztestbit_two_p_m1:
  forall n i, 0 <= n -> 0 <= i ->
  Z.testbit (two_p n - 1) i = if zlt i n then true else false.
Proof.
  intros. replace (two_p n - 1) with ((-1) mod (two_p n)).
  rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto.
  apply Zmod_unique with (-1). ring.
  exploit (two_p_gt_ZERO n). auto. omega.
Qed.

Corollary Ztestbit_neg_two_p:
  forall n i, 0 <= n -> 0 <= i ->
  Z.testbit (- (two_p n)) i = if zlt i n then false else true.
Proof.
  intros.
  replace (- two_p n) with (- (two_p n - 1) - 1) by omega.
  rewrite Z_one_complement by auto.
  rewrite Ztestbit_two_p_m1 by auto.
  destruct (zlt i n); auto.
Qed.

Lemma Z_add_is_or:
  forall i, 0 <= i ->
  forall x y,
  (forall j, 0 <= j <= i -> Z.testbit x j && Z.testbit y j = false) ->
  Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.
Proof.
  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
  intros i IND POS x y EXCL.
  rewrite (Zdecomp x) in *. rewrite (Zdecomp y) in *.
  transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i).
  - f_equal. rewrite !Zshiftin_spec.
    exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros.
Opaque Z.mul.
    destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring.
  - rewrite !Ztestbit_shiftin; auto.
    destruct (zeq i 0).
    + auto.
    + apply IND. omega. intros.
      exploit (EXCL (Z.succ j)). omega.
      rewrite !Ztestbit_shiftin_succ. auto.
      omega. omega.
Qed.

(** ** Zero and sign extensions *)

(** In pseudo-code:
<<
    Fixpoint Zzero_ext (n: Z) (x: Z) : Z :=
      if zle n 0 then
        0
      else
        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
    Fixpoint Zsign_ext (n: Z) (x: Z) : Z :=
      if zle n 1 then
        if Z.odd x then -1 else 0
      else
        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
>>
  We encode this [nat]-like recursion using the [Z.iter] iteration
  function, in order to make the [Zzero_ext] and [Zsign_ext]
  functions efficiently executable within Coq.
*)

Definition Zzero_ext (n: Z) (x: Z) : Z :=
  Z.iter n
    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
    (fun x => 0)
    x.

Definition Zsign_ext (n: Z) (x: Z) : Z :=
  Z.iter (Z.pred n)
    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
    (fun x => if Z.odd x then -1 else 0)
    x.

Lemma Ziter_base:
  forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x.
Proof.
  intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto.
Qed.

Lemma Ziter_succ:
  forall (A: Type) n (f: A -> A) x,
  0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x).
Proof.
  intros. destruct n; simpl.
  - auto.
  - rewrite Pos.add_1_r. apply Pos.iter_succ.
  - compute in H. elim H; auto.
Qed.

Lemma Znatlike_ind:
  forall (P: Z -> Prop),
  (forall n, n <= 0 -> P n) ->
  (forall n, 0 <= n -> P n -> P (Z.succ n)) ->
  forall n, P n.
Proof.
  intros. destruct (zle 0 n).
  apply natlike_ind; auto. apply H; omega.
  apply H. omega.
Qed.

Lemma Zzero_ext_spec:
  forall n x i, 0 <= i ->
  Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false.
Proof.
  unfold Zzero_ext. induction n using Znatlike_ind.
  - intros. rewrite Ziter_base; auto.
    rewrite zlt_false. rewrite Ztestbit_0; auto. omega.
  - intros. rewrite Ziter_succ; auto.
    rewrite Ztestbit_shiftin; auto.
    rewrite (Ztestbit_eq i x); auto.
    destruct (zeq i 0).
    + subst i. rewrite zlt_true; auto. omega.
    + rewrite IHn. destruct (zlt (Z.pred i) n).
      rewrite zlt_true; auto. omega.
      rewrite zlt_false; auto. omega.
      omega.
Qed.

Lemma Zsign_ext_spec:
  forall n x i, 0 <= i -> 0 < n ->
  Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1).
Proof.
  intros n0 x i I0 N0.
  revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1).
  - unfold Zsign_ext. intros.
    destruct (zeq x 1).
    + subst x; simpl.
      replace (if zlt i 1 then i else 0) with 0.
      rewrite Ztestbit_base.
      destruct (Z.odd x0).
      apply Ztestbit_m1; auto.
      apply Ztestbit_0.
      destruct (zlt i 1); omega.
    + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)).
      rewrite Ziter_succ. rewrite Ztestbit_shiftin.
      destruct (zeq i 0).
      * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega.
      * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)).
        rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega.
        rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto.
        omega. omega. omega. unfold x1; omega. omega.
      * omega.
      * unfold x1; omega.
      * omega.
  - omega.
Qed.

(** [Zzero_ext n x] is [x modulo 2^n] *)

Lemma Zzero_ext_mod:
  forall n x, 0 <= n -> Zzero_ext n x = x mod (two_p n).
Proof.
  intros. apply equal_same_bits; intros.
  rewrite Zzero_ext_spec, Ztestbit_mod_two_p by auto. auto.
Qed.

(** [Zzero_ext n x] is the unique integer congruent to [x] modulo [2^n] in the range [0...2^n-1]. *)

Lemma Zzero_ext_range:
  forall n x, 0 <= n -> 0 <= Zzero_ext n x < two_p n.
Proof.
  intros. rewrite Zzero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega.
Qed.

Lemma eqmod_Zzero_ext:
  forall n x, 0 <= n -> eqmod (two_p n) (Zzero_ext n x) x.
Proof.
  intros. rewrite Zzero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod.
  apply two_p_gt_ZERO. omega.
Qed.

(** Relation between [Zsign_ext n x] and (Zzero_ext n x] *)

Lemma Zsign_ext_zero_ext:
  forall n, 0 < n -> forall x,
  Zsign_ext n x = Zzero_ext n x - (if Z.testbit x (n - 1) then two_p n else 0).
Proof.
  intros. apply equal_same_bits; intros.
  rewrite Zsign_ext_spec by auto.
  destruct (Z.testbit x (n - 1)) eqn:SIGNBIT.
- set (n' := - two_p n).
  replace (Zzero_ext n x - two_p n) with (Zzero_ext n x + n') by (unfold n'; omega).
  rewrite Z_add_is_or; auto.
  rewrite Zzero_ext_spec by auto. unfold n'; rewrite Ztestbit_neg_two_p by omega.
  destruct (zlt i n). rewrite orb_false_r; auto. auto.
  intros. rewrite Zzero_ext_spec by omega. unfold n'; rewrite Ztestbit_neg_two_p by omega.
  destruct (zlt j n); auto using andb_false_r.
- replace (Zzero_ext n x - 0) with (Zzero_ext n x) by omega.
  rewrite Zzero_ext_spec by auto.
  destruct (zlt i n); auto.
Qed.

(** [Zsign_ext n x] is the unique integer congruent to [x] modulo [2^n]
    in the range [-2^(n-1)...2^(n-1) - 1]. *)

Lemma Zsign_ext_range:
  forall n x, 0 < n -> -two_p (n-1) <= Zsign_ext n x < two_p (n-1).
Proof.
  intros.
  assert (A: 0 <= Zzero_ext n x < two_p n) by (apply Zzero_ext_range; omega).
  assert (B: Z.testbit (Zzero_ext n x) (n - 1) =
             if zlt (Zzero_ext n x) (two_p (n - 1)) then false else true).
  { set (N := Z.to_nat (n - 1)).
    generalize (Zsign_bit N (Zzero_ext n x)).
    rewrite ! two_power_nat_two_p.
    rewrite inj_S.  unfold N; rewrite Z2Nat.id by omega.
    intros X; apply X.  replace (Z.succ (n - 1)) with n by omega. exact A.
  }
  assert (C: two_p n = 2 * two_p (n - 1)).
  { rewrite <- two_p_S by omega. f_equal; omega. }
  rewrite Zzero_ext_spec, zlt_true in B by omega.
  rewrite Zsign_ext_zero_ext by auto. rewrite B.
  destruct (zlt (Zzero_ext n x) (two_p (n - 1))); omega.
Qed.

Lemma eqmod_Zsign_ext:
  forall n x, 0 < n ->
  eqmod (two_p n) (Zsign_ext n x) x.
Proof.
  intros. rewrite Zsign_ext_zero_ext by auto.
  apply eqmod_trans with (x - 0).
  apply eqmod_sub.
  apply eqmod_Zzero_ext; omega.
  exists (if Z.testbit x (n - 1) then 1 else 0). destruct (Z.testbit x (n - 1)); ring.
  apply eqmod_refl2; omega.
Qed.

(** ** Decomposition of a number as a sum of powers of two. *)

Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
  match n with
  | O => nil
  | S m =>
      if Z.odd x
      then i :: Z_one_bits m (Z.div2 x) (i+1)
      else Z_one_bits m (Z.div2 x) (i+1)
  end.

Fixpoint powerserie (l: list Z): Z :=
  match l with
  | nil => 0
  | x :: xs => two_p x + powerserie xs
  end.

Lemma Z_one_bits_powerserie:
  forall n x, 0 <= x < two_power_nat n -> x = powerserie (Z_one_bits n x 0).
Proof.
  assert (forall n x i,
    0 <= i ->
    0 <= x < two_power_nat n ->
    x * two_p i = powerserie (Z_one_bits n x i)).
  {
  induction n; intros.
  simpl. rewrite two_power_nat_O in H0.
  assert (x = 0) by omega. subst x. omega.
  rewrite two_power_nat_S in H0. simpl Z_one_bits.
  rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0.
  assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))).
    apply IHn. omega.
    destruct (Z.odd x); omega.
  rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ.
  rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec.
  destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring.
  omega. omega.
  }
  intros. rewrite <- H. change (two_p 0) with 1. omega.
  omega. exact H0.
Qed.

Lemma Z_one_bits_range:
  forall n x i, In i (Z_one_bits n x 0) -> 0 <= i < Z.of_nat n.
Proof.
  assert (forall n x i j,
    In j (Z_one_bits n x i) -> i <= j < i + Z.of_nat n).
  {
  induction n; simpl In.
  tauto.
  intros x i j. rewrite Nat2Z.inj_succ.
  assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)).
    intros. exploit IHn; eauto. omega.
  destruct (Z.odd x); simpl.
  intros [A|B]. subst j. omega. auto.
  auto.
  }
  intros. generalize (H n x 0 i H0). omega.
Qed.

Remark Z_one_bits_zero:
  forall n i, Z_one_bits n 0 i = nil.
Proof.
  induction n; intros; simpl; auto.
Qed.

Remark Z_one_bits_two_p:
  forall n x i,
  0 <= x < Z.of_nat n ->
  Z_one_bits n (two_p x) i = (i + x) :: nil.
Proof.
  induction n; intros; simpl. simpl in H. omegaContradiction.
  rewrite Nat2Z.inj_succ in H.
  assert (x = 0 \/ 0 < x) by omega. destruct H0.
  subst x; simpl. decEq. omega. apply Z_one_bits_zero.
  assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)).
    apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec.
    rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega.
  destruct H1 as [A B]; rewrite A; rewrite B.
  rewrite IHn. f_equal; omega. omega.
Qed.

(** ** Recognition of powers of two *)

Fixpoint P_is_power2 (p: positive) : bool :=
  match p with
  | xH => true
  | xO q => P_is_power2 q
  | xI q => false
  end.

Definition Z_is_power2 (x: Z) : option Z :=
  match x with
  | Z0 => None
  | Zpos p => if P_is_power2 p then Some (Z.log2 x) else None
  | Zneg _ => None
  end.

Remark P_is_power2_sound:
  forall p, P_is_power2 p = true -> Z.pos p = two_p (Z.log2 (Z.pos p)).
Proof.
  induction p; simpl P_is_power2; intros.
- discriminate.
- change (Z.pos p~0) with (2 * Z.pos p).  apply IHp in H.
  rewrite Z.log2_double by xomega. rewrite two_p_S.  congruence.
  apply Z.log2_nonneg.
- reflexivity.
Qed.

Lemma Z_is_power2_sound:
  forall x i, Z_is_power2 x = Some i -> x = two_p i /\ i = Z.log2 x.
Proof.
  unfold Z_is_power2; intros. destruct x; try discriminate.
  destruct (P_is_power2 p) eqn:P; try discriminate.
  apply P_is_power2_sound in P. rewrite P; split; congruence.
Qed.

Corollary Z_is_power2_range:
  forall n x i,
  0 <= n -> 0 <= x < two_p n -> Z_is_power2 x = Some i -> 0 <= i < n.
Proof.
  intros.
  assert (x <> 0) by (red; intros; subst x; discriminate).
  apply Z_is_power2_sound in H1. destruct H1 as [P Q]. subst i.
  split. apply Z.log2_nonneg. apply Z.log2_lt_pow2. omega. rewrite <- two_p_equiv; tauto.
Qed.

Lemma Z_is_power2_complete:
  forall i, 0 <= i -> Z_is_power2 (two_p i) = Some i.
Proof.
Opaque Z.log2.
  assert (A: forall x i, Z_is_power2 x = Some i -> Z_is_power2 (2 * x) = Some (Z.succ i)).
  { destruct x; simpl; intros; try discriminate.
    change (2 * Z.pos p) with (Z.pos (xO p)); simpl.
    destruct (P_is_power2 p); inv H. rewrite <- Z.log2_double by xomega. auto.
  }
  induction i using Znatlike_ind; intros.
- replace i with 0 by omega. reflexivity.
- rewrite two_p_S by omega. apply A. apply IHi; omega.
Qed.

Definition Z_is_power2m1 (x: Z) : option Z := Z_is_power2 (Z.succ x).

Lemma Z_is_power2m1_sound:
  forall x i, Z_is_power2m1 x = Some i -> x = two_p i - 1.
Proof.
  unfold Z_is_power2m1; intros. apply Z_is_power2_sound in H. omega.
Qed.

Lemma Z_is_power2m1_complete:
  forall i, 0 <= i -> Z_is_power2m1 (two_p i - 1) = Some i.
Proof.
  intros. unfold Z_is_power2m1. replace (Z.succ (two_p i - 1)) with (two_p i) by omega.
  apply Z_is_power2_complete; auto.
Qed.

Lemma Z_is_power2m1_range:
  forall n x i,
  0 <= n -> 0 <= x < two_p n -> Z_is_power2m1 x = Some i -> 0 <= i <= n.
Proof.
  intros. destruct (zeq x (two_p n - 1)).
- subst x. rewrite Z_is_power2m1_complete in H1 by auto. inv H1; omega.
- unfold Z_is_power2m1 in H1. apply (Z_is_power2_range n (Z.succ x) i) in H1; omega.
Qed.

(** ** Relation between bitwise operations and multiplications / divisions by powers of 2 *)

(** Left shifts and multiplications by powers of 2. *)

Lemma Zshiftl_mul_two_p:
  forall x n, 0 <= n -> Z.shiftl x n = x * two_p n.
Proof.
  intros. destruct n; simpl.
  - omega.
  - pattern p. apply Pos.peano_ind.
    + change (two_power_pos 1) with 2. simpl. ring.
    + intros. rewrite Pos.iter_succ. rewrite H0.
      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
      change (two_power_pos 1) with 2. ring.
  - compute in H. congruence.
Qed.

(** Right shifts and divisions by powers of 2. *)

Lemma Zshiftr_div_two_p:
  forall x n, 0 <= n -> Z.shiftr x n = x / two_p n.
Proof.
  intros. destruct n; unfold Z.shiftr; simpl.
  - rewrite Zdiv_1_r. auto.
  - pattern p. apply Pos.peano_ind.
    + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div.
    + intros. rewrite Pos.iter_succ. rewrite H0.
      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
      change (two_power_pos 1) with 2.
      rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv.
      rewrite two_power_pos_nat. apply two_power_nat_pos. omega.
  - compute in H. congruence.
Qed.

(** ** Properties of [shrx] (signed division by a power of 2) *)

Lemma Zquot_Zdiv:
  forall x y,
  y > 0 ->
  Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.
Proof.
  intros. destruct (zlt x 0).
  - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)).
     + red. right; split. omega.
       exploit (Z_mod_lt (x + y - 1) y); auto.
       rewrite Z.abs_eq. omega. omega.
     + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)).
       rewrite <- Z_div_mod_eq. ring. auto. ring.
  - apply Zquot_Zdiv_pos; omega.
Qed.

Lemma Zdiv_shift:
  forall x y, y > 0 ->
  (x + (y - 1)) / y = x / y + if zeq (Z.modulo x y) 0 then 0 else 1.
Proof.
  intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H).
  set (q := x / y). set (r := x mod y). intros.
  destruct (zeq r 0).
  apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega.
  apply Zdiv_unique with (r - 1). rewrite H1. ring. omega.
Qed.

(** ** Size of integers, in bits. *)

Definition Zsize (x: Z) : Z :=
  match x with
  | Zpos p => Zpos (Pos.size p)
  | _ => 0
  end.

Remark Zsize_pos: forall x, 0 <= Zsize x.
Proof.
  destruct x; simpl. omega. compute; intuition congruence. omega.
Qed.

Remark Zsize_pos': forall x, 0 < x -> 0 < Zsize x.
Proof.
  destruct x; simpl; intros; try discriminate. compute; auto.
Qed.

Lemma Zsize_shiftin:
  forall b x, 0 < x -> Zsize (Zshiftin b x) = Z.succ (Zsize x).
Proof.
  intros. destruct x; compute in H; try discriminate.
  destruct b.
  change (Zshiftin true (Zpos p)) with (Zpos (p~1)).
  simpl. f_equal. rewrite Pos.add_1_r; auto.
  change (Zshiftin false (Zpos p)) with (Zpos (p~0)).
  simpl. f_equal. rewrite Pos.add_1_r; auto.
Qed.

Lemma Ztestbit_size_1:
  forall x, 0 < x -> Z.testbit x (Z.pred (Zsize x)) = true.
Proof.
  intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto.
  intros. rewrite Zsize_shiftin; auto.
  replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega.
  rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega.
Qed.

Lemma Ztestbit_size_2:
  forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false.
Proof.
  intros x0 POS0. destruct (zeq x0 0).
  - subst x0; intros. apply Ztestbit_0.
  - pattern x0; apply Zshiftin_pos_ind.
    + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin.
      rewrite zeq_false. apply Ztestbit_0. omega. omega.
    + intros. rewrite Zsize_shiftin in H1; auto.
      generalize (Zsize_pos' _ H); intros.
      rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega.
      omega. omega.
    + omega.
Qed.

Lemma Zsize_interval_1:
  forall x, 0 <= x -> 0 <= x < two_p (Zsize x).
Proof.
  intros.
  assert (x = x mod (two_p (Zsize x))).
    apply equal_same_bits; intros.
    rewrite Ztestbit_mod_two_p; auto.
    destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto.
    apply Zsize_pos; auto.
  rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto.
Qed.

Lemma Zsize_interval_2:
  forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x.
Proof.
  intros. set (N := Z.to_nat n).
  assert (Z.of_nat N = n) by (apply Z2Nat.id; auto).
  rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0.
  destruct (zeq x 0).
  subst x; simpl; omega.
  destruct (zlt n (Zsize x)); auto.
  exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega.
  rewrite Ztestbit_size_1. congruence. omega.
Qed.

Lemma Zsize_monotone:
  forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
Proof.
  intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos.
  exploit (Zsize_interval_1 y). omega.
  omega.
Qed.

author: PrincetonUniversity

repo: VST


text:
From iris.algebra Require Import gmap auth frac.
From iris.proofmode Require Import proofmode.
From lrust.lifetime Require Export lifetime.
From iris.prelude Require Import options.

(** Atomic persistent bors  *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
Definition at_bor `{!invGS Σ, !lftGS Σ userE} κ N (P : iProp Σ) :=
  (∃ i, &{κ,i}P ∗
    (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
     ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.

Section atomic_bors.
  Context `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) (N : namespace).

  Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
  Proof. solve_proper. Qed.
  Global Instance at_bor_contractive κ : Contractive (at_bor κ N).
  Proof. solve_contractive. Qed.
  Global Instance at_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
  Proof. solve_proper. Qed.

  Lemma at_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &at{κ, N} P -∗ &at{κ, N} P'.
  Proof.
    iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
    iApply (idx_bor_iff with "HPP' HP").
  Qed.

  Global Instance at_bor_persistent κ N P : Persistent (&at{κ, N} P) := _.

  Lemma bor_share E κ :
    N ## lftN → &{κ}P ={E}=∗ &at{κ, N}P.
  Proof.
    iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
    iExists i. iFrame "#".
    iLeft. iSplitR; first done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
  Qed.

  Lemma bor_share_lftN E κ :
    ↑lftN ⊆ E → &{κ}P ={E}=∗ &at{κ, lftN}P.
  Proof.
    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
    iExists i. iFrame "#". subst.
    iRight. iSplitR; first done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
  Qed.

  Lemma at_bor_acc E κ :
    ↑lftN ⊆ E → ↑N ⊆ E →
    lft_ctx -∗ &at{κ,N}P ={E,E∖↑N∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑N∖↑lftN,E}=∗ True) ∨
               [†κ] ∗ |={E∖↑N∖↑lftN,E}=> True.
  Proof.
    iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
    - iInv N as ">Hi" "Hclose". iMod (idx_bor_atomic_acc with "LFT Hidx Hi")
        as "[[HP Hclose']|[H† Hclose']]"; first solve_ndisj.
      + iLeft. iFrame. iIntros "!>HP". iMod ("Hclose'" with "HP"). by iApply "Hclose".
      + iRight. iFrame. iIntros "!>". iMod "Hclose'". by iApply "Hclose".
    - subst. rewrite difference_twice_L. iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
      iMod ("Hclose" with "[Hq'1]") as "_"; first solve_ndisj.
      iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]"; first done.
      + iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
      + iRight. iFrame. iIntros "!>". by iMod "Hclose".
  Qed.

  Lemma at_bor_acc_tok E q κ :
    ↑lftN ⊆ E → ↑N ⊆ E →
    lft_ctx -∗ &at{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗ ▷P ∗ (▷P ={E∖↑N,E}=∗ q.[κ]).
  Proof.
    iIntros (??) "#LFT #HP Hκ". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
    - iInv N as ">Hi" "Hclose".
      iMod (idx_bor_acc with "LFT Hidx Hi Hκ") as "[$ Hclose']"; first solve_ndisj.
      iIntros "!> H". iMod ("Hclose'" with "H") as "[? $]". by iApply "Hclose".
    - iMod (at_bor_acc with "LFT []") as "[[$ Hclose]|[H† _]]"; try done.
      + iExists i. auto.
      + subst. rewrite difference_twice_L. iIntros "!>HP". by iMod ("Hclose" with "HP").
      + iDestruct (lft_tok_dead with "Hκ H†") as "[]".
  Qed.

  Lemma at_bor_shorten κ κ': κ ⊑ κ' -∗ &at{κ',N}P -∗ &at{κ,N}P.
  Proof.
    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
      by iApply (idx_bor_shorten with "H⊑").
  Qed.

  Lemma at_bor_fake E κ:
    ↑lftN ⊆ E → N ## lftN → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,N}P.
  Proof.
    iIntros (??) "#LFT#H†". iApply (bor_share with "[>]"); try done.
    by iApply (bor_fake with "LFT H†").
  Qed.

  Lemma at_bor_fake_lftN E κ:
    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,lftN}P.
  Proof.
    iIntros (?) "#LFT#H†". iApply (bor_share_lftN with "[>]"); try done.
    by iApply (bor_fake with "LFT H†").
  Qed.
End atomic_bors.

Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) E κ :
  ↑lftN ⊆ E →
  lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
             [†κ] ∗ |={E∖↑lftN,E}=> True.
Proof. intros. by rewrite (at_bor_acc _ lftN) // difference_twice_L. Qed.

Global Typeclasses Opaque at_bor.

author: lambdaxymox

repo: LambdaRust-coq


text:
Require Export SetoidClass.
Require Export RelationClasses.
Require Import Lia.
Require Export FOPL.Basic.

Set Implicit Arguments.

(**)
  Lemma nfn_e : forall (t : Type) p, (~ forall (x : t), ~ p x) -> exists x, p x.
  Proof.
    intros.
    apply NNPP.
    intro.
    contradict H.
    intros. intro.
    assert (exists x : t, p x).
    exists x. auto.
    auto.
  Qed.

  Lemma e_nfn : forall (t : Type) p, (exists x, p x) -> (~ forall (x : t), ~ p x).
  Proof.
    intros.
    intro.
    destruct H.
    specialize (H0 x).
    auto.
  Qed.
(**)

Section TarskiSemantics.

  Variable L : Lang.

  Class Model :=
  {
    Dom : Type;
    SDom :> Setoid Dom;
    cnsM : Dom;
    Fc0M : fc0 -> Dom;
    Fc1M : fc1 -> Dom -> Dom;
    Fc2M : fc2 -> Dom -> Dom -> Dom;
    Pd0M : pd0 -> Prop;
    Pd1M : pd1 -> Dom -> Prop;
    Pd2M : pd2 -> Dom -> Dom -> Prop;

    ProperFc1M :> forall (c : fc1), Proper (equiv ==> equiv) (Fc1M c);
    ProperFc2M :> forall (c : fc2), Proper (equiv ==> equiv ==> equiv) (Fc2M c);
    ProperPd1M :> forall (c : pd1), Proper (equiv ==> equiv) (Pd1M c);
    ProperPd2M :> forall (c : pd2), Proper (equiv ==> equiv ==> equiv) (Pd2M c)
  }.

  Fixpoint Valt
  (M : Model)
  (s : nat -> Dom)
  (t : Term) : Dom :=
    match t with
    | 'm          => s m
    | [O]         => cnsM
    | Fc0 c     => Fc0M c
    | Fc1 c x   => Fc1M c (Valt M s x)
    | Fc2 c x y => Fc2M c (Valt M s x) (Valt M s y)
    end.

  Fixpoint Valp
  (M : Model)
  (s : nat -> Dom)
  (p : Formula) : Prop :=
    match p with
    | x [=] y     => (Valt M s x) == (Valt M s y)
    | Pd0 c     => Pd0M c
    | Pd1 c x   => Pd1M c (Valt M s x)
    | Pd2 c x y => Pd2M c (Valt M s x) (Valt M s y)
    | q [->] r    => (Valp M s q) -> (Valp M s r)
    | [~] q       => ~ (Valp M s q)
    | fal q       => forall (t : Dom), Valp M (t;s) q
    end.

End TarskiSemantics.

  Definition models {L : Lang} M p := forall s, Valp M s p.
  Notation "M |= p" := (models M p) (at level 99).
  Definition modelsTh {L : Lang} M (T :Th) := forall p, T p -> M |= p.
  Notation "M |=th T" := (modelsTh M T) (at level 99).
  Definition SValid {L : Lang} (T : Th) p := forall M, modelsTh M T -> M |= p.
  Notation "T ||= p" := (SValid T p) (at level 99).
  Definition function_equiv {L : Lang} {M : Model L} (s0 s1 : nat -> @Dom _ _) := forall n, s0 n == s1 n.
  Notation " x ~ y " := (function_equiv x y) (at level 70, no associativity).

Instance Valt_s_rew : forall (L : Lang) M, Proper (function_equiv ==> eq ==> equiv) (Valt M).
Proof.
  unfold Proper, respectful.
  intros L M s0 s1 H.
  assert(forall t, Valt M s0 t == Valt M s1 t).
  - induction t.
    + simpl. auto.
    + simpl. reflexivity.
    + simpl. reflexivity.
    + simpl.
      rewrite <- IHt.
      reflexivity.
    + simpl.
      rewrite <- IHt1.
      rewrite <- IHt2.
      reflexivity.
  - intros.
    rewrite <- H1.
    auto.
Qed.

Instance Valp_s_rew : forall (L : Lang) M, Proper (function_equiv ==> eq ==> iff) (Valp M).
Proof.
  unfold Proper, respectful.
  intros L M s0 s1 H.
  assert (forall q s0 s1, (s0 ~ s1) -> Valp M s0 q <-> Valp M s1 q).
  - induction q.
    + simpl.
      intros.
      rewrite <- H0.
      reflexivity.
    + simpl.
      intros.
      reflexivity.
    + simpl.
      intros.
      rewrite <- H0.
      reflexivity.
    + simpl.
      intros.
      rewrite <- H0.
      reflexivity.
    + simpl.
      intros.
      rewrite <- (IHq1 s2 s3).
      rewrite <- (IHq2 s2 s3).
      reflexivity.
      auto. auto.
    + simpl.
      intros.
      rewrite <- (IHq s2 s3).
      reflexivity.
      auto.
    + simpl.
      intros.
      assert (forall t, Valp M (t;s2) q <-> Valp M (t;s3) q).
      intros. apply IHq.
      {unfold function_equiv. destruct n. simpl. reflexivity. simpl. auto. }
      split.
      intros.
      rewrite <- H1.
      auto.
      intros.
      rewrite -> H1.
      auto.
  - intros.
    rewrite <- H1.
    auto.
Qed.

Section Semantics.

  Variable L : Lang.

  Lemma M_and_destruct : forall M p q, (M |= p [/\] q) <-> (M |= p) /\ (M |= q).
  Proof.
    unfold models.
    simpl.
    intros.
    split.
    - intros.
      split.
      + intros.
        specialize (H s).
        apply NNPP.
        contradict H.
        auto.
      + intros.
        specialize (H s).
        apply NNPP.
        contradict H.
        auto.
    - intros.
      destruct H.
      intro.
      apply H1.
      auto. auto.
  Qed.

  Lemma M_iff_destruct : forall M p q, (M |= p [<->] q) <-> (M |= p [->] q) /\ (M |= q [->] p).
  Proof.
    intros M p q.
    apply M_and_destruct.
  Qed.

  Lemma M_fal : forall M p s, (Valp M s (fal p)) <-> (forall x, Valp M (x;s) p).
  Proof.
    simpl.
    intros.
    reflexivity.
  Qed.

  Lemma M_ext : forall M p s, (Valp M s (ext p)) <-> (exists x, Valp M (x;s) p).
  Proof.
    simpl.
    intros.
    split.
    intros.
    apply nfn_e. auto.
    intros.
    apply e_nfn.
    auto.
  Qed.

  Lemma lc_eq : forall M t s c, Valt M s (rewc c t) == Valt M (fun x => Valt M s (c x)) t.
  Proof.
    induction t.
    - simpl.
      reflexivity.
    - simpl.
      reflexivity.
    - simpl.
      reflexivity.
    - simpl.
      intros.
      rewrite <- IHt.
      reflexivity.
    - simpl.
      intros.
      rewrite <- IHt1.
      rewrite <- IHt2.
      reflexivity.
  Qed.

  Lemma shiftc_eq : forall M t s c, Valt M s c == Valt M (t; s) (sfc c).
  Proof.
    unfold sfc.
    induction c.
    - simpl. reflexivity.
    - simpl. reflexivity.
    - simpl. reflexivity.
    - simpl.
      rewrite <- IHc.
      reflexivity.
    - simpl.
      rewrite <- IHc1.
      rewrite <- IHc2.
      reflexivity.
  Qed.

  Lemma lp_iff0 : forall M p s0 s1 u,
    (forall n, s0 n == Valt M s1 (u n)) ->
    Valp M s0 p <-> Valp M s1 (p.[u]).
  Proof.
    intros M.
    induction p.
    - simpl.
      intros.
      rewrite -> lc_eq. rewrite -> lc_eq.
      assert (s0 ~ (fun x : nat => Valt M s1 (u x))).
      {unfold function_equiv. auto. }
      rewrite <- H0.
      reflexivity.
    - simpl.
      intros.
      reflexivity.
    - simpl.
      intros.
      rewrite -> lc_eq.
      assert (s0 ~ (fun x : nat => Valt M s1 (u x))).
      {unfold function_equiv. auto. }
      rewrite <- H0.
      reflexivity.
    - simpl.
      intros.
      rewrite -> lc_eq. rewrite -> lc_eq.
      assert (s0 ~ (fun x : nat => Valt M s1 (u x))).
      {unfold function_equiv. auto. }
      rewrite <- H0.
      reflexivity.
    - simpl.
      intros.
      rewrite <- (IHp1 s0 s1). rewrite <- (IHp2 s0 s1).
      reflexivity.
      auto. auto.
    - simpl.
      intros.
      rewrite <- (IHp s0 s1).
      reflexivity.
      auto.
    - simpl.
      intros.
      assert (miff : forall t, Valp M (t; s0) p <-> Valp M (t; s1) (p.['0; fun x => sfc (u x)])).
      + intros.
        apply IHp.
        destruct n.
        simpl. reflexivity.
        simpl. rewrite <- shiftc_eq. auto.
      + split.
        intros.
        apply miff. auto.
        intros.
        apply miff. auto.
  Qed.

  Lemma lp_iff1 : forall M p s u,
    Valp M (fun n => Valt M s (u n)) p <-> Valp M s (p.[u]).
  Proof.
    intros.
    apply lp_iff0.
    reflexivity.
  Qed.

  Lemma mthsfT: forall M T, modelsTh M T -> modelsTh M (sfT T).
  Proof.
    unfold modelsTh, sf, models.
    intros.
    destruct H0.
    unfold sf.
    rewrite <- lp_iff1.
    apply H.
    auto.
  Qed.

  Theorem Soundness : forall T p, (T ||- p) -> (T ||= p).
  Proof.
    unfold SValid.
    intros.
    unfold models.
    induction H.
    - simpl.
      intros.
      apply IHprovable.
      apply mthsfT.
      auto.
    - intros.
      simpl in IHprovable2.
      auto.
    - intros.
      apply H0.
      auto.
    - simpl. auto.
    - simpl. auto.
    - simpl.
      intros.
      apply NNPP.
      intro.
      apply H.
      auto. auto.
    - simpl.
      intros.
      rewrite <- lp_iff1.
      assert ((Valt M s t; s) = fun n => Valt M s ((t; \0) n)).
      + apply functional_extensionality.
        intros.
        destruct x.
        simpl. auto.
        simpl. auto.
      + rewrite <- H1.
        auto.
    - simpl. auto.
    - simpl.
      intros.
      unfold sf.
      rewrite <- lp_iff1.
      assert (s = fun n => Valt M (t;s) '(S n)).
      + apply functional_extensionality.
        intros.
        simpl. auto.
      + rewrite <-  H1.
        auto.
    - simpl.
      intros.
      reflexivity.
    - simpl.
      intros.
      rewrite <- lp_iff1.
      rewrite <- lp_iff1 in H1.
      assert ((fun n => Valt M s ((t; \0) n)) ~ (fun n => Valt M s ((u; \0) n))).
      + unfold function_equiv.
        destruct n.
        simpl. auto.
        simpl. reflexivity.
      + rewrite <- H2.
        auto.
  Qed.

  Lemma Val_eq : forall M t s0 s1,
    (forall n, n < Art t -> s0 n == s1 n) ->
    Valt M s0 t == Valt M s1 t.
  Proof.
    intros M.
    induction t.
    - simpl.
      intros.
      auto.
    - simpl. intros. reflexivity.
    - simpl. intros. reflexivity.
    - simpl. intros.
      rewrite (IHt _ s1).
      reflexivity.
      auto.
    - simpl. intros.
      rewrite (IHt1 _ s1).
      rewrite (IHt2 _ s1).
      reflexivity.
      intros.
      apply H.
      apply lt_lt_max_r. auto.
      intros.
      apply H.
      apply lt_lt_max_l. auto.
  Qed.

  Lemma Val_iff : forall M p s0 s1,
    (forall n, n < Ar p -> s0 n == s1 n) ->
    Valp M s0 p == Valp M s1 p.
  Proof.
    intros M.
    induction p.
    - simpl.
      intros.
      rewrite (Val_eq _ t _ s1).
      rewrite (Val_eq _ t0 _ s1).
      reflexivity.
      intros. apply H. apply lt_lt_max_r. auto.
      intros. apply H. apply lt_lt_max_l. auto.
    - simpl.
      intros.
      reflexivity.
    - simpl.
      intros.
      rewrite (Val_eq _ t _ s1).
      reflexivity.
      auto.
    - simpl.
      intros.
      rewrite (Val_eq _ t _ s1).
      rewrite (Val_eq _ t0 _ s1).
      reflexivity.
      intros. apply H. apply lt_lt_max_r. auto.
      intros. apply H. apply lt_lt_max_l. auto.
    - simpl.
      intros.
      rewrite (IHp1 s0 s1).
      rewrite (IHp2 s0 s1).
      reflexivity.
      intros. apply H. apply lt_lt_max_r. auto.
      intros. apply H. apply lt_lt_max_l. auto.
    - simpl.
      intros.
      rewrite (IHp s0 s1).
      reflexivity.
      auto.
    - simpl.
      intros.
      assert(forall t, Valp M (t; s0) p == Valp M (t; s1) p).
      + intros.
        apply IHp.
        intros.
        destruct n.
        simpl. reflexivity.
        simpl.
        apply H.
        lia.
      + split.
        intros. apply H0. auto.
        intros. apply H0. auto.
  Qed.

End Semantics.

Section DSetoid.

  Variable A : Type.

  Lemma equiveq : @Equivalence A eq.
  Proof.
    split.
    auto.
    auto.
    unfold Transitive.
    intros.
    rewrite -> H.
    auto.
  Qed.

  Instance DSetoid : Setoid A := {equiv:=eq; setoid_equiv:=equiveq}.

End DSetoid.

author: iehality

repo: FOPL

save_path: github-repos/coq/iehality-FOPL


text:
(**********************************************
  iALC - Labeled Natural Deduction System
  Author: Bernardo Alkmim (bpalkmim@gmail.com)
  TODO
**********************************************)

Require Export Unicode.Utf8.
Require Export Relations_1.
Require Export Ensembles.
Require Export List.
(*Require Export iALC_NaturalDeduction_Definitions.*)
Set Implicit Arguments.

Module iALC_ND_Labels.

(* Definition of variables, used in the Completeness proof. *)
Parameter ConV : Set.

(* Nominal variables. *)
Parameter NomV : Set.

(* Role Variables. *)
Parameter RoleV : Set.

(* Labels. *)
(* TODO *)

(* Constructor for nominals. *)
Inductive Nom : Set :=
  AtomN : NomV → Nom.

(* Constructor for roles. *)
Inductive Role : Set :=
  AtomR : RoleV → Role.

(* Constructor for labels. *)
Inductive Label : Set :=
  | ExisL : RoleV → Label
  | UnivL : RoleV → Label
  | NegL : Label → Label
.

(* Constructor for Concepts. *)
Inductive Concept : Set :=
  | Top : Concept
  | Bot : Concept
  | AtomC : Concept
  (*| Neg : Concept → Concept -- moved to Formula (defined by subj) *)
  | Conj : Concept → Concept → Concept
  | Disj : Concept → Concept → Concept
  (*| Subj : Concept → Concept → Concept -- moved to Formula *)
  | Univ : Role → Concept → Concept
  | Exis : Role → Concept → Concept
.

(* Formulas are concepts with a list of labels. *)
(* TODO possible problems may arise with ⊑, ∀, ∃, ¬, rest seems ok *)
Inductive Formula : Set :=
  | Simple : Concept → list Label → Formula
  | NCon : Nom → Formula → Formula (* for nominals *)
  | Neg : Formula → list Label → Formula
  | Subj : Formula → Formula → list Label → Formula
.

(* Useful notations. *)
Notation "' C" := (AtomC C) (at level 1).
Notation "# R" := (AtomR R) (at level 1).
Notation "$ N" := (NomV N) (at level 1).
Notation "⊤" := (Simple Top nil) (at level 0).
Notation "⊥" := (Simple Bot nil) (at level 0).
Notation "C ⊓ D" := (Conj C D) (at level 15, right associativity).
Notation "C ⊔ D" := (Disj C D) (at level 15, right associativity).
Notation "¬ C" := (Neg C) (at level 75, right associativity).
Notation "x ∈ C" := (NCon x C) (at level 25, right associativity).
(*
Notation "C ⊑ D" := (Subj C D nil) (at level 16, right associativity).
Notation "( C ⊑ D ) L" := (Subj C D L) (at level 16, right associativity).
Notation "∀ R . C" := (Univ R C nil) (at level 14, right associativity).
Notation "( ∀ R . C ) L" := (Univ R C L) (at level 14, right associativity).
Notation "∃ R . C" := (Exis R C nil) (at level 14, right associativity).
Notation "( ∃ R . C ) L" := (Exis R C L) (at level 14, right associativity).
*)

(* Natural Deduction Rules *)
(* TODO see how to force ¬L, ∀L, ∃L (lists restricted to negations, univ restrictions
        and exis restrictions, respectively). Perhaps only semantically possible. *)
Reserved Notation "Γ ⊢ A" (at level 80).
Inductive NDcalc : list Formula → Formula → Set :=
  (* Without nominals *)
  | SubjI : ∀ Γ α β L, α::Γ ⊢ β → Γ ⊢ (Subj α β L) (* α and β are already formulas with their respective lists of labels *)
  | SubjE : ∀ Γ α β L, Γ ⊢ α → Γ ⊢ (Subj α β L) → Γ ⊢ β
  | NegI : ∀ Γ α L, α::Γ ⊢ ⊥ → Γ ⊢ ((¬α) L) (* Ver como definir ¬L *)
  | NegE : ∀ Γ α L, Γ ⊢ α → Γ ⊢ ((¬α) L) → Γ ⊢ ⊥
  | ConjI : ∀ Γ α β L, Γ ⊢ (Simple α L) → Γ ⊢ (Simple β L) → Γ ⊢ (Simple (α ⊓ β) L) (* Garantia de ter apenas ∀ : semântica?*)
  | ConjE1 : ∀ Γ α β L, Γ ⊢ (Simple (α ⊓ β) L) → Γ ⊢ (Simple α L)
  | ConjE2 : ∀ Γ α β L, Γ ⊢ (Simple (α ⊓ β) L) → Γ ⊢ (Simple β L)
  | DisjI1 : ∀ Γ α β L, Γ ⊢ (Simple α L) → Γ ⊢ (Simple (α ⊔ β) L) (* Garantia de ter apenas ∃ : semântica?*)
  | DisjI2 : ∀ Γ α β L, Γ ⊢ (Simple β L) → Γ ⊢ (Simple (α ⊔ β) L)
  | DisjE : ∀ Γ α β δ L, Γ ⊢ (Simple (α ⊔ β) L) → (Simple α L)::Γ ⊢ δ → (Simple β L)::Γ ⊢ δ → Γ ⊢ δ
  | Efq : ∀ Γ δ, Γ ⊢ ⊥ → Γ ⊢ δ
  (* With nominals *)
  | SubjIn : ∀ Γ α β x L1 L2 L, (x ∈ (Simple α L1))::Γ ⊢ (x ∈ (Simple β L2)) → Γ ⊢ (x ∈ (Subj (Simple α L1) (Simple β L2) L))
  | SubjEn : ∀ Γ α β x L1 L2 L, Γ ⊢ (x ∈ (Simple α L1)) → Γ ⊢ (x ∈ (Subj (Simple α L1) (Simple β L2) L)) → Γ ⊢ (x ∈ (Simple β L2))
  | NegIn : ∀ Γ α x L, (x ∈ α)::Γ ⊢ (x ∈ ⊥) → Γ ⊢ (x ∈ ((¬α) L))
  | NegEn : ∀ Γ α x L, Γ ⊢ (x ∈ α) → Γ ⊢ (x ∈ ((¬α) L)) → Γ ⊢ (x ∈ ⊥)
  | ConjIn : ∀ Γ α β x L, Γ ⊢ (x ∈ (Simple α L)) → Γ ⊢ (x ∈ (Simple β L)) → Γ ⊢ (x ∈ (Simple (α ⊓ β) L))
  | ConjE1n : ∀ Γ α β x L, Γ ⊢ (x ∈ (Simple (α ⊓ β) L)) → Γ ⊢ (x ∈ (Simple α L))
  | ConjE2n : ∀ Γ α β x L, Γ ⊢ (x ∈ (Simple (α ⊓ β) L)) → Γ ⊢ (x ∈ (Simple β L))
  | DisjI1n : ∀ Γ α β x L, Γ ⊢ (x ∈ (Simple α L)) → Γ ⊢ (x ∈ (Simple (α ⊔ β) L))
  | DisjI2n : ∀ Γ α β x L, Γ ⊢ (x ∈ (Simple β L)) → Γ ⊢ (x ∈ (Simple (α ⊔ β) L))
  | DisjEn : ∀ Γ α β δ x L, Γ ⊢ (x ∈ (Simple (α ⊔ β) L)) → (x ∈ (Simple α L))::Γ ⊢ δ → (x ∈ (Simple β L))::Γ ⊢ δ → Γ ⊢ δ
  | Efqn : ∀ Γ δ x, Γ ⊢ (x ∈ ⊥) → Γ ⊢ δ
  (* ∃ and ∀ rules - how to guarantee x ≼ y ? Only semantically *)
  | ExisI : ∀ Γ α R x y L, Γ ⊢ (y ∈ (Simple α ((ExisL R)::L))) → Γ ⊢ x ∈ (Simple (Exis (#R) α) L)
  | ExisE : ∀ Γ α R x y L, Γ ⊢ x ∈ (Simple (Exis (#R) α) L) → Γ ⊢ (y ∈ (Simple α ((ExisL R)::L)))
  | UnivI : ∀ Γ α R x y L, Γ ⊢ (y ∈ (Simple α ((UnivL R)::L))) → Γ ⊢ x ∈ (Simple (Univ (#R) α) L)
  | UnivE : ∀ Γ α R x y L, Γ ⊢ x ∈ (Simple (Univ (#R) α) L) → Γ ⊢ (y ∈ (Simple α ((UnivL R)::L)))
  (* Structural rules TODO *)
  | Hyp : ∀ Γ α, In α Γ → Γ ⊢ α
  where "Γ ⊢ A" := (NDcalc Γ A).

(* Casos de teste *)
(* Sem Nominals *)
Lemma ConjComm : ∀ Γ C D L, Γ ⊢ (Subj (Simple (D ⊓ C) L) (Simple (C ⊓ D) L) nil).
Proof.
  intros.
  apply SubjI.
  apply ConjI.
  - apply ConjE2 with (α := D).
    apply Hyp. apply in_eq.
  - apply ConjE1 with (β := C).
    apply Hyp. apply in_eq.
Qed.

Lemma DisjComm : ∀ Γ C D L, Γ ⊢ (Subj (Simple (D ⊔ C) L) (Simple (C ⊔ D) L) nil).
Proof.
  intros.
  apply SubjI.
  apply DisjE with (α := D) (β := C) (L := L).
  - apply Hyp. apply in_eq.
  - apply DisjI2.
    apply Hyp. apply in_eq.
  - apply DisjI1.
    apply Hyp. apply in_eq.
Qed.

Lemma SubjABA : ∀ Γ C D L1 L2 L3 L4, (* Γ ⊢ C ⊑ (C ⊑ D) *)
  Γ ⊢ (Subj (Simple C L1) (Subj (Simple D L2) (Simple C L1) L3) L4).
Proof.
  intros.
  apply SubjI.
  apply SubjI.
  apply Hyp. apply in_cons. apply in_eq.
Qed.

Lemma ModusTollensAlmost : ∀ Γ C D L1 L2 L3 L4, (* Γ ⊢ (C ⊑ D) ⊑ (¬D ⊑ ¬C) *)
  Γ ⊢ (Subj (Subj (Simple C L1) (Simple D L2) L1) (Subj ((¬(Simple D L2)) L2) ((¬(Simple C L1)) L1) L3) L4).
Proof.
  intros.
  apply SubjI.
  apply SubjI.
  apply NegI.
  apply NegE with (α := Simple D L2) (L := L2).
  - apply SubjE with (α := Simple C L1) (L:= L1).
    * apply Hyp. apply in_eq.
    * apply Hyp. apply in_cons. apply in_cons. apply in_eq.
  - apply Hyp. apply in_cons. apply in_eq.
Qed.

Lemma EfqTest : ∀ Γ C D G L, (* (C ⊑ D :: (C ⊓ ¬D) :: Γ) ⊢ G *)
  (() :: (Simple (C ⊓ ¬(Simple D L)) L) :: Γ) ⊢ G.
Proof.
  intros.
  apply Efq.
  apply @NegE with (α := C).
  - apply @ConjE1 with (β := ¬D).
    apply Hyp. apply in_cons. apply in_eq.
  - apply NegI.
    apply @NegE with (α := D).
    * apply @SubjE with (α := C).
      + apply Hyp. apply in_eq.
      + apply Hyp. apply in_cons. apply in_eq.
    * apply @ConjE2 with (α := C).
      apply Hyp. apply in_cons. apply in_cons. apply in_eq.
Qed.

(* Com Nominals *)
Lemma ConjCommN : ∀ Γ C D x, Γ ⊢ (x ∈ ((D ⊓ C) ⊑ (C ⊓ D))).
Proof.
  intros.
  apply SubjIn.
  apply ConjIn.
  - apply @ConjE2n with (α := D).
    apply Hyp. apply in_eq.
  - apply @ConjE1n with (β := C).
    apply Hyp. apply in_eq.
Qed.

Lemma DisjCommN : ∀ Γ C D x, Γ ⊢ (x ∈ ((D ⊔ C) ⊑ (C ⊔ D))).
Proof.
  intros.
  apply SubjIn.
  apply @DisjEn with (x := x) (α := D) (β := C).
  - apply Hyp. apply in_eq.
  - apply DisjI2n.
    apply Hyp. apply in_eq.
  - apply DisjI1n.
    apply Hyp. apply in_eq.
Qed.

Lemma SubjABAN : ∀ Γ C D x, Γ ⊢ (x ∈ (C ⊑ (D ⊑ C))).
Proof.
  intros.
  apply SubjIn.
  apply SubjIn.
  apply Hyp. apply in_cons. apply in_eq.
Qed.

Lemma ModusTollensAlmostN : ∀ Γ C D x, Γ ⊢ (x ∈ ((C ⊑ D) ⊑ ((¬D) ⊑ ¬C))).
Proof.
  intros.
  apply SubjIn.
  apply SubjIn.
  apply NegIn.
  apply NegEn with (α := D).
  - apply SubjEn with (α := C).
    * apply Hyp. apply in_eq.
    * apply Hyp. apply in_cons. apply in_cons. apply in_eq.
  - apply Hyp. apply in_cons. apply in_eq.
Qed.

Lemma EfqTestN : ∀ Γ C D G x, (x ∈ C ⊑ D :: x ∈ (C ⊓ ¬D) :: Γ) ⊢ x ∈ G.
Proof.
  intros.
  apply @Efqn with (x := x).
  apply @NegEn with (α := C).
  - apply @ConjE1n with (β := ¬D).
    apply Hyp. apply in_cons. apply in_eq.
  - apply NegIn.
    apply @NegEn with (α := D).
    * apply @SubjEn with (α := C).
      + apply Hyp. apply in_eq.
      + apply Hyp. apply in_cons. apply in_eq.
    * apply @ConjE2n with (α := C).
      apply Hyp. apply in_cons. apply in_cons. apply in_eq.
Qed.

Lemma proof1 : ∀ Γ C D R x (y : Nom), Γ ⊢ (x ∈ ((Univ R (C ⊑ D)) ⊑ ((Univ R C)⊑(Univ R D)))).
Proof.
  intros.
  apply SubjIn.
  apply SubjIn.
  apply @UnivI with (y := y).

End iALC_ND.

author: Bpalkmim

repo: iALC

save_path: github-repos/coq/Bpalkmim-iALC


text:
Require Import Eqdep String Arith Omega Program Relations Bool.
Require Import List.
Open Scope string_scope.
Open Scope list_scope.

Ltac inductN n :=
  match goal with
    | [ |- forall x : ?E, _ ] =>
      match type of E with
        | Prop =>
          let H := fresh in intro H;
            match n with
              | 1 => dependent induction H
              | S ?n' => inductN n'
            end
        | _ => intro; inductN n
      end
  end.

Ltac induct e := inductN e || dependent induction e.

Ltac invert' H := inversion H; clear H; subst.

Ltac invertN n :=
  match goal with
    | [ |- forall x : ?E, _ ] =>
      match type of E with
        | Prop =>
          let H := fresh in intro H;
            match n with
              | 1 => invert' H
              | S ?n' => invertN n'
            end
        | _ => intro; invertN n
      end
  end.

Ltac invert e := invertN e || invert' e.

Ltac invert0 e := invert e; fail.
Ltac invert1 e := invert0 e || (invert e; []).
Ltac invert2 e := invert1 e || (invert e; [|]).

Ltac simplify :=
                repeat match goal with
                       | [ H : True |- _ ] => clear H
                       end;
                repeat progress (simpl in *; intros; try autorewrite with core in *).
Ltac propositional := intuition idtac.

Ltac linear_arithmetic := intros;
    repeat match goal with
           | [ |- context[max ?a ?b] ] =>
             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
               rewrite Heq in *; clear Heq
           | [ _ : context[max ?a ?b] |- _ ] =>
             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
               rewrite Heq in *; clear Heq
           | [ |- context[min ?a ?b] ] =>
             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
               rewrite Heq in *; clear Heq
           | [ _ : context[min ?a ?b] |- _ ] =>
             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
               rewrite Heq in *; clear Heq
           end; omega.

Ltac equality := intuition congruence.

Ltac cases E :=
  ((is_var E; destruct E)
   || match type of E with
      | {_} + {_} => destruct E
      | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
      end);
  repeat match goal with
         | [ H : _ = left _ |- _ ] => clear H
         | [ H : _ = right _ |- _ ] => clear H
         end.

Global Opaque max min.

Infix "==n" := eq_nat_dec (no associativity, at level 50).
Infix "<=?" := le_lt_dec.

Ltac first_order := firstorder idtac.

(** * Model checking *)

Lemma eq_iff : forall P Q,
    P = Q
    -> (P <-> Q).
Proof.
  equality.
Qed.

Inductive ordering (n m : nat) :=
| Lt (_ : n < m)
| Eq (_ : n = m)
| Gt (_ : n > m).

Local Hint Constructors ordering.
Local Hint Extern 1 (_ < _) => omega.
Local Hint Extern 1 (_ > _) => omega.

Theorem totally_ordered : forall n m, ordering n m.
Proof.
  induction n; destruct m; simpl; eauto.
  destruct (IHn m); eauto.
Qed.

Ltac total_ordering N M := destruct (totally_ordered N M).

Ltac inList x xs :=
  match xs with
  | (x, _) => constr:(true)
  | (_, ?xs') => inList x xs'
  | _ => constr:(false)
  end.

Require Import Classical.
Ltac excluded_middle P := destruct (classic P).

author: asya-bergal

repo: cross-crypto