text:
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Classical.
Require Import ClassicalChoice.
Require Import structures.Category.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Upset.
Require Import lattices.FCD.

Module Lazy <: LatticeCategory.

  Section DEF.
    Context {L M : cdlattice} (f : L -> M).

    Class NSupMorphism :=
      mor_sup: forall {I} (x : I -> L), inhabited I -> f (lsup x) = lsup (f @ x).

    Class Morphism := mor : NSupMorphism /\ Inf.Morphism f.
    Global Instance cmor_sup : Morphism -> NSupMorphism := @proj1 _ _.
    Global Instance cmor_inf : Morphism -> Inf.Morphism f := @proj2 _ _.

    Global Instance mor_ref :
      Morphism -> PosetMorphism f.
    Proof.
      intros [_ H].
      apply Inf.mor_ref; auto.
    Qed.
  End DEF.

  Lemma id_mor (L : cdlattice) :
    Morphism (fun x:L => x).
  Proof.
    firstorder.
  Qed.

  Lemma compose_mor {A B C : cdlattice} (g : B -> C) (f : A -> B) :
    Morphism f ->
    Morphism g ->
    Morphism (fun a => g (f a)).
  Proof.
    split.
    - intros I x Hx. rewrite (mor_sup f), (mor_sup g); auto.
    - apply Inf.compose_mor; typeclasses eauto.
  Qed.

End Lazy.

Module LBot.

  (** We construct the extended the lattice with a new ⊥ by using sets
    with at most one element. *)

  Inductive opt {A} :=
    mkopt (s : A -> Prop) (Hs : forall a b, s a -> s b -> a = b).

  Arguments opt : clear implicits.
  Definition is {A} : opt A -> A -> Prop := fun '(mkopt a _) => a.

  Lemma is_unique {A} (x : opt A) (a b : A) :
    is x a -> is x b -> a = b.
  Proof.
    destruct x; auto.
  Qed.

  Lemma opt_eq {A} (x y : opt A) :
    (forall a, is x a <-> is y a) -> x = y.
  Proof.
    destruct x as [x Hx], y as [y Hy]. cbn. intros H.
    cut (x = y).
    - intro. subst. f_equal. apply proof_irrelevance.
    - apply functional_extensionality. intro.
      apply propositional_extensionality; auto.
  Qed.

  Section DEF.
    Context {L M : cdlattice}.

    (** ** Poset *)

    Program Definition Fposet : poset :=
      {|
        poset_carrier := opt L;
        ref x y := forall l, is x l -> exists m, is y m /\ ref l m;
      |}.

    Next Obligation.
      split.
      - firstorder.
      - intros [x Hx] [y Hy] [z Hz] Hxy Hyz l Hl. cbn in *.
        destruct (Hxy l) as (m & Hm & Hlm); auto.
        destruct (Hyz m) as (n & Hn & Hmn); auto.
        exists n. split; auto. transitivity m; auto.
    Qed.

    Next Obligation.
      intros [x Hx] [y Hy] Hxy Hyx. cbn in *.
      apply opt_eq. intros l. split.
      - intros Hl.
        destruct (Hxy l) as (m & Hm & Hlm); auto.
        destruct (Hyx m) as (n & Hn & Hmn); auto.
        assert (n = l) by auto; subst.
        assert (m = l) by (apply antisymmetry; auto); subst.
        assumption.
      - intros Hl.
        destruct (Hyx l) as (m & Hm & Hlm); auto.
        destruct (Hxy m) as (n & Hn & Hmn); auto.
        assert (n = l) by auto; subst.
        assert (m = l) by (apply antisymmetry; auto); subst.
        assumption.
    Qed.

    (** ** Lattice structure *)

    Definition proj (x : opt L) : L :=
      sup {l | is x l}, l.

    Lemma proj_is x l :
      is x l -> proj x = l.
    Proof.
      intros Hl. apply antisymmetry.
      - apply fsup_lub. intros m Hm.
        assert (m = l) by eauto using is_unique. rauto.
      - eapply fsup_at; eauto. reflexivity.
    Qed.

    Definition sup_of {I} (x : I -> opt L) (l : L) :=
      (exists i, exists li, is (x i) li) /\
      sup i, proj (x i) = l.

    Definition inf_of {I} (x : I -> opt L) (l : L) :=
      (forall i, exists li, is (x i) li) /\
      inf i, proj (x i) = l.

    Definition sup_inf_of {I J} (x : forall i:I, J i -> opt L) (l : L) :=
      (exists i, forall j, exists li, is (x i j) li) /\
      sup i, inf j, proj (x i j) = l.

    Definition inf_sup_of {I J} (x : forall i:I, J i -> opt L) (l : L) :=
      (forall i, exists j, exists li, is (x i j) li) /\
      inf i, sup j, proj (x i j) = l.

    Lemma sup_inf_of_cd {I J} (x : forall i:I, J i -> opt L) (l : L) :
      sup_inf_of x l <->
      inf_sup_of (fun f i => x i (f i)) l.
    Proof.
      split.
      - intros [Hx Hl]. split.
        + firstorder.
        + subst. rewrite sup_inf. reflexivity.
      - intros [Hx Hl]. split.
        + destruct (classic (forall i, exists j, ~ exists li, is (x i j) li)).
          * exfalso.
            admit.
            (*
            apply choice in H as [f Hf].
            specialize (Hx f) as (i & li & Hli).
            apply (Hf i). eauto.
             *)
          * apply not_all_ex_not in H as (i & H). exists i. intro j.
            apply not_ex_not_all with _ _ j in H. auto.
        + subst. rewrite sup_inf. reflexivity.
    Admitted.

    Hint Unfold sup_of inf_of.

    Program Definition F : cdlattice :=
      {|
        cdl_poset := Fposet;
        lsup I x := mkopt (sup_of x) _;
        linf I x := mkopt (inf_of x) _;
      |}.

    (** [sup], [inf] are singletons. *)

    Next Obligation.
      firstorder congruence.
    Qed.
    Next Obligation.
      firstorder congruence.
    Qed.

    (** [sup] is the least upper bound *)

    Next Obligation.
      eexists; split; eauto.
      apply (sup_at i). cbn.
      erewrite proj_is by eauto. rauto.
    Qed.

    Next Obligation.
      destruct H0 as [(i & li & Hli) Hl]. subst. cbn.
      destruct (H i li Hli) as (m & Hm & _). clear i li Hli.
      exists m. split; auto.
      apply sup_lub. intros i.
      apply fsup_lub. intros li Hli.
      destruct (H i li Hli) as (m' & Hm' & LE).
      assert (m' = m) by eauto using is_unique. congruence.
    Qed.

    (** [inf] is the greatest lower bound *)

    Next Obligation.
      destruct H as [H Hl]. subst.
      destruct (H i) as (l & Hl).
      exists l; split; auto. cbn.
      apply (inf_at i). rewrite (proj_is (x i) l) by auto.
      reflexivity.
    Qed.

    Next Obligation.
      eexists; split.
      - split; [ | auto].
        intros i. destruct (H i l) as (m & Hm & Hlm); eauto.
      - apply inf_glb. intros i. cbn.
        edestruct (H i) as (m & Hm & Hlm); eauto.
        erewrite proj_is; eauto.
    Qed.

    (** Distributivity *)

    Next Obligation.
      apply opt_eq. intros l. cbn.
      transitivity (sup_inf_of x l).
      {
        unfold sup_of, inf_of, sup_inf_of, proj; cbn.
        split; intros [Hx Hl]; subst.
        - split.
          + firstorder.
          + apply antisymmetry.
            * apply sup_lub. intros i. apply (sup_at i).
              destruct (classic (forall j, exists lij, is (x i j) lij)).
              -- eapply fsup_at; eauto. reflexivity.
              -- apply not_all_ex_not in H as (j & Hj).
                 apply (inf_at j). apply fsup_lub. firstorder.
            * apply sup_lub. intros i. apply (sup_at i).
              apply fsup_lub. intros _ [H [ ]].
              reflexivity.
        - split.
          + destruct Hx as [i Hi]. eauto.
          + apply antisymmetry.
            * apply sup_lub. intros i. apply (sup_at i).
              apply fsup_lub. intros _ [Hi [ ]].
              reflexivity.
            * apply sup_lub. intros i. apply (sup_at i).
              destruct (classic (forall j, exists lij, is (x i j) lij)).
              -- eapply fsup_at; eauto. reflexivity.
              -- apply not_all_ex_not in H as (j & Hj).
                 apply (inf_at j). apply fsup_lub. firstorder.
      }
      rewrite sup_inf_of_cd.
      {
        unfold sup_of, inf_of, inf_sup_of, proj; cbn.
        split; intros [Hx Hl]; subst.
        - split.
          + intros f. destruct (Hx f) as (i & l & Hl). eauto.
          + f_equal. apply functional_extensionality. intros f.
            apply antisymmetry.
            * apply fsup_lub. intros _ [(i & l & Hl) [ ]]. reflexivity.
            * eapply fsup_at; eauto. reflexivity.
        - split.
          + intros f. destruct (Hx f) as (i & l & Hl). eauto.
          + f_equal. apply functional_extensionality. intros f.
            apply antisymmetry.
            * apply sup_lub. intros i. apply fsup_lub. intros l Hl.
              eapply fsup_at; eauto. eapply sup_at, fsup_at; eauto. reflexivity.
            * apply fsup_lub. intros _ [(i & l & Hl) [ ]]. reflexivity.
      }
    Qed.

    (** ** Adjunction *)

    Program Definition emb (l : L) : F := mkopt (eq l) _.

    Global Instance emb_mor :
      Lazy.Morphism emb.
    Proof.
      split.
      - red. intros I x [i]. apply antisymmetry.
        + intros l Hl. cbn in *. subst.
          eexists; split; [ | reflexivity]. red; cbn.
          split. exists i. eauto. unfold proj; cbn.
          apply antisymmetry.
          * apply sup_lub. intros j.
            apply fsup_lub. intros _ [ ].
            apply (sup_at j). reflexivity.
          * apply sup_lub. intros j. apply (sup_at j). cbn.
            eapply fsup_at; eauto. reflexivity.
        + apply sup_lub. cbn. intros j _ [ ].
          eexists; split; [reflexivity | ].
          apply sup_ub.
      - red. intros I x. apply antisymmetry.
        + cbn. intros _ [ ].
          eexists; split; [constructor; cbn; eauto | ].
          eapply inf_glb. intros i. apply (inf_at i).
          unfold proj; cbn. eapply fsup_at; eauto. reflexivity.
        + cbn. intros _ [? [ ]]. cbn in *.
          eexists; split; [reflexivity | ].
          eapply inf_glb. intros i. unfold proj; cbn.
          apply (inf_at i). apply fsup_lub. intros _ [ ]. reflexivity.
    Qed.

    (*
    Lemma emb_mor c1 c2 :
      emb c1 ⊑ emb c2 -> c1 ⊑ c2.
    Proof.
      unfold emb. cbn.
      split.
      - intros H. destruct (H c1) as (? & ? & ?); auto. congruence.
      - intros H l Hl. subst. eauto.
    Qed.
     *)

    Lemma cases x :
      x = bot \/ exists l, x = emb l.
    Proof.
      destruct (classic (ex (is x))) as [[l Hl] | H].
      - right. exists l.
        destruct x as [x Hx]; cbn in *.
        apply opt_eq. intros l'.
        cbn. split; auto. congruence.
      - left. apply antisymmetry.
        + intros l Hl. elim H; eauto.
        + apply bot_lb.
    Qed.

    Lemma sup_cases {I} (x : I -> F) :
      (lsup x = bot /\
       forall i, x i = bot) \/
      (lsup x = emb (sup {l | exists i, is (x i) l}, l) /\
       exists i l, is (x i) l).
    Proof.
      destruct (classic (forall i, x i = bot)).
      - left. split; auto.
        apply antisymmetry; auto using bot_lb.
        apply sup_lub. intros i.
        intros l Hl. rewrite H in Hl. elim Hl.
        intros ([ ] & _).
      - right. apply not_all_ex_not in H as (i & Hi).
        split.
        unfold fsup. rewrite (Lazy.mor_sup emb).
        + cbn. apply opt_eq. intros l. cbn. split.
          * intros [(j & m & Hm)].
            econstructor.
    Admitted.

    Definition ext (f : L -> M) (x : F) : M :=
      sup {l | is x l}, f l.

    Context {f : L -> M} `{Hf : !Lazy.Morphism f}.

    Lemma ext_bot :
      ext f bot = bot.
    Proof.
      apply antisymmetry; try apply bot_lb.
      unfold ext. apply fsup_lub. Local Transparent bot. cbn.
      intros i [? ?]. destruct H as [[ ]].
    Qed.

    Lemma ext_ana :
      (forall x, ext f (emb x) = f x).
    Proof.
      intros x. unfold ext, emb. cbn.
      apply antisymmetry.
      - apply fsup_lub. intros _ [ ]. reflexivity.
      - apply fsup_ub. reflexivity.
    Qed.

    Instance ext_mor :
      CDL.Morphism (ext f).
    Proof.
      split.
      - red. intros I x.
        destruct (sup_cases x) as [[Hsup H] | [Hsup H]]; rewrite Hsup.
        + rewrite ext_bot. transitivity (sup i:I, ext f bot).
          * apply antisymmetry; try apply bot_lb.
            apply sup_lub. intros _. rewrite ext_bot. reflexivity.
          * f_equal. apply functional_extensionality. intro. rewrite H. reflexivity.
        + rewrite ext_ana. unfold fsup. rewrite (Lazy.mor_sup f).
          * apply antisymmetry.
            -- apply sup_lub. intros (l & i & Hli). cbn.
               apply (sup_at i). eapply fsup_at; eauto. reflexivity.
            -- apply sup_lub. intros i. apply fsup_lub. intros l Hli. cbn.
               admit.
          * admit.
      - admit.
    Admitted.

    Lemma ext_unique (g : F -> M) `{Hg : !CDL.Morphism g} :
      (forall x, g (emb x) = f x) -> forall x, g x = ext f x.
    Proof.
      intros Hgf l. destruct (cases l) as [? | [y Hy]]; subst.
      - rewrite (Downset.Sup.mor_bot (f := g)).
        rewrite (Downset.Sup.mor_bot (f := ext f)).
        reflexivity.
      - rewrite ext_ana. auto.
    Qed.

  End DEF.

End LBot.

author: CertiKOS

repo: rbgs

save_path: github-repos/coq/CertiKOS-rbgs


text:
From Coq Require Import Arith Div2 Omega Lia Nat.

Fixpoint div_mod2 (n : nat) : (nat * bool) :=
  match n with
  | 0 => (0, false)
  | 1 => (0, true)
  | S (S n) => let (a, b) := div_mod2 n in (S a, b)
  end.

Fixpoint pow_sqr_aux (k b e : nat) : nat :=
  match k, e with
  | 0, _ => 1
  | _, 0 => 1
  | S k, _ => match div_mod2 e with
              | (e', false) => pow_sqr_aux k (b * b) e'
              | (e', true) => b * pow_sqr_aux k (b * b) e'
              end
  end.

Definition pow_sqr (b e : nat) : nat := pow_sqr_aux e b e.

Lemma silly:
  forall n, div_mod2 n = (div2 n, odd n).
Proof.
  induction n using (well_founded_induction lt_wf).
  destruct n; simpl; auto.
  destruct n; simpl; auto.
  rewrite H; auto.
Qed.

Lemma pow_eq_extended:
  forall k b e,
    (k >= e) ->
    pow_sqr_aux k b e = b ^ e.
Proof.
  induction k;intros;simpl. inversion H;subst. auto.
  rewrite silly. destruct e; auto.
  generalize (lt_div2 (S e) ltac:(lia)). intros.
  assert (div2 (S e) <= k). omega. rewrite IHk.
  destruct (odd (S e)) eqn:He;
 try (rewrite (Nat.div2_odd (S e)) at 2; rewrite He;
    rewrite Nat.pow_add_r; rewrite Nat.pow_mul_r; rewrite Nat.pow_2_r;
    simpl;lia). auto.
Qed.

Theorem pow_eq (b e : nat) : pow_sqr b e = b ^ e.
Proof. apply pow_eq_extended. auto. Qed.

author: Brethland

repo: LEARNING-STUFF


text:
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

Require Export OrderedType.
Require Export OrderedTypeEx.
Require Export OrderedTypeAlt.
Require Export DecidableType.
Require Export DecidableTypeEx.
Require Export FSetInterface.
Require Export FSetBridge.
Require Export FSetFacts.
Require Export FSetDecide.
Require Export FSetProperties.
Require Export FSetEqProperties.
Require Export FSetWeakList.
Require Export FSetList.
Require Export FSetPositive.
Require Export FSetAVL.

repo: Coq-misc


text:
From iris.algebra Require Export ofe.
From iris.prelude Require Import options.

Section language_mixin.
  (** [state] is per-machine state; [global_state] is state shared across machines. *)
  Context {expr val state global_state observation : Type}.
  Context (of_val : val → expr).
  Context (to_val : expr → option val).
  (** We annotate the reduction relation with observations [κ], which we will
     use in the definition of weakest preconditions to predict future
     observations and assert correctness of the predictions. *)
  Context (prim_step : expr → state → global_state → list observation → expr → state → global_state → list expr → Prop).

  Record LanguageMixin := {
    mixin_to_of_val v : to_val (of_val v) = Some v;
    mixin_of_to_val e v : to_val e = Some v → of_val v = e;
    mixin_val_stuck e g σ κ e' g' σ' efs : prim_step e σ g κ e' σ' g' efs → to_val e = None
  }.
End language_mixin.

Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
  global_state : Type;
  observation : Type;
  of_val : val → expr;
  to_val : expr → option val;
  prim_step : expr → state → global_state → list observation → expr → state → global_state → list expr → Prop;
  language_mixin : LanguageMixin of_val to_val prim_step
}.

Declare Scope expr_scope.
Delimit Scope expr_scope with E.
Bind Scope expr_scope with expr.

Declare Scope val_scope.
Delimit Scope val_scope with V.
Bind Scope val_scope with val.

Global Arguments Language {_ _ _ _ _ _ _ _} _.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments prim_step {_} _ _ _ _ _ _.

Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure global_stateO Λ := leibnizO (global_state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
Canonical Structure exprO Λ := leibnizO (expr Λ).

(** This is the system configuration for a *one-machine execution. *)
Definition cfg (Λ : language) := (list (expr Λ) * (state Λ * global_state Λ))%type.

Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
  fill_not_val e :
    to_val e = None → to_val (K e) = None;
  fill_val_inv v v' :
    is_Some (to_val (K (of_val v))) → is_Some (to_val (K (of_val v')));
  fill_step e1 σ1 g1 κ e2 σ2 g2 efs :
    prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
    prim_step (K e1) σ1 g1 κ (K e2) σ2 g2 efs;
  fill_step_inv e1' σ1 g1 κ e2 σ2 g2 efs :
    to_val e1' = None → prim_step (K e1') σ1 g1 κ e2 σ2 g2 efs →
    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 g1 κ e2' σ2 g2 efs
}.

Inductive atomicity := StronglyAtomic | WeaklyAtomic.

Section language.
  Context {Λ : language}.
  Implicit Types v : val Λ.
  Implicit Types e : expr Λ.

  Lemma to_of_val v : to_val (of_val v) = Some v.
  Proof. apply language_mixin. Qed.
  Lemma of_to_val e v : to_val e = Some v → of_val v = e.
  Proof. apply language_mixin. Qed.
  Lemma val_stuck e σ g κ e' σ' g' efs : prim_step e σ g κ e' σ' g' efs → to_val e = None.
  Proof. apply language_mixin. Qed.

  Global Instance language_ctx_id : LanguageCtx (@id (expr Λ)).
  Proof.
    constructor; try naive_solver.
    intros ?? Hval. rewrite to_of_val //=; eauto.
  Qed.

  Definition reducible (e : expr Λ) (σ : state Λ) (g : global_state Λ) :=
    ∃ κ e' σ' g' efs, prim_step e σ g κ e' σ' g' efs.
  (* Total WP only permits reductions without observations *)
  Definition reducible_no_obs (e : expr Λ) (σ : state Λ) (g : global_state Λ) :=
    ∃ e' σ' g' efs, prim_step e σ g [] e' σ' g' efs.
  Definition irreducible (e : expr Λ) (σ : state Λ) (g : global_state Λ) :=
    ∀ κ e' σ' g' efs, ¬prim_step e σ g κ e' σ' g' efs.
  Definition stuck (e : expr Λ) (σ : state Λ) (g : global_state Λ) :=
    to_val e = None ∧ irreducible e σ g.
  Definition not_stuck (e : expr Λ) (σ : state Λ) (g : global_state Λ) :=
    is_Some (to_val e) ∨ reducible e σ g.

  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
     invariants when WP ensures safety, i.e., programs never can get stuck.  We
     have an example in lambdaRust of an expression that is atomic in this
     sense, but not in the stronger sense defined below, and we have to be able
     to open invariants around that expression.  See `CasStuckS` in
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).

     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
     safety, we need a stronger form of atomicity.  With the above definition,
     in case `e` reduces to a stuck non-value, there is no proof that the
     invariants have been established again. *)
  Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
    atomic σ g e' κ σ' g' efs :
      prim_step e σ g κ e' σ' g' efs →
      if a is WeaklyAtomic then irreducible e' σ' g' else is_Some (to_val e').

  Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
    | step_atomic e1 σ1 g1 e2 σ2 g2 efs t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, (σ1, g1)) →
       ρ2 = (t1 ++ e2 :: t2 ++ efs, (σ2, g2)) →
       prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
       step ρ1 κ ρ2.
  Local Hint Constructors step : core.

  Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
    | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
    | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 →
       nsteps n ρ2 κs ρ3 →
       nsteps (S n) ρ1 (κ ++ κs) ρ3.
  Local Hint Constructors nsteps : core.

  Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.

  (** [rtc erased_step] and [nsteps] encode the same thing, just packaged
      in a different way. *)
  Lemma erased_steps_nsteps ρ1 ρ2 :
    rtc erased_step ρ1 ρ2 ↔ ∃ n κs, nsteps n ρ1 κs ρ2.
  Proof.
    split.
    - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
    - intros (n & κs & Hsteps). unfold erased_step.
      induction Hsteps; eauto using rtc_refl, rtc_l.
  Qed.

  Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.

  Lemma not_reducible e σ g : ¬reducible e σ g ↔ irreducible e σ g.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
  Lemma reducible_not_val e σ f : reducible e σ f → to_val e = None.
  Proof. intros (?&?&?&?&?&?); eauto using val_stuck. Qed.
  Lemma reducible_no_obs_reducible e σ g : reducible_no_obs e σ g → reducible e σ g.
  Proof. intros (?&?&?&?&?); eexists; eauto. Qed.
  Lemma val_irreducible e σ g : is_Some (to_val e) → irreducible e σ g.
  Proof. intros [??] ????? ?%val_stuck. by destruct (to_val e). Qed.
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
  Lemma not_not_stuck e σ g : ¬not_stuck e σ g ↔ stuck e σ g.
  Proof.
    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
    destruct (decide (to_val e = None)); naive_solver.
  Qed.

  Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e → Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.

  Lemma reducible_fill `{!@LanguageCtx Λ K} e σ g :
    reducible e σ g → reducible (K e) σ g.
  Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.
  Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ g :
    to_val e = None → reducible (K e) σ g → reducible e σ g.
  Proof.
    intros ? (e'&σ'&g'&k&efs&Hstep); unfold reducible.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto 10.
  Qed.
  Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ g :
    reducible_no_obs e σ g → reducible_no_obs (K e) σ g.
  Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.
  Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ g :
    to_val e = None → reducible_no_obs (K e) σ g → reducible_no_obs e σ g.
  Proof.
    intros ? (e'&σ'&g'&efs&Hstep); unfold reducible_no_obs.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto 10.
  Qed.
  Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ g :
    to_val e = None → irreducible e σ g → irreducible (K e) σ g.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.
  Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ g :
    irreducible (K e) σ g → irreducible e σ g.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.

  Lemma not_stuck_fill_inv K `{!@LanguageCtx Λ K} e σ g :
    not_stuck (K e) σ g → not_stuck e σ g.
  Proof.
    rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
    - auto using fill_not_val.
    - destruct (decide (to_val e = None)); eauto using reducible_fill_inv.
  Qed.

  Lemma stuck_fill `{!@LanguageCtx Λ K} e σ g :
    stuck e σ g → stuck (K e) σ g.
  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed.

  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σg1 σg2 :
    t1 ≡ₚ t1' → step (t1,σg1) κ (t2,σg2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σg1) κ (t2',σg2).
  Proof.
    intros Ht [e1 σ1' g1' e2 σ2' g2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.

  Lemma step_insert i t2 σ2 g2 e κ e' σ3 g3 efs :
    t2 !! i = Some e →
    prim_step e σ2 g2 κ e' σ3 g3 efs →
    step (t2, (σ2, g2)) κ (<[i:=e']>t2 ++ efs, (σ3, g3)).
  Proof.
    intros.
    edestruct (elem_of_list_split_length t2) as (t21&t22&?&?);
      first (by eauto using elem_of_list_lookup_2); simplify_eq.
    econstructor; eauto.
    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
  Qed.

  Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2).
  Proof.
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
     (* FIXME: [naive_solver] should be able to handle this *)
  Qed.

  Record pure_step (e1 e2 : expr Λ) := {
    pure_step_safe σ1 g1 : reducible_no_obs e1 σ1 g1;
    pure_step_det σ1 g1 κ e2' σ2 g2 efs :
      prim_step e1 σ1 g1 κ e2' σ2 g2 efs → κ = [] ∧ σ2 = σ1 ∧ g2 = g1 ∧ e2' = e2 ∧ efs = []
  }.

  Notation pure_steps_tp := (Forall2 (rtc pure_step)).

  (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
  succeeding when it did not actually do anything. *)
  Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
    pure_exec : φ → relations.nsteps pure_step n e1 e2.

  Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    pure_step e1 e2 →
    pure_step (K e1) (K e2).
  Proof.
    intros [Hred Hstep]. split.
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
    - intros σ1 g1 κ e2' σ2 g2 efs Hpstep.
      destruct (fill_step_inv e1 σ1 g1 κ e2' σ2 g2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
      + destruct (Hred σ1 g1) as (? & ? & ? & ? & ?); eauto using val_stuck.
      + edestruct (Hstep σ1 g1 κ e2'' σ2 g2 efs) as (? & -> & -> & -> & ->); auto.
  Qed.

  Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
    relations.nsteps pure_step n e1 e2 →
    relations.nsteps pure_step n (K e1) (K e2).
  Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.

  Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2).
  Proof. eauto using rtc_congruence, pure_step_ctx. Qed.

  (* We do not make this an instance because it is awfully general. *)
  Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
    PureExec φ n e1 e2 →
    PureExec φ n (K e1) (K e2).
  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.

  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
    into_val : of_val v = e.

  Class AsVal (e : expr Λ) := as_val : ∃ v, of_val v = e.
  (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
  efficiently since no witness has to be computed. *)
  Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
  Proof.
    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
    rewrite /AsVal /=; eauto.
  Qed.

  Lemma as_val_is_Some e :
    (∃ v, of_val v = e) → is_Some (to_val e).
  Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.

  Lemma prim_step_not_stuck e σ g κ e' σ' g' efs :
    prim_step e σ g κ e' σ' g' efs → not_stuck e σ g.
  Proof. rewrite /not_stuck /reducible. eauto 10. Qed.

  Lemma rtc_pure_step_val `{!Inhabited (state Λ)} `{!Inhabited (global_state Λ)} v e :
    rtc pure_step (of_val v) e → to_val e = Some v.
  Proof.
    intros ?; rewrite <- to_of_val.
    f_equal; symmetry; eapply rtc_nf; first done.
    intros [e' [Hstep _]].
    destruct (Hstep inhabitant inhabitant) as (?&?&?&?&Hval%val_stuck).
    by rewrite to_of_val in Hval.
  Qed.

  (** Let thread pools [t1] and [t3] be such that each thread in [t1] makes
   (zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
   let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
   step to thread pool [t2] and state [σ2]. In this situation, either the step
   from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
   or, there is an [i] such that [i]th thread does not participate in the
   pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
   the [i]th thread starting from [t1]. *)
  Lemma erased_step_pure_step_tp t1 σ1 g1 t2 σ2 g2 t3 :
    erased_step (t1, (σ1, g1)) (t2, (σ2, g2)) →
    pure_steps_tp t1 t3 →
    (σ1 = σ2 ∧ pure_steps_tp t2 t3) ∨
    (∃ i e efs e' κ,
      t1 !! i = Some e ∧ t3 !! i = Some e ∧
      t2 = <[i:=e']>t1 ++ efs ∧
      prim_step e σ1 g1 κ e' σ2 g2 efs).
  Proof.
    intros [κ [e σ g e' σ' g' efs t11 t12 ?? Hstep]] Hps; simplify_eq/=.
    apply Forall2_app_inv_l in Hps
      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
    - right.
      exists (length t11), e, efs, e', κ; split_and!; last done.
      + by rewrite lookup_app_r // Nat.sub_diag.
      + apply Forall2_length in Hpsteps.
        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
    - edestruct Hprs as (?&?&?&?&?); first done; simplify_eq.
      left; split; first done.
      rewrite right_id_L.
      eauto using Forall2_app.
  Qed.

End language.

Global Arguments step_atomic {Λ ρ1 κ ρ2}.

Notation pure_steps_tp := (Forall2 (rtc pure_step)).

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import PartSum.
Local Open Scope R_scope.

Definition C (n p:nat) : R :=
  INR (fact n) / (INR (fact p) * INR (fact (n - p))).

Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i).
Proof.
  intros; unfold C; replace (n - (n - i))%nat with i.
  rewrite Rmult_comm.
  reflexivity.
  apply plus_minus; rewrite plus_comm; apply le_plus_minus; assumption.
Qed.

Lemma pascal_step2 :
  forall n i:nat,
    (i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n i.
Proof.
  intros; unfold C; replace (S n - i)%nat with (S (n - i)).
  cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
  intro; repeat rewrite H0.
  unfold Rdiv; repeat rewrite mult_INR; repeat rewrite Rinv_mult_distr.
  ring.
  apply INR_fact_neq_0.
  apply INR_fact_neq_0.
  apply not_O_INR; discriminate.
  apply INR_fact_neq_0.
  apply INR_fact_neq_0.
  apply prod_neq_R0.
  apply not_O_INR; discriminate.
  apply INR_fact_neq_0.
  intro; reflexivity.
  apply minus_Sn_m; assumption.
Qed.

Lemma pascal_step3 :
  forall n i:nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n i.
Proof.
  intros; unfold C.
  cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
  intro.
  cut ((n - i)%nat = S (n - S i)).
  intro.
  pattern (n - i)%nat at 2; rewrite H1.
  repeat rewrite H0; unfold Rdiv; repeat rewrite mult_INR;
    repeat rewrite Rinv_mult_distr.
  rewrite <- H1; rewrite (Rmult_comm (/ INR (n - i)));
    repeat rewrite Rmult_assoc; rewrite (Rmult_comm (INR (n - i)));
      repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
  ring.
  apply not_O_INR; apply minus_neq_O; assumption.
  apply not_O_INR; discriminate.
  apply INR_fact_neq_0.
  apply INR_fact_neq_0.
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
  apply not_O_INR; discriminate.
  apply INR_fact_neq_0.
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
  apply INR_fact_neq_0.
  rewrite minus_Sn_m.
  simpl; reflexivity.
  apply lt_le_S; assumption.
  intro; reflexivity.
Qed.

  (**********)
Lemma pascal :
  forall n i:nat, (i < n)%nat -> C n i + C n (S i) = C (S n) (S i).
Proof.
  intros.
  rewrite pascal_step3; [ idtac | assumption ].
  replace (C n i + INR (n - i) / INR (S i) * C n i) with
    (C n i * (1 + INR (n - i) / INR (S i))); [ idtac | ring ].
  replace (1 + INR (n - i) / INR (S i)) with (INR (S n) / INR (S i)).
  rewrite pascal_step1.
  rewrite Rmult_comm; replace (S i) with (S n - (n - i))%nat.
  rewrite <- pascal_step2.
  apply pascal_step1.
  apply le_trans with n.
  apply le_minusni_n.
  apply lt_le_weak; assumption.
  apply le_n_Sn.
  apply le_minusni_n.
  apply lt_le_weak; assumption.
  rewrite <- minus_Sn_m.
  cut ((n - (n - i))%nat = i).
  intro; rewrite H0; reflexivity.
  symmetry ; apply plus_minus.
  rewrite plus_comm; rewrite le_plus_minus_r.
  reflexivity.
  apply lt_le_weak; assumption.
  apply le_minusni_n; apply lt_le_weak; assumption.
  apply lt_le_weak; assumption.
  unfold Rdiv.
  repeat rewrite S_INR.
  rewrite minus_INR.
  cut (INR i + 1 <> 0).
  intro.
  apply Rmult_eq_reg_l with (INR i + 1); [ idtac | assumption ].
  rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  do 2 rewrite (Rmult_comm (INR i + 1)).
  repeat rewrite Rmult_assoc.
  rewrite <- Rinv_l_sym; [ idtac | assumption ].
  ring.
  rewrite <- S_INR.
  apply not_O_INR; discriminate.
  apply lt_le_weak; assumption.
Qed.

  (*********************)
  (*********************)
Lemma binomial :
  forall (x y:R) (n:nat),
    (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.
Proof.
  intros; induction  n as [| n Hrecn].
  unfold C; simpl; unfold Rdiv;
    repeat rewrite Rmult_1_r; rewrite Rinv_1; ring.
  pattern (S n) at 1; replace (S n) with (n + 1)%nat; [ idtac | ring ].
  rewrite pow_add; rewrite Hrecn.
  replace ((x + y) ^ 1) with (x + y); [ idtac | simpl; ring ].
  rewrite tech5.
  cut (forall p:nat, C p p = 1).
  cut (forall p:nat, C p 0 = 1).
  intros; rewrite H0; rewrite <- minus_n_n; rewrite Rmult_1_l.
  replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl; reflexivity ].
  induction  n as [| n Hrecn0].
  simpl; do 2 rewrite H; ring.
  (* N >= 1 *)
  set (N := S n).
  rewrite Rmult_plus_distr_l.
  replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * x) with
    (sum_f_R0 (fun i:nat => C N i * x ^ S i * y ^ (N - i)) N).
  replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * y) with
    (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (S N - i)) N).
  rewrite (decomp_sum (fun i:nat => C (S N) i * x ^ i * y ^ (S N - i)) N).
  rewrite H; replace (x ^ 0) with 1; [ idtac | reflexivity ].
  do 2 rewrite Rmult_1_l.
  replace (S N - 0)%nat with (S N); [ idtac | reflexivity ].
  set (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)).
  set (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)).
  replace (pred N) with n.
  replace (sum_f_R0 (fun i:nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n)
    with (sum_f_R0 (fun i:nat => An i + Bn i) n).
  rewrite plus_sum.
  replace (x ^ S N) with (An (S n)).
  rewrite (Rplus_comm (sum_f_R0 An n)).
  repeat rewrite Rplus_assoc.
  rewrite <- tech5.
  fold N.
  set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)).
  cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i).
  intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n).
  replace (y ^ S N) with (Cn 0%nat).
  rewrite <- Rplus_assoc; rewrite (decomp_sum Cn N).
  replace (pred N) with n.
  ring.
  unfold N; simpl; reflexivity.
  unfold N; apply lt_O_Sn.
  unfold Cn; rewrite H; simpl; ring.
  apply sum_eq.
  intros; apply H1.
  unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ].
  reflexivity.
  unfold An; fold N; rewrite <- minus_n_n; rewrite H0;
    simpl; ring.
  apply sum_eq.
  intros; unfold An, Bn.
  change (S N - S i)%nat with (N - i)%nat.
  rewrite <- pascal;
    [ ring
      | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ].
  unfold N; reflexivity.
  unfold N; apply lt_O_Sn.
  rewrite <- (Rmult_comm y); rewrite scal_sum; apply sum_eq.
  intros; replace (S N - i)%nat with (S (N - i)).
  replace (S (N - i)) with (N - i + 1)%nat; [ idtac | ring ].
  rewrite pow_add; replace (y ^ 1) with y; [ idtac | simpl; ring ];
    ring.
  apply minus_Sn_m; assumption.
  rewrite <- (Rmult_comm x); rewrite scal_sum; apply sum_eq.
  intros; replace (S i) with (i + 1)%nat; [ idtac | ring ]; rewrite pow_add;
    replace (x ^ 1) with x; [ idtac | simpl; ring ];
      ring.
  intro; unfold C.
  replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
  replace (p - 0)%nat with p; [ idtac | apply minus_n_O ].
  rewrite Rmult_1_l; unfold Rdiv; rewrite <- Rinv_r_sym;
    [ reflexivity | apply INR_fact_neq_0 ].
  intro; unfold C.
  replace (p - p)%nat with 0%nat; [ idtac | apply minus_n_n ].
  replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
  rewrite Rmult_1_r; unfold Rdiv; rewrite <- Rinv_r_sym;
    [ reflexivity | apply INR_fact_neq_0 ].
Qed.

author: Priyanka-Mondal

repo: Coq

save_path: github-repos/coq/Priyanka-Mondal-Coq


text:
Require Import preds_in List Lia.

(* Takes in a list of predicates and returns a list of reverse indicies at which Q occurs in l. *)
Fixpoint indicies_l_rev (l : list predicate) (Q : predicate) : list nat :=
  match l with
  | nil => nil
  | cons P l' => if predicate_dec P Q then cons (length l) (indicies_l_rev l' Q)
                                      else indicies_l_rev l' Q
  end.

Lemma indicies_l_rev_cons : forall (l : list predicate) (P Q : predicate),
  indicies_l_rev (cons P l) Q
  = if predicate_dec P Q then cons (length (cons P l)) (indicies_l_rev l Q)
                                      else indicies_l_rev l Q.
Proof. auto. Qed.

Lemma indicies_l_rev_app : forall (l1 l2 : list predicate) (Q : predicate),
    indicies_l_rev (app l1 l2) Q
  = app (map (fun n:nat => length l2 + n) (indicies_l_rev l1 Q))
                   (indicies_l_rev l2 Q).
Proof.
  induction l1; intros l2 Q. auto.
  simpl. destruct (predicate_dec a Q). subst. simpl. rewrite IHl1.
  rewrite app_length. rewrite PeanoNat.Nat.add_comm.
  rewrite PeanoNat.Nat.add_succ_r.  auto.
  apply IHl1.
Qed.

(* -------------------------------------------------------------------------- *)

(* Takes in a list of predicates and returns a list of indicies at which Q occurs in l. *)
Definition indicies (alpha :SecOrder) (Q : predicate) : list nat :=
  map (fun n:nat => length (preds_in alpha) + 1 - n)
           (indicies_l_rev (preds_in alpha) Q).

Lemma indicies_conjSO : forall (alpha1 alpha2 : SecOrder) (P : predicate),
  indicies (conjSO alpha1 alpha2) P
  = app (map (fun n:nat => length (preds_in alpha1) + 1 - n)
                (indicies_l_rev (preds_in alpha1) P))
        (map (fun n:nat => length (preds_in alpha1 ++ preds_in alpha2) + 1 - n)
                (indicies_l_rev (preds_in alpha2) P)).
Proof.
  intros. unfold indicies. simpl.
  rewrite indicies_l_rev_app.
  rewrite map_app. rewrite map_map.
  rewrite app_length.
  assert (forall a b l,
             map (fun x : nat => a + b + 1 - (b + x)) l =
             map (fun x : nat => a + 1 - x) l) as Hass.
  intros. apply map_ext. intros. lia. rewrite Hass. auto.
Qed.

Lemma indicies_disjSO : forall (alpha1 alpha2 : SecOrder) (P : predicate),
  indicies (disjSO alpha1 alpha2) P
  = app (map (fun n:nat => length (preds_in alpha1) + 1 - n)
                (indicies_l_rev (preds_in alpha1) P))
        (map (fun n:nat => length (preds_in alpha1 ++ preds_in alpha2) + 1 - n)
                (indicies_l_rev (preds_in alpha2) P)).
Proof.
  intros. unfold indicies. simpl.
  rewrite indicies_l_rev_app.
  rewrite map_app. rewrite map_map.
  rewrite app_length.
  assert (forall a b l,
             map (fun x : nat => a + b + 1 - (b + x)) l =
             map (fun x : nat => a + 1 - x) l) as Hass.
  intros. apply map_ext. firstorder. rewrite Hass. auto.
Qed.

Lemma le_indicies_l_rev : forall (l : list predicate) (P : predicate),
  (length (indicies_l_rev l P)) <= (length l).
Proof.
  induction l; intros P. firstorder.
  simpl. destruct (predicate_dec a P); simpl; firstorder.
Qed.

Lemma length_ind : forall (alpha : SecOrder) (P : predicate),
  length (indicies (alpha) P) = length (indicies_l_rev (preds_in alpha) P).
Proof.
  intros; unfold indicies.
  rewrite map_length. auto.
Qed.

Lemma indicies_l_rev_not_in : forall l P,
~ In P l ->  length (indicies_l_rev l P) = 0.
Proof.
  induction l; intros P H. auto.
  simpl. rewrite predicate_dec_r. 2 : firstorder.
  apply IHl; firstorder.
Qed.

author: caitlindabrera

repo: Sahlqvist


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.montgomery32_2e254m127x2e240m1_8limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition sub :
  { sub : feBW_small -> feBW_small -> feBW_small
  | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_sub ().
  Show Ltac Profile.
Time Defined.

Print Assumptions sub.


text:
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import TableWalk.Spec.
Require Import AbsAccessor.Spec.
Require Import TableAux2.Spec.
Require Import TableAux.Specs.granule_fill_table.

Local Open Scope Z_scope.

Section Spec.

  Definition create_table (llt_gidx: Z) (idx: Z) (rtt_addr: Z) (rtt_gidx: Z) (rd_gidx: Z) (level: Z) (map_addr: Z) (adt: RData) :=
    let gn_llt := (gs (share adt)) @ llt_gidx in
    let gn_rtt := (gs (share adt)) @ rtt_gidx in
    rely (g_tag (ginfo gn_llt) =? GRANULE_STATE_TABLE);
    rely (gtype gn_llt =? GRANULE_STATE_TABLE);
    rely (gtype gn_rtt =? GRANULE_STATE_DELEGATED);
    rely prop_dec (glock gn_rtt = Some CPU_ID);
    rely (tbl_level (gaux gn_rtt) =? 0);
    let llt_pte := (g_data (gnorm gn_llt)) @ idx in
    rely is_int64 llt_pte;
    if __entry_is_table llt_pte then
      Some (adt {log: EVT CPU_ID (REL llt_gidx gn_llt {glock: Some CPU_ID}) :: log adt}, VZ64 1)
    else
      let ipa_state := PTE_TO_IPA_STATE llt_pte in
      if (ipa_state =? IPA_STATE_VACANT) || (ipa_state =? IPA_STATE_DESTROYED) then
        let pte_val := IPA_STATE_TO_PTE ipa_state in
        match fill_table (Z.to_nat PGTES_PER_TABLE) (g_data (gnorm gn_rtt)) 0 pte_val 0 with
        | (tbl', _, _) =>
          let llt' := (g_data (gnorm gn_llt)) # idx == (Z.lor rtt_addr PGTE_S2_TABLE) in
          let grtt' := gn_rtt {ginfo: (ginfo gn_rtt) {g_tag: GRANULE_STATE_TABLE} {g_rd: rd_gidx} {g_refcount: (g_refcount (ginfo (gn_rtt))) + 1}}
                              {gnorm : (gnorm gn_rtt) {g_data : tbl'}} {gaux: mkAuxillaryVars level idx llt_gidx} in
          let gllt' := gn_llt {ginfo : (ginfo gn_llt) {g_refcount : g_refcount (ginfo gn_llt) + 1}}
                             {gnorm: (gnorm gn_llt) {g_data: llt'}} in
          Some (adt {log: EVT CPU_ID (REL llt_gidx gllt' {glock: Some CPU_ID}) :: log adt}
                    {share : (share adt) {gs : ((gs (share adt)) # rtt_gidx == grtt') # llt_gidx == gllt'}},
                VZ64 0)
        end
      else
        if ipa_state =? IPA_STATE_ABSENT then
          rely (level =? RTT_PAGE_LEVEL);
          let pa := __entry_to_phys llt_pte 2 in
          let pte_val := Z.lor (IPA_STATE_TO_PTE IPA_STATE_ABSENT) pa in
          match fill_table (Z.to_nat PGTES_PER_TABLE) (g_data (gnorm gn_rtt)) 0 pte_val GRANULE_SIZE with
          | (tbl', _, _) =>
            let llt' := (g_data (gnorm gn_llt)) # idx == (Z.lor rtt_addr PGTE_S2_TABLE) in
            let grtt' := gn_rtt {ginfo: (ginfo gn_rtt) {g_tag: GRANULE_STATE_TABLE} {g_rd: rd_gidx}
                                                       {g_refcount: (g_refcount (ginfo (gn_rtt))) + PGTES_PER_TABLE + 1}}
                                {gnorm : (gnorm gn_rtt) {g_data : tbl'}} {gaux: mkAuxillaryVars level idx llt_gidx} in
            let gllt' := gn_llt {gnorm: (gnorm gn_llt) {g_data: llt'}} in
            Some (adt {log: EVT CPU_ID (REL llt_gidx gllt' {glock: Some CPU_ID}) :: log adt}
                      {share : (share adt) {gs : ((gs (share adt)) # rtt_gidx == grtt') # llt_gidx == gllt'}},
                  VZ64 0)
          end
        else if ipa_state =? IPA_STATE_PRESENT then
               rely (level =? RTT_PAGE_LEVEL);
               let pa := __entry_to_phys llt_pte 2 in
               let pte_val := Z.lor (Z.lor (IPA_STATE_TO_PTE IPA_STATE_PRESENT) pa) PGTE_S2_PAGE in
               match fill_table (Z.to_nat PGTES_PER_TABLE) (g_data (gnorm gn_rtt)) 0 pte_val GRANULE_SIZE with
               | (tbl', _, _) =>
                 let llt' := (g_data (gnorm gn_llt)) # idx == (Z.lor rtt_addr PGTE_S2_TABLE) in
                 let grtt' := gn_rtt {ginfo: (ginfo gn_rtt) {g_tag: GRANULE_STATE_TABLE} {g_rd: rd_gidx}
                                                             {g_refcount: (g_refcount (ginfo (gn_rtt))) + PGTES_PER_TABLE + 1}}
                                     {gnorm : (gnorm gn_rtt) {g_data : tbl'}} {gaux: mkAuxillaryVars level idx llt_gidx} in
                 let gllt' := gn_llt {gnorm: (gnorm gn_llt) {g_data: llt'}} in
                 let ipa_gidx := __addr_to_gidx map_addr in
                 let tlbs' := fun cpu gidx => if gidx =? ipa_gidx then -1 else tlbs (share adt) cpu gidx in
                 Some (adt {log: EVT CPU_ID (REL llt_gidx gllt' {glock: Some CPU_ID}) :: log adt}
                           {share : (share adt) {gs : ((gs (share adt)) # rtt_gidx == grtt') # llt_gidx == gllt'} {tlbs: tlbs'}},
                       VZ64 0)
               end
             else None.

  Definition table_create_spec (g_rd: Pointer) (map_addr: Z64) (level: Z64) (g_rtt': Pointer) (rtt_addr: Z64) (adt: RData) : option (RData * Z64) :=
    match map_addr, level, rtt_addr with
    | VZ64 map_addr, VZ64 level, VZ64 rtt_addr =>
      rely is_int64 map_addr; rely is_int64 rtt_addr; rely GRANULE_ALIGNED map_addr;
      let idx0 := __addr_to_idx map_addr 0 in
      let idx1 := __addr_to_idx map_addr 1 in
      let idx2 := __addr_to_idx map_addr 2 in
      let idx3 := __addr_to_idx map_addr 3 in
      let ret_idx := (if level =? 1 then idx0 else if level =? 2 then idx1 else if level =? 3 then idx2 else idx3) in
      let rtt_gidx := __addr_to_gidx rtt_addr in
      rely is_gidx rtt_gidx;
      rely (peq (base g_rd) ginfo_loc);
      rely (peq (base g_rtt') ginfo_loc);
      rely (offset g_rtt' =? rtt_gidx);
      rely prop_dec ((buffer (priv adt)) @ SLOT_RD = None);
      rely prop_dec ((buffer (priv adt)) @ SLOT_TABLE = None);
      rely prop_dec ((buffer (priv adt)) @ SLOT_DELEGATED = None);
      let rd_gidx := (offset g_rd) in
      let grd := (gs (share adt)) @ rd_gidx in
      rely (g_tag (ginfo grd) =? GRANULE_STATE_RD);
      rely prop_dec (glock grd = Some CPU_ID);
      let root_gidx := (g_rtt (gnorm grd)) in
      rely is_gidx rd_gidx; rely is_gidx root_gidx;
      when adt == query_oracle adt;
      (* hold root lock *)
      let adt := adt {log: EVT CPU_ID (ACQ root_gidx) :: log adt} in
      let groot := (gs (share adt)) @ root_gidx in
      rely (tbl_level (gaux groot) =? 0);
      rely prop_dec (glock groot = None);
      if level =? 1 then
        (* walk until root *)
        let adt :=  adt {priv: (priv adt) {wi_llt: root_gidx} {wi_index: idx0}} in
        create_table root_gidx idx0 rtt_addr rtt_gidx rd_gidx 1 map_addr adt
      else
        (* walk deeper root *)
        rely (level >? 1);
        rely (g_tag (ginfo groot) =? GRANULE_STATE_TABLE);
        rely (gtype groot =? GRANULE_STATE_TABLE);
        let entry0 := (g_data (gnorm groot)) @ idx0 in
          rely is_int64 entry0;
          let phys0 := __entry_to_phys entry0 3 in
          let lv1_gidx := __addr_to_gidx phys0 in
          if (__entry_is_table entry0) && (GRANULE_ALIGNED phys0) && (is_gidx lv1_gidx) then
            (* level 1 valid, hold level 1 lock *)
            let adt := adt {log: EVT CPU_ID (REL root_gidx groot {glock: Some CPU_ID}) :: EVT CPU_ID (ACQ lv1_gidx) :: log adt} in
            let glv1 := (gs (share adt)) @ lv1_gidx in
            rely prop_dec (glock glv1 = None);
            rely (tbl_level (gaux glv1) =? 1);
            if level =? 2 then
              (* walk until level 1 *)
              let adt :=  adt {priv: (priv adt) {wi_llt: lv1_gidx} {wi_index: idx1}} in
              create_table lv1_gidx idx1 rtt_addr rtt_gidx rd_gidx 2 map_addr adt
            else
              (* walk deeper level 1 *)
              rely (level >? 2);
              rely (g_tag (ginfo glv1) =? GRANULE_STATE_TABLE);
              rely (gtype glv1 =? GRANULE_STATE_TABLE);
              let entry1 := (g_data (gnorm glv1)) @ idx1 in
              rely is_int64 entry1;
              let phys1 := __entry_to_phys entry1 3 in
              let lv2_gidx := __addr_to_gidx phys1 in
              if (__entry_is_table entry1) && (GRANULE_ALIGNED phys1) && (is_gidx lv2_gidx) then
                (* level 2 valid, hold level 2 lock *)
                when adt == query_oracle adt;
                let adt := adt {log: EVT CPU_ID (REL lv1_gidx glv1 {glock: Some CPU_ID}) :: EVT CPU_ID (ACQ lv2_gidx) :: log adt} in
                let glv2 := (gs (share adt)) @ lv2_gidx in
                rely (tbl_level (gaux glv2) =? 2);
                rely prop_dec (glock glv2 = None);
                if level =? 3 then
                  (* walk until level 2 *)
                  let adt :=  adt {priv: (priv adt) {wi_llt: lv2_gidx} {wi_index: idx2}} in
                  create_table lv2_gidx idx2 rtt_addr rtt_gidx rd_gidx 3 map_addr adt
                else None
              else
                (* level 2 invalid *)
                Some (adt {log: EVT CPU_ID (REL lv1_gidx glv1 {glock: Some CPU_ID}) :: log adt}
                          {priv: (priv adt) {wi_llt: 0} {wi_index: ret_idx}}, VZ64 1)
          else
            (* level 1 invalid *)
            Some (adt {log: EVT CPU_ID (REL root_gidx groot {glock: Some CPU_ID}) :: log adt}
                      {priv: (priv adt) {wi_llt: 0} {wi_index: ret_idx}}, VZ64 1)
    end.

End Spec.

author: columbia


text:
Require Import QArith.
Require Import Setoid.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import profinite.
Require Import cusl.

Require Import rational_intervals.
Require Import realdom.

Require Import Qabs.
Require Import Qminmax.

Record convergence_rate :=
  { convg :> N -> Q
  ; convg_decreasing : forall n1 n2, (n1 <= n2)%N -> (convg n1 >= convg n2)%Q
  ; convg_pos : forall n, 0 < convg n
  ; convg_small : forall ε:Q, 0 < ε -> exists n, convg n <= ε
  }.

Program Definition convg_interval (θ:convergence_rate) (n:N) :=
  RatInt (-θ n) (θ n) _.
Next Obligation.
  intros.
  apply Qle_trans with 0%Q.
  rewrite <- (Qplus_le_l _ _ (θ n)). ring_simplify.
  apply Qlt_le_weak. apply convg_pos.
  apply Qlt_le_weak. apply convg_pos.
Qed.

Require Import flat.

Program Definition enumN : enumtype :=
  Enumtype N (fun n => Some n) _ N.eq_dec.
Next Obligation.
  intro x. exists x. auto.
Qed.

Lemma Ndownset (n:N) :
  { l:finset (flat enumN) | forall m:flat enumN, (m < n)%N <-> m ∈ l }.
Proof.
  induction n using N.peano_rect.
  exists nil.
  intuition.
  compute in H. destruct m; discriminate.
  apply nil_elem in H. elim H.
  destruct IHn as [l ?].
  exists (n::l)%list.
  intuition.
  apply N.lt_succ_r in H.
  apply N.le_lteq in H.
  destruct H.
  apply (@cons_elem (flat enumN)).
  right. apply i. auto.
  apply (@cons_elem (flat enumN)).
  left. split; hnf; auto.
  apply N.lt_succ_r.
  apply N.le_lteq.
  apply (@cons_elem (flat enumN)) in H.
  destruct H.
  right.
  destruct H. hnf in H. auto.
  left. apply i. auto.
Qed.

(**)

  Definition partial_limit (n:N) (x:cut_preord) :=
    forall m, (m <= n)%N -> widen_cut m (seq m) ≤ x.

  Program Definition limit_uppers (n:N) : eset Qpreord :=
    image (Preord.Hom _ _ (Qplus (oneOver2n n)) _)
     (esubset
            (fun q => forall m:flat enumN, m ∈ proj1_sig (Ndownset n) ->
                      exists q',
                        q' ∈ cut_upper (seq m) /\
                        q' <= q + oneOver2n n + oneOver2n m )
            _
            (cut_upper (seq n))).
  Next Obligation.
    intros. red in H. simpl in H.
    red; simpl. rewrite H. reflexivity.
  Qed.
  Next Obligation.
    intros.
    apply all_finset_semidec.
    intros. destruct H0 as  [q' [??]]. exists q'; split; auto.
    destruct H. hnf in H . subst a0. auto.
    destruct H. hnf in H . subst a0. auto.
admit.
(*
    intro m.
    apply (semidec_ex _ _ (fun a q' => q' ∈ cut_upper (seq m) /\ q' + oneOver2n m <= a)).
    intros x y z [??]. red in H. simpl in H.
    intros [??].
    rewrite H in H2. split; auto.
    apply member_eq with y; auto.
    apply Qpreord_eff.
    intros [a' q']. simpl.
    apply semidec_conj.
    apply semidec_in.
    constructor. apply eff_ord_dec. apply Qpreord_eff.
    apply dec_semidec.
*)
(*
    destruct (Qlt_le_dec (a' + oneOver2n m) q').
    right; intro.
    eapply Qlt_irrefl.
    eapply Qle_lt_trans; eauto.
    left; auto.
*)
  Qed.

  Lemma limit_least_partial_limit_upper l :
    (forall n x, partial_limit n x -> x ≤ l) ->
    limit_upper ⊆ cut_upper l.
  Proof.
    repeat intro.
    unfold limit_upper in H0.
    apply union_axiom in H0.
    destruct H0 as [X [??]].
    destruct H0 as [n ?].
    rewrite H0 in H1. clear X H0.
    unfold limit_uppers in H1.
    apply image_axiom2 in H1.
    destruct H1 as [y [??]]; simpl in *.
    apply esubset_elem in H0.
    destruct H0.

  Qed.

  Lemma cut_upper_partial_limit a n :
    a ∈ limit_uppers n ->
    exists x, partial_limit n x /\ a ∈ cut_upper x.
  Proof.
    intros.
    unfold limit_uppers in H.
    apply image_axiom2 in H. destruct H as [y [??]].
    simpl in H0.
    apply esubset_elem in H.
    destruct H.

    assert (exists w:cut,
              (forall ru, ru ∈ cut_upper w <->
                          y+oneOver2n n <= ru /\
                          (forall m, (m <= n)%N ->
                              exists q', q' ∈ cut_upper (seq m) /\
                                         q' + oneOver2n m <= ru))
               /\
               (forall rl, rl ∈ cut_lower w ->
                           (forall m, (m <= n)%N ->
                                      (rl + oneOver2n m)%Q ∈ cut_lower (seq m)))).
admit.

    destruct H2 as [w [??]].
    exists w.
    split.
    red; intros.
    split; red; simpl; intros.
    apply image_axiom1'. simpl.
    apply H2 in H5.
    destruct H5.
    destruct (H6 m) as [q' [??]]; auto.
    exists (a0 - oneOver2n m).
    split.
    simpl in *; split; red; simpl; ring.
    apply cut_is_upper with q'; auto.
    apply (Qplus_le_l _ _ (oneOver2n m)).
    ring_simplify. auto.
    apply image_axiom1'.
    simpl.
    exists (a0 + oneOver2n m)%Q.
    split.
    simpl in *; split; red; simpl; ring.
    apply H3; auto.

    apply H2.
    split.
    destruct H0. red in H0. simpl in H0.
    rewrite H0. rewrite Qplus_comm. apply Qle_refl.
    intros.
    apply N.lt_eq_cases in H4. destruct H4.
    destruct (H1 m) as [q' [??]].
    destruct (Ndownset n); simpl. apply i; auto.
    exists q'. split; auto.
    destruct H0. red in H0. simpl in H0. rewrite H0.
    apply (Qplus_le_l _ _ (- oneOver2n m)).
    ring_simplify.
    eapply Qle_trans. apply H6.
    ring_simplify. apply Qle_refl.

    subst n.
    exists y. split; auto.
    destruct H0.
    red in H0. simpl in H0.
    rewrite H0.
    rewrite (Qplus_comm). apply Qle_refl.

  Qed.
*)

  Program Definition limit_lowers (n:N) : eset Qpreord :=
    image (Preord.Hom _ _ (Qplus (-oneOver2n n)) _)
     (esubset
            (fun q => forall m:flat enumN, m ∈ proj1_sig (Ndownset n) ->
                      exists q',
                        q' ∈ cut_lower (seq m) /\
                        q <= q' + oneOver2n m + oneOver2n n)
            _
            (cut_lower (seq n))).
  Next Obligation.
    intros. red; simpl.
    red in H; simpl in H. rewrite H. reflexivity.
  Qed.
  Next Obligation.
    intros.
    apply all_finset_semidec.
    intros. destruct H0 as  [q' [??]]. exists q'; split; auto.
    destruct H. hnf in H . subst a0. auto.
    destruct H. hnf in H . subst a0. auto.
    intro m.
    apply (semidec_ex _ _ (fun a q' => q' ∈ cut_lower (seq m) /\ a <= q' + oneOver2n m + oneOver2n n )).
    intros x y z [??]. red in H. simpl in H.
    intros [??].
    rewrite H in H2. split; auto.
    apply member_eq with y; auto.
    apply Qpreord_eff.
    intros [a' q']. simpl.
    apply semidec_conj.
    apply semidec_in.
    constructor. apply eff_ord_dec. apply Qpreord_eff.
    apply dec_semidec.
    destruct (Qlt_le_dec (q'  + oneOver2n m  + oneOver2n n) (a')).
    right; intro.
    apply (Qlt_irrefl a').
    eapply Qle_lt_trans; eauto.
    left; auto.
  Qed.

  Definition limit_lower : eset Qpreord :=
    union ( (fun n => Some (limit_lowers n)) : eset (eset Qpreord)).

  Program Definition limit : cut :=
    Cut limit_upper limit_lower _ _ _ _.
  Next Obligation.
    simpl; intros.
    apply union_axiom in H.
    apply union_axiom in H0.
    destruct H as [R [??]].
    destruct H0 as [S [??]].
    destruct H as [n ?].
    destruct H0 as [m ?].
    rewrite H in H1.
    rewrite H0 in H2. clear H H0.
    unfold limit_uppers in H1.
    apply image_axiom2 in H1.
    destruct H1 as [y [??]].
    simpl in *.
    destruct H0 as [? _]. red in H0; simpl in H0.
    rewrite H0.
    apply esubset_elem in H.
    destruct H.
    unfold limit_lowers in H2.
    apply image_axiom2 in H2.
    destruct H2 as [y' [??]].
    simpl in *.
    destruct H3 as [? _]. red in H3. simpl in H3. rewrite H3.
    apply esubset_elem in H2.
    destruct H2.
    destruct (N.compare_spec n m).
    subst m.
    apply Qplus_le_compat.
    apply Qle_trans with 0%Q.
    rewrite <- (Qplus_le_l _ _ (oneOver2n n)).
    ring_simplify. apply Qlt_le_weak. apply oneOver2n_pos.
    apply Qlt_le_weak. apply oneOver2n_pos.
    apply cut_proper with (seq n); auto.
    destruct (H4 n) as [q' [??]].
    destruct (Ndownset m); simpl in *.
    apply i; auto.
    rewrite <- (Qplus_le_l _ _ (oneOver2n m)).
    ring_simplify.
    apply Qle_trans with (q' + oneOver2n n + oneOver2n m)%Q. auto.
    rewrite <- (Qplus_le_l _ _ (- (oneOver2n n + oneOver2n m))). ring_simplify.
    apply cut_proper with (seq n); auto.
    destruct (H1 m) as [q' [??]].
    destruct (Ndownset n); simpl in *.
    apply i; auto.
    rewrite <- (Qplus_le_l _ _ (oneOver2n m)).
    ring_simplify.
    apply Qle_trans with q'; auto.
    apply cut_proper with (seq m); auto.
    eapply Qle_trans. apply H7.
    ring_simplify. apply Qle_refl.

    simpl; intros.
    destruct (H5 m0) as [q' [??]]; auto.
    exists q'; split; auto.
    destruct H4. red in H4. simpl in H4.
    rewrite <- H4; auto.

    simpl; intros.
    destruct (H3 m0) as [q' [??]]; auto.
    exists q'; split; auto.
    destruct H1. red in H1. simpl in H1.
    rewrite <- H1; auto.
  Qed.
  Next Obligation.
    unfold limit_lower.
    simpl; intros.
    apply union_axiom in H0.
    apply union_axiom.
    destruct H0 as [X [??]].
    exists X. split; auto.
    destruct H0 as [n ?].
    rewrite H0. rewrite H0 in H1.
    unfold limit_lowers in H1.
    unfold limit_lowers.
    apply image_axiom2 in H1.
    destruct H1 as [q [??]]. simpl in *.
    apply image_axiom1'. simpl.
    apply esubset_elem in H1.
    destruct H1.
    exists (q1 + oneOver2n n)%Q.
    split.
    split; red; simpl; ring.
    apply esubset_elem.
    intros.
    destruct (H5 m) as [q' [??]]; auto.
    exists q'.
    split; auto.
    destruct H4.
    red in H4. simpl in H4. rewrite <- H4; auto.
    split.
    apply cut_is_lower with q; auto.
    apply Qle_trans with (q2 + oneOver2n n)%Q.
    apply Qplus_le_compat; auto. apply Qle_refl.
    destruct H2. red in H2; simpl in H2. rewrite H2.
    ring_simplify. apply Qle_refl.
    intros.
    destruct (H3 m) as [q' [??]]; auto.
    exists q'. split; auto.
    apply Qle_trans with q; auto.
    apply Qle_trans with (q2 + oneOver2n n)%Q.
    apply Qplus_le_compat; auto. apply Qle_refl.
    destruct H2. red in H2; simpl in H2. rewrite H2.
    ring_simplify. apply Qle_refl.
    intros.
    destruct (H4 m) as [q' [??]]; auto. exists q'; split; auto.
    destruct H3 as [? _]. red in H3. simpl in H3.
    rewrite <- H3; auto.
  Qed.
  Next Obligation.
    unfold limit_upper.
    simpl; intros.
    apply union_axiom in H0.
    apply union_axiom.
    destruct H0 as [X [??]].
    exists X. split; auto.
    destruct H0 as [n ?].
    rewrite H0. rewrite H0 in H1.
    unfold limit_uppers in H1.
    unfold limit_uppers.
    apply image_axiom2 in H1.
    destruct H1 as [q [??]]. simpl in *.
    apply image_axiom1'. simpl.
    apply esubset_elem in H1.
    destruct H1.
    exists (q2 - oneOver2n n)%Q.
    split.
    split; red; simpl; ring.
    apply esubset_elem.
    intros.
    destruct (H5 m) as [q' [??]]; auto.
    exists q'.
    split; auto.
    destruct H4.
    red in H4. simpl in H4. rewrite <- H4; auto.
    split.
    apply cut_is_upper with q; auto.
    apply Qle_trans with (q1 - oneOver2n n)%Q.
    destruct H2. red in H2; simpl in H2. rewrite H2.
    ring_simplify. apply Qle_refl.
    apply Qplus_le_compat; auto. apply Qle_refl.
    intros.
    destruct (H3 m) as [q' [??]]; auto.
    exists q'. split; auto.
    eapply Qle_trans. apply H6.
    apply (Qplus_le_l _ _ (oneOver2n n)).
    apply (Qplus_le_l _ _ (oneOver2n m)).
    apply Qle_trans with (q1 - oneOver2n n)%Q.
    destruct H2. red in H2. simpl in H2. rewrite H2.
    ring_simplify. apply Qle_refl.
    apply Qplus_le_compat; auto. apply Qle_refl.
    intros.
    destruct (H4 m) as [q' [??]]; auto. exists q'; split; auto.
    destruct H3 as [? _]. red in H3. simpl in H3.
    rewrite <- H3; auto.
  Qed.
  Next Obligation.
    unfold limit_upper, limit_lower.
    split; intros [x ?].
    apply union_axiom in H.
    destruct H as [X [??]].
    destruct H as [n ?]. rewrite H in H0.
    unfold limit_uppers in H0.
    apply image_axiom2 in H0.
    destruct H0 as [y [??]]. simpl in *.
    apply esubset_elem in H0. destruct H0.
    assert (exists q', q' ∈ cut_upper (seq 0) /\ q' <= y + oneOver2n 0 + oneOver2n n).
    destruct (N.compare_spec 0 n).
    subst n.
    exists y; split; auto.
    apply Qle_trans with (y+0)%Q.
    ring_simplify; auto. apply Qle_refl.
    rewrite <- Qplus_assoc.
    apply Qplus_le_compat. apply Qle_refl.
    apply Qle_trans with (0+0)%Q.
    ring_simplify. apply Qle_refl.
    apply Qplus_le_compat; apply Qlt_le_weak; apply oneOver2n_pos.
    destruct (H2 0)%N as [q' [??]].
    destruct (Ndownset n); simpl.
    apply i. auto.
    exists q'; split; auto.
    compute in H3.
    destruct n; discriminate.
    destruct H3 as [q' [??]].
    destruct (cut_nonextended (seq 0)).
    destruct H5 as [z ?]; eauto.
    exists (z  - oneOver2n 0).
    apply union_axiom.
    exists (limit_lowers 0).
    split. exists 0%N. auto.
    unfold limit_lowers.
    apply image_axiom1'.
    simpl.
    exists z. split.
    split; red; simpl in *; ring.
    apply esubset_elem.
      intros.
      destruct (H8 m) as [w [??]]; auto.
      exists w; split; auto.
      destruct H7. red in H7; simpl in H7; rewrite <- H7; auto.
    split; auto.
    intros.
    destruct (Ndownset 0); simpl in *.
    apply i in H7.
    destruct m; compute in H7; discriminate.
      intros.
      destruct (H3 m) as [w [??]]; auto.
      exists w; split; auto.
      destruct H2. red in H2; simpl in H2; rewrite <- H2; auto.

    apply union_axiom in H.
    destruct H as [X [??]].
    destruct H as [n ?]. rewrite H in H0.
    unfold limit_lowers in H0.
    apply image_axiom2 in H0.
    destruct H0 as [y [??]]. simpl in *.
    apply esubset_elem in H0. destruct H0.
    assert (exists q', q' ∈ cut_lower (seq 0) /\ y <= q' + oneOver2n 0 + oneOver2n n).
    destruct (N.compare_spec 0 n).
    subst n.
    exists y; split; auto.
    apply Qle_trans with (y+0)%Q.
    ring_simplify; auto. apply Qle_refl.
    rewrite <- Qplus_assoc.
    apply Qplus_le_compat. apply Qle_refl.
    apply Qle_trans with (0+0)%Q.
    ring_simplify. apply Qle_refl.
    apply Qplus_le_compat; apply Qlt_le_weak; apply oneOver2n_pos.
    destruct (H2 0)%N as [q' [??]].
    destruct (Ndownset n); simpl.
    apply i. auto.
    exists q'; split; auto.
    compute in H3.
    destruct n; discriminate.
    destruct H3 as [q' [??]].
    destruct (cut_nonextended (seq 0)).
    destruct H6 as [z ?]; eauto.
    exists (z  + oneOver2n 0)%Q.
    apply union_axiom.
    exists (limit_uppers 0).
    split. exists 0%N. auto.
    unfold limit_uppers.
    apply image_axiom1'.
    simpl.
    exists z. split.
    split; red; simpl in *; ring.
    apply esubset_elem.
      intros.
      destruct (H8 m) as [w [??]]; auto.
      exists w; split; auto.
      destruct H7. red in H7; simpl in H7; rewrite <- H7; auto.
    split; auto.
    intros.
    destruct (Ndownset 0); simpl in *.
    apply i in H7.
    destruct m; compute in H7; discriminate.
      intros.
      destruct (H3 m) as [w [??]]; auto.
      exists w; split; auto.
      destruct H2. red in H2; simpl in H2; rewrite <- H2; auto.
  Qed.

  Lemma cut_lower_partial_limit a n :
    a ∈ limit_lowers n ->
    exists x, partial_limit n x /\ a ∈ cut_lower x.
  Admitted.

  Lemma limit_least_partial_limit l :
    (forall n x, partial_limit n x -> x ≤ l) ->
    limit ≤ l.
  Proof.
    intros. split; red; simpl; intros.
    unfold limit_upper in H0.
    apply union_axiom in H0.
    destruct H0 as [?[??]].
    destruct H0 as [n ?]. rewrite H0 in H1. clear x H0.
    apply cut_upper_partial_limit in H1.
    destruct H1 as [x [??]].
    destruct (H n x); auto.
    unfold limit_lower in H0.
    apply union_axiom in H0.
    destruct H0 as [?[??]].
    destruct H0 as [n ?]. rewrite H0 in H1. clear x H0.
    apply cut_lower_partial_limit in H1.
    destruct H1 as [x [??]].
    destruct (H n x); auto.
  Qed.

  Lemma limit_partial_limit n x :
    partial_limit n x -> x ≤ limit.
  Proof.
    intros. split.
    red; simpl; intros.
    red in H.
    unfold limit_upper.
    apply union_axiom.
    exists (limit_uppers n).
    split; simpl. exists n. auto.
    unfold limit_uppers.
    apply image_axiom1'. simpl.
    exists (a - oneOver2n n).
    split.
    split; red; simpl; ring.
    apply esubset_elem.
admit.
    split.
    destruct (H n). apply N.le_refl.
    simpl in H1.
    generalize (H1 a H0).
    intros. apply image_axiom2 in H3.
    destruct H3 as [?[??]]. simpl in *.
    apply member_eq with x0; auto.
    destruct H4. red in H4; simpl in H4.
    split; red; simpl; rewrite H4; ring.
    intros.
    destruct (H m).
    destruct (Ndownset n); simpl in *.
    apply i in H1.
    apply N.lt_le_incl; auto.
    generalize (H2 a H0); intros.
    simpl in H4.
    apply image_axiom2 in H4.
    destruct H4 as [y [??]].
    simpl in *.
    exists y. split; auto.
    ring_simplify.
    destruct H5 as [??]. red in H5. simpl in H5.
    rewrite H5.

  Qed.

Section cut_limit.

Section real_limit.
  Variable θ:convergence_rate.
  Variable A:∂PLT.
  Variable f:(A ⊗ flat enumN → PreRealDom)%plt.

  Let P (anr:(prod_preord (prod_preord A (flat enumN)) PreRealDom)) :=
      forall m:flat enumN, m ∈ proj1_sig (Ndownset (snd (fst anr))) ->
         exists r',
           (fst (fst anr),m,r') ∈ PLT.hom_rel f /\
           rint_plus r' (convg_interval θ m) ≤ snd anr.

  Program Definition widen_sequence :
    Preord.hom (prod_preord (prod_preord A (flat enumN)) PreRealDom)
               (prod_preord A PreRealDom)
    := Preord.Hom _ _
                  (fun anr => (fst (fst anr)
                  , rint_plus (convg_interval θ (snd (fst anr))) (snd anr)
                  ))
        _.
  Next Obligation.
    simpl; intros.
    destruct a as [[??]?].
    destruct b as [[??]?].
    destruct H as [[??]?]. simpl in *.
    split; simpl; auto.
    hnf; intros.
    apply rint_plus_correct in H2.
    apply rint_plus_correct.
    destruct H2 as [q1 [q2 [?[??]]]].
    exists q1. exists q2. intuition.
    hnf in H0. subst n0. auto.
  Qed.

  Lemma Psemidec : forall ar, semidec (P ar).
Admitted.
(*
  Proof.
    intro ar.
    unfold P.
    apply (semidec_ex (prod_preord A PreRealDom) (flat enumN)
            (fun ar n =>
               rint_end (snd ar) - rint_start (snd ar) >= θ n /\
      (forall m:flat enumN, m ∈ proj1_sig (Ndownset n) ->
         exists r',
           (fst ar,m,r') ∈ PLT.hom_rel f /\
           exists q, in_interval q r' /\ in_interval q (snd ar)) /\

               (fst ar, n, snd ar) ∈ PLT.hom_rel f)).
    intros a b c ?. intuition.
    hnf in H. destruct H. hnf in H. subst c. auto.
    destruct H. hnf in H. subst c. auto.
    revert H3. apply (PLT.hom_order _ _ _ f); auto.
    destruct H; split; auto.
    apply PLT.effective.
    intros.
    apply semidec_conj.
    apply dec_semidec.
    destruct (Qlt_le_dec
                (rint_end (snd (fst ab)) - rint_start (snd (fst ab)))
                (θ (snd ab))).
    right. intro.
    apply (Qlt_irrefl (θ (snd ab))).
    eapply Qle_lt_trans; eauto.
    left; auto.
    apply semidec_conj.
    apply all_finset_semidec.
    intros. destruct H. hnf in H. subst b. auto.
    intro a.
    apply (semidec_ex (flat enumN) PreRealDom
      (fun a r' =>
        (fst (fst ab), a, r') ∈ PLT.hom_rel f /\
        (exists q : Q, in_interval q r' /\ in_interval q (snd (fst ab))))).
    intuition.
    revert H1.
    apply (PLT.hom_order _ _ _ f); auto.
    destruct H2 as [q [??]]. exists q. split; auto.
    destruct H. apply H3. auto.
    apply PLT.effective.
    intros.
    apply semidec_conj.
    apply semidec_in.
    constructor.
    apply eff_ord_dec.
    apply effective_prod.
    apply effective_prod.
    apply PLT.effective.
    apply PLT.effective.
    apply PLT.effective.
    apply dec_semidec.
    destruct (cusl_lub _ rint_cusl (snd ab0) (snd (fst ab))).
    destruct s as [z [?[??]]].
    left.
    exists (rint_start z).
    split.
    apply H.
    split. apply Qle_refl. apply rint_proper.
    apply H0.
    split. apply Qle_refl. apply rint_proper.
    right; intro.
    destruct H as [q [??]].
    apply (f0 (RatInt q q (Qle_refl q))).
    apply rint_ord_test; simpl; auto.
    apply rint_ord_test; simpl; auto.
    apply semidec_in.
    constructor.
    apply eff_ord_dec.
    apply effective_prod.
    apply effective_prod.
    apply PLT.effective.
    apply PLT.effective.
    apply PLT.effective.
  Qed.
*)

  Definition real_limit_rel : erel A PreRealDom :=
    image widen_sequence (esubset P Psemidec (PLT.hom_rel f)).

  Lemma real_limit_rel_elem a r :
    (a,r) ∈ real_limit_rel <->
    exists x,
      x ∈ PLT.hom_rel f /\ P x /\ widen_sequence x ≈ (a,r).
  Proof.
    unfold real_limit_rel.
    split; intros.
    apply image_axiom2 in H. destruct H as [x [??]].
    apply esubset_elem in H. destruct H. eauto.
    unfold P; intros.
    destruct a0 as [[??]?].
    destruct b as [[??]?].
    destruct H1 as [[[??]?][[??]?]]. simpl in *.
    hnf in H7. subst c3. clear H4.
    destruct (H2 m) as [r' [??]]; auto.
    exists r'; intuition.
    apply (PLT.hom_order _ _ _ f) with (c,m) r'; auto.
    split; auto.
    etransitivity; eauto.

    destruct H as [x [?[??]]].
    apply image_axiom1'.
    exists x; intuition.
    rewrite esubset_elem. split; auto.

    unfold P; intros.
    destruct a0 as [[??]?].
    destruct b as [[??]?].
    destruct H2 as [[[??]?][[??]?]]. simpl in *.
    hnf in H8. subst c3. clear H5.
    destruct (H3 m) as [r' [??]]; auto.
    exists r'; intuition.
    apply (PLT.hom_order _ _ _ f) with (c,m) r'; auto.
    split; auto.
    etransitivity; eauto.
  Qed.

(*
  Definition real_limit_rel : erel A PreRealDom :=
      (@esubset (prod_preord A PreRealDom) P Psemidec
                (eff_enum _ (effective_prod (PLT.effective A) (PLT.effective PreRealDom)))
       ).

  Lemma real_limit_rel_elem : forall a r,
    (a,r) ∈ real_limit_rel <->
    P (a,r).
  Proof.
    intros. unfold real_limit_rel.
    rewrite esubset_elem.
    intuition. apply eff_complete.
    unfold P; simpl; intros.
    destruct H0 as [n [??]]. exists n. split; auto.
    destruct H.
    destruct a0 as [p q]. destruct b as [p' q'].
    destruct H. destruct H2. simpl in *.
    apply rint_ord_test in H3.
    apply rint_ord_test in H4.
    assert (rint_end q == rint_end q').
    apply Qle_antisym; intuition.
    assert (rint_start q == rint_start q').
    apply Qle_antisym; intuition.
    rewrite <- H5. rewrite <- H6.
    auto.
    destruct H1. split.
    intros.
    destruct (H1 m) as [r' [?[?[??]]]]; auto.
    exists r'; intuition.
    destruct H as [[??][??]].
    revert H4. apply (PLT.hom_order _ _ _ f); auto.
    split; simpl; auto.
    exists x; split; auto.
    destruct H as [[??][??]].
    apply H9. auto.
    destruct H as [[??][??]].

    revert H2. apply (PLT.hom_order _ _ _ f); auto.
    split; auto.
  Qed.
*)

  Program Definition real_limit : A → PreRealDom :=
    PLT.Hom true A PreRealDom real_limit_rel _ _ .
  Next Obligation.
    intros; simpl.
    apply real_limit_rel_elem in H1.
    apply real_limit_rel_elem.
    destruct H1 as [z [?[??]]].
    destruct z as [[x0 n] y0].
    simpl in H3.
    destruct H3 as [[??][??]].
    simpl in *.
    admit.
Qed.
Next Obligation.
    intro a.
    apply prove_directed; auto.
    simpl; intros.
    apply erel_image_elem in H.
    apply erel_image_elem in H0.
    apply real_limit_rel_elem in H.
    apply real_limit_rel_elem in H0.

    destruct H as [[[a1 n1] r1] [?[??]]].
    destruct H0 as [[[a2 n2] r2] [?[??]]].

    destruct (N.compare_spec n1 n2).
admit.

    exists y. split.
    red in H3.
    destruct (H3 n1) as [r' [??]].
    simpl.
    destruct (Ndownset n2).
    simpl. apply i. auto.
    simpl in H6. simpl in H7.
    simpl in H4.
    destruct H4 as [[??][??]].
    simpl in *.
    etransitivity. 2: apply H8.
    destruct H2 as [[??][??]].
    simpl in *.
    etransitivity. apply H13.
    apply rint_ord_test; simpl.
    apply rint_ord_test in H7. simpl in H7.
    destruct H7; split.

    etransitivity. apply H13.
    hnf; intros.
    hnf in H9.
    hnf in H7.

admit.

    destruct (plt_hom_directed2 _ _ _ f (a,n1) r1 r2)
       as [z [?[??]]]; auto.
admit. admit.
    exists (rint_plus (convg_interval θ n1) z).
    split.
admit.
    split.
admit.

    apply erel_image_elem.
    apply real_limit_rel_elem.
    exists (a,n1,z). simpl; split; auto. split; auto.
    red; simpl; intros.
    destruct (H1 m) as [q1 [??]]; simpl; auto.
    simpl in *.
    destruct (H3 m) as [q2 [??]]; simpl; auto.
    simpl in *.
    destruct (plt_hom_directed2 _ _ _ f (a1,m) q1 q2)
       as [q [?[??]]]; auto.
admit.

admit.

    hnf in H3. simpl in H3.
    destruct (H3 n1) as [r' [??]].
    destruct (Ndownset n2). simpl. apply i. auto.
    destruct (cusl_lub _ rint_cusl r' r1).
    destruct s as [r'' [?[??]]].
    exists (rint_plus r'' (convg_interval θ n1)).
    split.
admit.
    split.
    hnf; intros.
admit.
    apply erel_image_elem.
    apply real_limit_rel_elem.

    exists q. split; auto.
admit.
    etransitivity. 2: apply H10.

    red.
    exists n1. simpl.

    exists (x', n, rint_plus y' (rint_opp (convg_interval θ n))). simpl. split.
    revert H1. apply (PLT.hom_order _ _ _ f).
    split; simpl; auto.
    etransitivity; eauto.
    hnf; intros.
    apply rint_plus_correct.
    hnf in H6.
    hnf in H0.
    exists q. exists 0%Q.
    intuition.
    apply H0.
    apply H6.
    apply rint_plus_correct.
    exists 0%Q. exists q.
    intuition.
    split; simpl.
    rewrite <- (Qplus_le_l _ _ (θ n)). ring_simplify.
    generalize (convg_pos θ n). intuition.
    generalize (convg_pos θ n). intuition.
    ring.
    split; simpl.
    rewrite <- (Qplus_le_l _ _ (θ n)). ring_simplify.
    generalize (convg_pos θ n). intuition.
    rewrite Qopp_involutive.
    generalize (convg_pos θ n). intuition.
    ring.
    split.
    red. simpl. intros.
    destruct (H2 m H7) as [r' [??]]. simpl in *.
    exists r'. split; auto.
    revert H8.
    apply (PLT.hom_order _ _ _ f).
    split; simpl; auto.
    etransitivity; eauto.
    auto.
    hnf; intros.
    apply H9 in H10.
    apply rint_plus_correct in H10.
    destruct H10 as [q1 [q2 [?[??]]]].
    hnf in H6.
    hnf in H0.
    apply rint_plus_correct.
    exists q1. exists q2. intuition.
    apply rint_plus_correct.
    exists q1. exists 0%Q.
    split.
    apply H0.
    apply H6.
    apply rint_plus_correct.
    exists 0%Q. exists q1.
    intuition.
    split; simpl.
    rewrite <- (Qplus_le_l _ _ (θ n)). ring_simplify.
    generalize (convg_pos θ n). intuition.
    generalize (convg_pos θ n). intuition.
    ring.
    split. split; simpl.
    rewrite <- (Qplus_le_l _ _ (θ n)). ring_simplify.
    generalize (convg_pos θ n). intuition.
    rewrite Qopp_involutive.
    generalize (convg_pos θ n). intuition.
    ring.

    split; split; simpl; auto.
    apply rint_ord_test. simpl.
    split; ring_simplify.
    admit. admit.
    apply rint_ord_test. simpl.
    split; ring_simplify.

    hnf; simpl. intros.

    subst P. simpl in *.
    destruct H1 as [n [??]].
    exists n. split.
    eapply Qle_trans. apply H1.
    rewrite <- (Qplus_le_l _ _ (rint_start y')).
    rewrite <- (Qplus_le_l _ _ (rint_start y)).
    ring_simplify.
    rewrite (Qplus_comm (rint_end y)).
    apply rint_ord_test in H0. destruct H0.
    apply Qplus_le_compat; auto.
    destruct H2. split.
    intros.
    destruct (H2 m) as [r' [?[?[??]]]]; auto.
    exists r'; split; auto.
    revert H5. apply (PLT.hom_order _ _ _ f); auto.
    split; auto.
    exists x0; split; auto.
    revert H3. apply (PLT.hom_order _ _ _ f); auto.
    split; auto.
  Qed.
  Next Obligation.
    intro a.
    apply prove_directed; auto.
    simpl; intros.
    apply erel_image_elem in H.
    apply erel_image_elem in H0.
    apply real_limit_rel_elem in H.
    apply real_limit_rel_elem in H0.
    unfold P in H.
    unfold P in H0. simpl in *.
    destruct H as [n1 [?[??]]].
    destruct H0 as [n2 [?[??]]].

    destruct (N.compare_spec n1 n2).
    subst n2.
    destruct (plt_hom_directed2 _ _ _ f (a,n1) x y)
       as [z [?[??]]]; auto.

    exists z. intuition.
    apply erel_image_elem.
    apply real_limit_rel_elem.
    red.
    exists n1. simpl.

  Qed.

semidec_ex:
  forall (A B : preord) (P : A -> B -> Prop),
  (forall (a : A) (b c : Preord_Eq B), b ≈ c -> P a b -> P a c) ->
  effective_order B ->
  (forall ab : A * B, semidec (P (fst ab) (snd ab))) ->
  forall a : A, semidec (exists x, P a x)

author: robdockins

repo: domains

save_path: github-repos/coq/robdockins-domains


text:
(* This module contains additional definitions that can only be defined after *)
(* the Cryptol prelude has been defined. *)

From Coq          Require Import Lists.List.
From Coq          Require Import String.
From Coq          Require Import Vectors.Vector.
From CryptolToCoq Require Import SAWCoreScaffolding.
From CryptolToCoq Require Import SAWCorePrelude.
Import SAWCorePrelude.
From CryptolToCoq Require Import SAWCorePreludeExtra.
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
Import CryptolPrimitives.

Import ListNotations.

(** It is annoying to have to wrap natural numbers into [TCNum] to use them at
type [Num], so these coercions will do it for us.
 *)
Coercion TCNum : Nat >-> Num.
Definition natToNat (n : nat) : Nat := n.
Coercion natToNat : nat >-> Nat.

Theorem Eq_TCNum a b : a = b -> Eq _ (TCNum a) (TCNum b).
Proof.
  intros EQ.
  rewrite EQ.
  reflexivity.
Qed.

Theorem min_S n : min n (S n) = n.
Proof.
  rewrite PeanoNat.Nat.min_comm.
  induction n.
  { reflexivity. }
  { simpl in *. intuition. }
Qed.

Ltac solveUnsafeAssertStep :=
  match goal with
  | [ |- context [ Succ ] ] => unfold Succ
  | [ n : Num |- _ ] => destruct n
  | [ |- Eq Num (TCNum _) (TCNum _) ] => apply Eq_TCNum
  | [ |- Eq Num _ _ ] => reflexivity
  | [ |- context [ minNat _ _ ] ] => rewrite minNat_min
  | [ |- min ?n (S ?n) = ?n ] => apply min_S
  end.

Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl).

Definition cbc_enc_helper n : Eq Num (tcMin n (tcAdd (TCNum 1) n)) n :=
  ltac:(solveUnsafeAssert).

(*
Goal forall n p b, Eq Num (tcAdd n (tcAdd (TCNum 32) p)) (tcMul (tcAdd (TCNum 2) b) (TCNum 16)).
  intros.
  simpl.
  solve_unsafeAssert_step. simpl.

Goal forall n0, Eq Num TCInf
   (TCNum
      (S
         (S
            (S
               (S
                  (S
                     (S
                        (S
                           (S
                              (S
                                 (S
                                    (S
                                       (S
                                          (S
                                             (S
                                                (S
                                                   (S
                                                      (S
                                                         (S
                                                            (S
                                                               (S
                                                                  (S
                                                                     (S
                                                                        (S
                                                                           (S
                                                                              (S
                                                                                (S
                                                                                (S
                                                                                (S
                                                                                (S (S (S (S (mulNat n0 16)))))))))))))))))))))))))))))))))).
  intros.
  solve_unsafeAssert.
*)

Fixpoint iterNat {a : Type} (n : nat) (f : a -> a) : a -> a :=
  match n with
  | O    => fun x => x
  | S n' => fun x => iterNat  n' f (f x) (* TODO: check that this is what iter is supposed to do *)
  end
.

Fixpoint iter {a : Type} (n : Num) (f : a -> a) : a -> a :=
    match n with
    | TCNum n => fun xs => iterNat n f xs
    | TCInf   => fun xs => xs
    end
.

author: GaloisInc

repo: saw-core-coq

save_path: github-repos/coq/GaloisInc-saw-core-coq


text:
Require Import CertiGraph.lib.Coqlib.
Require Import CertiGraph.lib.Ensembles_ext.
Require Import CertiGraph.lib.EquivDec_ext.
Require Import CertiGraph.lib.List_ext.
Require Import CertiGraph.lib.relation_list.
Require Import CertiGraph.lib.Equivalence_ext.
Require Import CertiGraph.graph.graph_model.
Require Import CertiGraph.graph.graph_gen.

Section MathGraph.

Context {V E: Type} {EV: EqDec V eq} {EE: EqDec E eq}.

Class MathGraph (pg: PreGraph V E) (is_null: DecidablePred V): Prop := {
  weak_valid: V -> Prop := fun p => is_null p \/ vvalid pg p;
  valid_graph: forall e, evalid pg e -> vvalid pg (src pg e) /\ weak_valid (dst pg e);
  valid_not_null: forall x, vvalid pg x -> is_null x -> False
}.

Class MathGraph' (pg: PreGraph V E) (is_null: DecidablePred V): Prop := {
  weak_valid': V -> Prop := fun p => is_null p \/ vvalid pg p;
  valid_graph': forall e, evalid pg e -> vvalid pg (src pg e);
  valid_not_null': forall x, vvalid pg x -> is_null x -> False
}.

Context {is_null: DecidablePred V}.

Lemma is_null_dec: forall x, {is_null x} + {~ is_null x}.
Proof.
  intros.
  destruct is_null as [P ?].
  simpl.
  auto.
Qed.

Arguments weak_valid _ {_} {_}  _.
Arguments valid_graph _ {_} {_} _ _.
Arguments valid_not_null _ {_} {_} _ _ _.
Arguments weak_valid' _ {_} {_}  _.
Arguments valid_graph' _ {_} {_} _ _.
Arguments valid_not_null' _ {_} {_} _ _ _.

Definition well_defined_list (pg: PreGraph V E) {ma: MathGraph pg is_null} (l : list V) := forall x, In x l -> weak_valid pg x.

Lemma valid_step: forall (pg: PreGraph V E) {ma: MathGraph pg is_null} x y, step pg x y -> vvalid pg x /\ weak_valid pg y.
Proof.
  intros.
  rewrite step_spec in H.
  destruct H as [? [? [? ?]]].
  subst.
  apply valid_graph; auto.
Qed.

Lemma null_or_valid: forall (pg: PreGraph V E) {ma: MathGraph pg is_null} x,
  weak_valid pg x -> {is_null x} + {vvalid pg x}.
Proof.
  intros.
  destruct (is_null_dec x); [left | right]; auto.
  unfold weak_valid in H.
  tauto.
Qed.

Lemma math_graph_si: forall (g1 g2: PreGraph V E),
  g1 ~=~ g2 ->
  MathGraph g1 is_null ->
  MathGraph g2 is_null.
Proof.
  intros.
  constructor.
  + intros.
    pose proof (proj2 (proj1 (proj2 H) _) H1).
    pose proof valid_graph g1 e H2.
    unfold weak_valid in H3.
    rewrite (si_src1 _ _ _ H) in H3 by auto.
    rewrite (si_dst1 _ _ _ H) in H3 by auto.
    rewrite !(proj1 H) in H3.
    auto.
  + intros.
    rewrite <- (proj1 H) in H1.
    apply (valid_not_null g1 x); auto.
Qed.

Lemma math_graph_si': forall (g1 g2: PreGraph V E),
  g1 ~=~ g2 ->
  MathGraph' g1 is_null ->
  MathGraph' g2 is_null.
Proof.
  intros.
  constructor.
  + intros.
    pose proof (proj2 (proj1 (proj2 H) _) H1).
    pose proof valid_graph' g1 e H2.
    unfold weak_valid in H3.
    rewrite (si_src1 _ _ _ H) in H3 by auto.
    rewrite !(proj1 H) in H3.
    auto.
  + intros.
    rewrite <- (proj1 H) in H1.
    apply (valid_not_null' g1 x); auto.
Qed.

Lemma gen_dst_preserve_math: forall (g: PreGraph V E) e t (M: MathGraph g is_null),
    weak_valid g t -> MathGraph (pregraph_gen_dst g e t) is_null.
Proof.
  intros. refine (Build_MathGraph (pregraph_gen_dst g e t) is_null _ (valid_not_null g)).
  simpl. intros. apply (valid_graph g) in H0. destruct H0. split.
  + auto.
  + unfold updateEdgeFunc.
    destruct_eq_dec e e0.
    - apply H.
    - apply H1.
Defined.

Definition predicate_sub_mathgraph (g: PreGraph V E) (p: V -> Prop) (MA: MathGraph g is_null): MathGraph (predicate_subgraph g p) is_null.
Proof.
  refine (Build_MathGraph _ _ _ _).
  + unfold predicate_subgraph, predicate_vvalid, predicate_evalid; simpl; intros.
    pose proof valid_graph g e.
    unfold weak_valid in H0.
    tauto.
  + unfold predicate_subgraph, predicate_vvalid, predicate_evalid; simpl; intros.
    pose proof valid_not_null g x.
    tauto.
Defined.

Lemma math_graph_join: forall (g: PreGraph V E) (PV1 PV2 PV: V -> Prop) (PE1 PE2 PE: E -> Prop),
  Prop_join PV1 PV2 PV ->
  Prop_join PE1 PE2 PE ->
  MathGraph (gpredicate_subgraph PV1 PE1 g) is_null ->
  MathGraph (gpredicate_subgraph PV2 PE2 g) is_null ->
  MathGraph (gpredicate_subgraph PV PE g) is_null.
Proof.
  intros.
  constructor.
  + simpl; intro; rewrite !Intersection_spec; intros.
    destruct H, H0.
    rewrite H0 in H3; destruct H3 as [? [? | ?]].
    - pose proof valid_graph (gpredicate_subgraph PV1 PE1 g) e.
      simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7.
      specialize (H7 (conj H3 H6)).
      rewrite !H.
      tauto.
    - pose proof valid_graph (gpredicate_subgraph PV2 PE2 g) e.
      simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7.
      specialize (H7 (conj H3 H6)).
      rewrite !H.
      tauto.
  + simpl; intros.
    destruct H, H0.
    rewrite Intersection_spec, H in H3.
    destruct H3 as [? [? | ?]].
    - apply (valid_not_null (gpredicate_subgraph PV1 PE1 g) x); auto.
      simpl; rewrite Intersection_spec; auto.
    - apply (valid_not_null (gpredicate_subgraph PV2 PE2 g) x); auto.
      simpl; rewrite Intersection_spec; auto.
Qed.

Lemma math_graph_join': forall (g: PreGraph V E) (PV1 PV2 PV: V -> Prop) (PE1 PE2 PE: E -> Prop),
  Prop_join PV1 PV2 PV ->
  Prop_join PE1 PE2 PE ->
  MathGraph' (gpredicate_subgraph PV1 PE1 g) is_null ->
  MathGraph' (gpredicate_subgraph PV2 PE2 g) is_null ->
  MathGraph' (gpredicate_subgraph PV PE g) is_null.
Proof.
  intros.
  constructor.
  + simpl; intro; rewrite !Intersection_spec; intros.
    destruct H, H0.
    rewrite H0 in H3; destruct H3 as [? [? | ?]].
    - pose proof valid_graph' (gpredicate_subgraph PV1 PE1 g) e.
      simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7.
      specialize (H7 (conj H3 H6)).
      rewrite !H.
      tauto.
    - pose proof valid_graph' (gpredicate_subgraph PV2 PE2 g) e.
      simpl in H7; unfold weak_valid in H7; simpl in H7; rewrite !Intersection_spec in H7.
      specialize (H7 (conj H3 H6)).
      rewrite !H.
      tauto.
  + simpl; intros.
    destruct H, H0.
    rewrite Intersection_spec, H in H3.
    destruct H3 as [? [? | ?]].
    - apply (valid_not_null' (gpredicate_subgraph PV1 PE1 g) x); auto.
      simpl; rewrite Intersection_spec; auto.
    - apply (valid_not_null' (gpredicate_subgraph PV2 PE2 g) x); auto.
      simpl; rewrite Intersection_spec; auto.
Qed.

End MathGraph.

Arguments weak_valid {_} {_} {_} {_} _ {_} {_} _.
Arguments valid_graph {_} {_} {_} {_} _ {_} {_} _ _.
Arguments valid_not_null {_} {_} {_} {_} _ {_} {_} _ _ _.
Arguments weak_valid' {_} {_} {_} {_} _ {_} {_} _.
Arguments valid_graph' {_} {_} {_} {_} _ {_} {_} _ _.
Arguments valid_not_null' {_} {_} {_} {_} _ {_} {_} _ _ _.

author: CertiGraph

repo: CertiGraph

save_path: github-repos/coq/CertiGraph-CertiGraph


text:
(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

Require Export ZArith.
Require Import Lia.

(* Compatibility with Coq versions not supporting hint localities *)
Set Warnings "-unsupported-attributes".

Local Open Scope Z_scope.

Coercion Zpos : positive >-> Z.
Coercion Z_of_N : N >-> Z.

Lemma Zpos_plus : forall p q, Zpos (p + q) = p + q.
Proof. intros;trivial. Qed.

Lemma Zpos_mult : forall p q, Zpos (p * q) = p * q.
Proof. intros;trivial. Qed.

Lemma Zpos_xI_add : forall p, Zpos (xI p) = Zpos p + Zpos p + Zpos 1.
Proof. intros p;rewrite Zpos_xI;ring. Qed.

Lemma Zpos_xO_add : forall p, Zpos (xO p) = Zpos p + Zpos p.
Proof. intros p;rewrite Zpos_xO;ring. Qed.

Lemma Psucc_Zplus : forall p, Zpos (Pos.succ p) = p + 1.
Proof. intros p;rewrite Zpos_succ_morphism; unfold Z.succ; trivial. Qed.

#[global]
Hint Rewrite Zpos_xI_add Zpos_xO_add Pplus_carry_spec
 Psucc_Zplus Zpos_plus : zmisc.

Lemma Zlt_0_pos : forall p, 0 < Zpos p.
Proof. unfold Z.lt; trivial. Qed.

Lemma Pminus_mask_carry_spec : forall p q,
  Pminus_mask_carry p q = Pminus_mask p (Pos.succ q).
Proof.
 intros p q;generalize q p;clear q p.
 induction q;destruct p;simpl;try rewrite IHq;trivial.
 destruct p;trivial.  destruct p;trivial.
Qed.

#[global]
Hint Rewrite Pminus_mask_carry_spec : zmisc.

Ltac zsimpl := autorewrite with zmisc.
Ltac CaseEq t := generalize (refl_equal t);pattern t at -1;case t.
Ltac generalizeclear H := generalize H;clear H.

Lemma Pminus_mask_spec :
   forall p q,
    match Pminus_mask p q with
    | IsNul    => Zpos p =  Zpos q
    | IsPos k => Zpos p = q + k
    | IsNeg   => p < q
    end.
Proof.
  intros p q;
  case (Pos.sub_mask_spec p q).
  lia.
  all: intros r <-; lia.
Qed.

Definition PminusN x y :=
  match Pminus_mask x y with
  | IsPos k => Npos k
  | _ => N0
  end.

Lemma PminusN_le : forall x y:positive, x <= y -> Z_of_N (PminusN y x) = y - x.
Proof.
 intros x y Hle;unfold PminusN.
 assert (H := Pminus_mask_spec y x);destruct (Pminus_mask y x).
 rewrite H;unfold Z_of_N;auto with zarith.
 rewrite H;unfold Z_of_N;auto with zarith.
 exfalso;lia.
Qed.

Lemma Ppred_Zminus : forall p, 1< Zpos p ->  (p-1)%Z = Pos.pred p.
Proof. destruct p;simpl;trivial. intros;exfalso;lia. Qed.

Local Open Scope positive_scope.

Declare Scope P_scope.
Delimit Scope P_scope with P.
Local Open Scope P_scope.

Definition is_lt (n m : positive) :=
  match (n ?= m) with
  | Lt => true
  | _ => false
  end.
Infix "?<" := is_lt (at level 70, no associativity) : P_scope.

Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z.
Proof.
intros n m; unfold is_lt, Z.lt , Z.le, Z.compare.
rewrite Pos.compare_antisym.
case (m ?= n); simpl; auto; intros HH; discriminate HH.
Qed.

Definition is_eq a b :=
  match (a ?= b) with
  | Eq => true
  | _ => false
  end.
Infix "?=" := is_eq (at level 70, no associativity) : P_scope.

Lemma is_eq_refl : forall n, n ?= n = true.
Proof. intros n;unfold is_eq;rewrite Pos.compare_refl;trivial. Qed.

Lemma is_eq_eq : forall n m, n ?= m = true -> n = m.
Proof.
 unfold is_eq;intros n m H; apply Pos.compare_eq.
destruct (n ?= m)%positive;trivial;try discriminate.
Qed.

Lemma is_eq_spec_pos : forall n m, if n ?= m then  n = m else  m <> n.
Proof.
 intros n m; CaseEq (n ?= m);intro H.
 rewrite (is_eq_eq _ _ H);trivial.
 intro H1;rewrite H1 in H;rewrite is_eq_refl in H;discriminate H.
Qed.

Lemma is_eq_spec : forall n m, if n ?= m then Zpos n = m else Zpos m <> n.
Proof.
 intros n m; CaseEq (n ?= m);intro H.
 rewrite (is_eq_eq _ _ H);trivial.
 intro H1;inversion H1.
 rewrite H2 in H;rewrite is_eq_refl in H;discriminate H.
Qed.

Definition is_Eq a b :=
  match a, b with
  | N0, N0 => true
  | Npos a', Npos b' => a' ?= b'
  | _, _ => false
  end.

Lemma is_Eq_spec :
 forall n m, if is_Eq n m then Z_of_N n = m else Z_of_N m <> n.
Proof.
 destruct n;destruct m;simpl;trivial;try (intro;discriminate).
 apply is_eq_spec.
Qed.

(* [times x y] return [x * y], a litle bit more efficiant *)
Fixpoint times (x y : positive) {struct y} : positive :=
  match x, y with
  | xH, _ => y
  | _, xH => x
  | xO x', xO y' => xO (xO (times x' y'))
  | xO x', xI y' => xO (x' + xO (times x' y'))
  | xI x', xO y' => xO (y' + xO (times x' y'))
  | xI x', xI y' => xI (x' + y' + xO (times x' y'))
  end.

Infix "*" := times : P_scope.

Lemma times_Zmult : forall p q, Zpos (p * q)%P = (p * q)%Z.
Proof.
 intros p q;generalize q p;clear p q.
 induction q;destruct p; unfold times; try fold (times p q);
   autorewrite with zmisc; try rewrite IHq; ring.
Qed.

Fixpoint square (x:positive) : positive :=
 match x with
 | xH => xH
 | xO x => xO (xO (square x))
 | xI x => xI (xO (square x + x))
 end.

Lemma square_Zmult : forall x, Zpos (square x) = (x * x) %Z.
Proof.
 induction x as [x IHx|x IHx |];unfold square;try (fold (square x));
   autorewrite with zmisc; try rewrite IHx; ring.
Qed.

author: thery

repo: coqprime

save_path: github-repos/coq/thery-coqprime