text:
Require Import Rbase Rfunctions Rfunction_def Rtopology Lra.
Require Import MyRIneq MyNeq PSeries_reg.
Require Import Tactics.

(** * The definitions used in this file: [middle], [interval], [Rball]. *)

Definition middle (x:R) (y:R) : R := (x + y) / 2.
Definition interval_dist lb ub x := Rmin (x - lb) (ub - x).
Definition interval_size lb ub : R := (ub - lb) / 2.

Lemma interval_size_pos : forall lb ub, lb < ub -> 0 < interval_size lb ub.
Proof.
unfold interval_size.
intros ; lra.
Qed.

Definition whole_R := fun (_ : R) => True.
Definition interval (lb ub x : R) := lb <= x <= ub.
Definition open_interval (lb ub x:R) := lb < x < ub.

Definition Rball c r x := Rabs (x - c) < r.
Definition Rball_dist c r := interval_dist (c - r) (c + r).

Definition Rball_eq c r (f g : R -> R) := forall x,
  Rball c r x -> f x = g x.

Lemma Req_Rball_eq: forall f g c r,
  f == g -> Rball_eq c r f g.
Proof.
intros f g c r Heq x x_in ; apply Heq.
Qed.

Lemma Rball_eq_refl: forall c r f, Rball_eq c r f f.
Proof.
unfold Rball_eq ; trivial.
Qed.

Lemma Rball_eq_sym: forall c r f g, Rball_eq c r f g -> Rball_eq c r g f.
Proof.
unfold Rball_eq ; intros ; symmetry ; auto.
Qed.

Lemma Rball_eq_trans: forall c r f g h, Rball_eq c r f g ->
  Rball_eq c r g h -> Rball_eq c r f h.
Proof.
unfold Rball_eq ; intros ; transitivity (g x) ; auto.
Qed.

Lemma Rball_radius_pos : forall c r x,
  Rball c r x -> 0 < r.
Proof.
unfold Rball ; intros c r x Hx ; eapply Rle_lt_trans ;
 [apply Rabs_pos | eassumption].
Qed.

Require Setoid.

Add Parametric Relation (c r: R) : (R -> R) (Rball_eq c r)
reflexivity proved by (Rball_eq_refl c r)
symmetry proved by (Rball_eq_sym c r)
transitivity proved by (Rball_eq_trans c r) as Rball_eq'.

(** The center of the (interval / ball) is in the interval *)

Lemma center_in_Rball : forall c r, 0 < r -> Rball c r c.
Proof.
intros ; apply Rabs_def1 ; lra.
Qed.

Lemma center_in_interval : forall c r, 0 <= r -> interval (c - r) (c + r) c.
Proof.
intros ; split ; lra.
Qed.

Lemma center_in_open_interval : forall c r, 0 < r -> open_interval (c - r) (c + r) c.
Proof.
intros ; split ; lra.
Qed.

(** * [middle]'s properties. *)

(** Remarkable properties. *)

Lemma middle_identity : forall x, middle x x = x.
Proof.
intros ; unfold middle ; field.
Qed.

Lemma middle_comm : forall x y, middle x y = middle y x.
Proof.
intros ; unfold middle ; field.
Qed.

Lemma middle_unfold : forall x y, middle x y = (x + y) / 2.
Proof.
intros ; reflexivity.
Qed.

Lemma middle_R0 : forall x, middle (- x) x = 0.
Proof.
intros ; unfold middle ; field.
Qed.

(** Compatibility with the orders. *)

Lemma middle_is_in_the_middle : forall x y, x < y -> x < middle x y < y.
Proof.
intros x y x_lt_y ; split.
 apply Rle_lt_trans with (middle x x).
 right ; symmetry ; apply middle_identity.
 unfold middle, Rdiv ; apply Rmult_lt_compat_r ; [lra |] ;
 apply Rplus_lt_compat_l ; assumption.
 apply Rlt_le_trans with (middle y y).
 unfold middle, Rdiv ; apply Rmult_lt_compat_r ; [lra |] ;
 apply Rplus_lt_compat_r ; assumption.
 right ; apply middle_identity.
Qed.

Lemma middle_is_in_the_middle': forall x y, x <= y -> x <= middle x y <= y.
Proof.
intros x y xley ; destruct (Req_dec x y).
 subst ; rewrite middle_identity ; auto.
 split ; left ; apply middle_is_in_the_middle, Rle_neq_lt ; assumption.
Qed.

Lemma Rabs_middle_is_in_the_middle : forall x y, 0 <= x -> x < y ->
  x < Rabs (middle x y) < y.
Proof.
intros x y x_pos x_lt_y.
 assert (mxy_pos : 0 < middle x y).
  apply Rle_lt_trans with x ;
  [| apply middle_is_in_the_middle] ;
  assumption.
 rewrite Rabs_pos_eq ;
 [ apply middle_is_in_the_middle |] ;
 intuition.
Qed.

Lemma middle_le_le_pos : forall x y, 0 <= x -> 0 <= y -> 0 <= middle x y.
Proof.
intros x y x_pos y_pos ; unfold middle, Rdiv ;
  lra.
Qed.

Lemma middle_lt_lt_pos_lt : forall x y, 0 < x -> 0 < y -> 0 < middle x y.
Proof.
intros x y x_pos y_pos ; unfold middle, Rdiv ;
 lra.
Qed.

Lemma middle_le_lt_pos_lt : forall x y, 0 <= x -> 0 < y -> 0 < middle x y.
Proof.
intros x y x_pos y_pos ; unfold middle, Rdiv ;
 lra.
Qed.

Lemma middle_lt_le_pos_lt : forall x y, 0 < x -> 0 <= y -> 0 < middle x y.
Proof.
intros x y x_pos y_pos ; rewrite middle_comm ;
 apply middle_le_lt_pos_lt ; assumption.
Qed.

Lemma middle_lt_lt_neg_lt : forall x y, x < 0 -> y < 0 -> middle x y < 0.
Proof.
intros x y x_neg y_neg ; unfold middle, Rdiv ;
 replace 0 with ((x + y) * 0) by ring ;
 apply Rmult_lt_gt_compat_neg_l ; lra.
Qed.

Lemma middle_le_lt_neg_lt : forall x y, x <= 0 -> y < 0 -> middle x y < 0.
Proof.
intros x y x_pos y_pos ; unfold middle, Rdiv ;
  replace 0 with ((x + y) * 0) by ring ;
 apply Rmult_lt_gt_compat_neg_l ; lra.
Qed.

Lemma middle_lt_le_neg_lt : forall x y, x < 0 -> y <= 0 -> middle x y < 0.
Proof.
intros x y x_neg y_neg ; rewrite middle_comm ;
 apply middle_le_lt_neg_lt ; assumption.
Qed.

(** * [interval]'s properties. *)

Lemma interval_l : forall lb ub, lb <= ub -> interval lb ub lb.
Proof.
intros ; split ; [right |] ; trivial.
Qed.

Lemma interval_r : forall lb ub, lb <= ub -> interval lb ub ub.
Proof.
intros ; split ; [| right] ; trivial.
Qed.

Lemma interval_restriction : forall lb ub a b,
  interval lb ub a -> interval lb ub b ->
  included (interval a b) (interval lb ub).
Proof.
intros lb ub a b a_in b_in x x_in ; split.
 transitivity a ; [apply a_in | apply x_in].
 transitivity b ; [apply x_in | apply b_in].
Qed.

Lemma open_interval_restriction : forall lb ub a b,
  interval lb ub a -> interval lb ub b ->
  included (open_interval a b) (open_interval lb ub).
Proof.
intros lb ub a b a_in b_in x x_in ; split.
 eapply Rle_lt_trans ; [eapply a_in | eapply x_in].
 eapply Rlt_le_trans ; [eapply x_in | eapply b_in].
Qed.

Lemma interval_open_restriction : forall lb ub a b,
  open_interval lb ub a -> open_interval lb ub b ->
  included (interval a b) (open_interval lb ub).
Proof.
intros lb ub a b a_in b_in x x_in ; split.
 eapply Rlt_le_trans ; [eapply a_in | eapply x_in].
 eapply Rle_lt_trans ; [eapply x_in | eapply b_in].
Qed.

Lemma open_interval_interval : forall lb ub x,
     open_interval lb ub x -> interval lb ub x.
Proof.
 intros ; split ; unfold open_interval in * ; intuition.
Qed.

Lemma interval_inhabited : forall lb ub x,
  interval lb ub x -> lb <= ub.
Proof.
intros ; etransitivity ; eapply_assumption.
Qed.

Lemma open_interval_inhabited : forall lb ub x,
  open_interval lb ub x -> lb < ub.
Proof.
intros ; etransitivity ; eapply_assumption.
Qed.

Lemma interval_opp_compat : forall lb ub x,
     interval lb ub x ->
     interval (-ub) (-lb) (-x).
Proof.
intros ; unfold interval in * ; split ; intuition ; lra.
Qed.

Lemma interval_minus_compat : forall lb ub x y,
  interval lb ub x -> interval (lb - y) (ub - y) (x - y).
Proof.
intros lb ub x y [Hlb Hub] ; split ; lra.
Qed.

Lemma interval_minus_compat_0 : forall lb ub x,
  interval lb ub x -> interval (lb - x) (ub - x) 0.
Proof.
intros lb ub x ; replace 0 with (x - x) by ring ;
 apply interval_minus_compat.
Qed.

Lemma open_interval_opp_compat : forall lb ub x,
     open_interval lb ub x ->
     open_interval (-ub) (-lb) (-x).
Proof.
intros ; unfold open_interval in * ; split ; intuition ; lra.
Qed.

Lemma interval_middle_compat: forall lb ub x y,
  interval lb ub x -> interval lb ub y ->
  interval lb ub (middle x y).
Proof.
intros lb ub x y x_in_I y_in_I.
  split ; unfold middle, interval in *.
  replace lb with ((lb + lb) * /2) by field.
  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
  replace ub with ((ub + ub) * /2) by field.
  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
Qed.

Lemma open_interval_middle_compat:  forall lb ub x y,
  open_interval lb ub x -> open_interval lb ub y ->
  open_interval lb ub (middle x y).
Proof.
intros lb ub x y x_in_I y_in_I.
  split ; unfold middle, open_interval in *.
  replace lb with ((lb + lb) * /2) by field.
  unfold Rdiv ; apply Rmult_lt_compat_r ; intuition.
  replace ub with ((ub + ub) * /2) by field.
  unfold Rdiv ; apply Rmult_lt_compat_r ; intuition.
Qed.

(** Decidability results. *)

Lemma in_interval_dec: forall lb ub x,
  { interval lb ub x } + { ~ interval lb ub x }.
Proof.
intros lb ub x.
  destruct (Rle_lt_dec lb x).
   destruct (Rle_lt_dec x ub).
    left ; split ; assumption.
    right ; intros [_ Hf] ; lra.
   right ; intros [Hf _] ; lra.
Qed.

Lemma in_open_interval_dec: forall lb ub x,
  { open_interval lb ub x } + { ~ open_interval lb ub x }.
intros lb ub x.
  destruct (Rlt_le_dec lb x).
   destruct (Rlt_le_dec x ub).
    left ; split ; assumption.
    right ; intros [_ Hf] ; lra.
   right ; intros [Hf _] ; lra.
Qed.

Lemma interval_open_interval_dec: forall lb ub x,
  interval lb ub x ->
  { x = lb } + { open_interval lb ub x } + { x = ub }.
Proof.
intros lb ub x [H1 H2].
  destruct (Req_dec x lb).
   left ; left ; assumption.
   destruct (Req_dec x ub).
    right ; assumption.
    left ; right ; split.
     apply Rneq_le_lt ; [symmetry |] ; assumption.
     apply Rneq_le_lt ; assumption.
Qed.

(** Extensional equality implies equality. *)

Lemma open_interval_ext_eq: forall lb1 lb2 ub1 ub2, lb1 < ub1 ->
  (forall x, open_interval lb1 ub1 x <-> open_interval lb2 ub2 x) ->
  lb1 = lb2 /\ ub1 = ub2.
Proof.
intros lb1 lb2 ub1 ub2 Hord Hext.
 assert (Hord': lb2 < ub2) by (transitivity (middle lb1 ub1) ;
  apply Hext, middle_is_in_the_middle ; assumption).
 destruct (Rlt_le_dec lb1 lb2).
  destruct (Rlt_le_dec ub1 lb2).
   assert (Hf: ~ open_interval lb2 ub2 (middle lb1 ub1)).
    intro Hf ; apply Rlt_irrefl with lb2 ; transitivity (middle lb1 ub1) ;
    [apply Hf | transitivity ub1 ; [apply middle_is_in_the_middle |]] ;
    assumption.
   apply False_ind, Hf, Hext, middle_is_in_the_middle ; assumption.
   assert (Hf: ~ open_interval lb2 ub2 (middle lb1 lb2)).
    intro Hf ; apply Rlt_irrefl with (middle lb1 lb2) ; transitivity lb2 ;
    [apply middle_is_in_the_middle | apply Hf] ; assumption.
   apply False_ind, Hf, Hext ; split ; [| apply Rlt_le_trans with lb2] ;
   trivial ; apply middle_is_in_the_middle ; assumption.
  destruct (Rlt_le_dec lb2 lb1).
   destruct (Rlt_le_dec lb1 ub2).
    assert (Hf: ~ open_interval lb1 ub1 (middle lb2 lb1)).
     intro Hf ; apply Rlt_irrefl with lb1 ; transitivity (middle lb2 lb1) ;
     [apply Hf | apply middle_is_in_the_middle] ; assumption.
    apply False_ind, Hf, Hext ; split ; [| transitivity lb1] ; auto ;
    apply middle_is_in_the_middle ; assumption.
    assert (Hf: ~ open_interval lb2 ub2 (middle lb1 ub1)).
     intro Hf ; apply False_ind, Rlt_irrefl with ub2, Rle_lt_trans with lb1 ;
     [| transitivity (middle lb1 ub1) ; [apply middle_is_in_the_middle | apply Hf]] ;
     assumption.
    apply False_ind, Hf, Hext, middle_is_in_the_middle ; assumption.
   assert (lb_eq: lb1 = lb2) by intuition ; split ; trivial.
  destruct (Rlt_le_dec ub1 ub2).
   assert (Hf: ~ open_interval lb1 ub1 (middle ub1 ub2)).
    intro Hf ; apply Rlt_irrefl with ub1 ; transitivity (middle ub1 ub2) ;
    [apply middle_is_in_the_middle | apply Hf] ; assumption.
   apply False_ind, Hf, Hext ; rewrite <- lb_eq ; split ; [transitivity ub1 |] ;
   auto ; apply middle_is_in_the_middle ; assumption.
  destruct (Rlt_le_dec ub2 ub1).
   assert (Hf: ~ open_interval lb2 ub2 (middle ub2 ub1)).
    intro Hf ; apply Rlt_irrefl with ub2 ; transitivity (middle ub2 ub1) ;
    [apply middle_is_in_the_middle | apply Hf] ; assumption.
   apply False_ind, Hf, Hext ; rewrite lb_eq ; split ; [transitivity ub2 |] ;
   auto ; apply middle_is_in_the_middle ; assumption.
  intuition.
Qed.

(** open interval are included into interval *)

Lemma included_open_interval_interval : forall a b,
  included (open_interval a b) (interval a b).
Proof.
intros a b x [x_l x_r] ; split ; left ; assumption.
Qed.

(** [Rball] describes intervals. *)

Lemma included_Rball_open_interval : forall c r,
  included (Rball c r) (open_interval (c - r) (c + r)).
Proof.
intros c r x H ; assert (H' := Rabs_def2 _ _ H) ;
 destruct H' ; split ; lra.
Qed.

Lemma included_Rball_open_interval2 : forall lb ub,
  included (Rball (middle lb ub) (interval_size lb ub)) (open_interval lb ub).
Proof.
intros lb ub x x_in ; destruct (Rabs_def2 _ _ x_in) as [x_lb x_ub] ; split.
 apply Rle_lt_trans with (middle lb ub - interval_size lb ub).
  right ; unfold middle, interval_size ; field.
  lra.
 apply Rlt_le_trans with (middle lb ub + interval_size lb ub).
  lra.
  right ; unfold middle, interval_size ; field.
Qed.

Lemma included_open_interval_Rball : forall lb ub,
  included (open_interval lb ub) (Rball (middle lb ub) (interval_size lb ub)).
Proof.
intros lb ub x x_in ; apply Rabs_def1.
 apply Rlt_minus_sort, Rlt_le_trans with ub.
  apply x_in.
  unfold middle, interval_size ; right ; field.
 apply Rlt_minus_sort2, Rle_lt_trans with lb.
  unfold middle, interval_size ; right ; field.
  apply x_in.
Qed.

Lemma included_open_interval_Rball2 : forall c r,
  included (open_interval (c - r) (c + r)) (Rball c r).
Proof.
intros c r x [x_lb x_ub] ; apply Rabs_def1 ; lra.
Qed.

Lemma Rball_rewrite: forall c r x,
  Rball c r x <-> open_interval (c - r) (c + r) x.
Proof.
intros ; split ; [apply included_Rball_open_interval | apply included_open_interval_Rball2].
Qed.

Lemma Rball_rewrite2: forall lb ub x,
  Rball (middle lb ub) (interval_size lb ub) x <-> open_interval lb ub x.
Proof.
intros ; split ; [apply included_Rball_open_interval2 | apply included_open_interval_Rball].
Qed.

(** Inclusion of [Rball]s. *)

Lemma Rball_included: forall c r1 r2 x,
  r1 <= r2 -> Rball c r1 x -> Rball c r2 x.
Proof.
unfold Rball ; intros ; lra.
Qed.

(** The specific case where the center of the ball is 0. *)

Lemma Rball_0_simpl: forall r x,
  Rball 0 r x <-> Rabs x < r.
Proof.
intros ; unfold Rball ; rewrite Rminus_0_r ; split ; trivial.
Qed.

Lemma Rball_c_0_empty: forall c r x, r <= 0 ->
  ~ Rball c r x.
Proof.
intros c r x Hr Hf ; eapply (Rlt_irrefl 0).
 eapply Rle_lt_trans ; [eapply Rabs_pos |].
 eapply Rlt_le_trans ; [eapply Hf | eassumption].
Qed.

(** Decidability result. *)

Lemma in_Rball_dec: forall c r x,
  { Rball c r x } + { ~ Rball c r x }.
Proof.
intros c r x ;
 destruct (in_open_interval_dec (c - r) (c + r) x) as [Ht | Hf].
  left ; rewrite Rball_rewrite ; assumption.
  right ; intro ; eapply Hf ; rewrite <- Rball_rewrite ; eassumption.
Qed.

(** Extensional equality implies equality. *)

Lemma Rball_ext_eq: forall c1 c2 r1 r2, r1 > 0 ->
  (forall x, Rball c1 r1 x <-> Rball c2 r2 x) ->
  c1 = c2 /\ r1 = r2.
Proof.
intros c1 c2 r1 r2 r1_pos Hext.
 assert (Hord: c1 - r1 < c1 + r1) by lra.
 assert (Heq: c1 - r1 = c2 - r2 /\ c1 + r1 = c2 + r2).
  apply open_interval_ext_eq.
   assumption.
   intro x ; split ; intro H ; eapply included_Rball_open_interval,
   Hext, included_open_interval_Rball2 ; assumption.
 split.
  replace c1 with ((c1 - r1 + (c1 + r1)) / 2) by field ;
  replace c2 with ((c2 - r2 + (c2 + r2)) / 2) by field ;
  destruct Heq as [H1 H2] ; rewrite H1, H2 ; field.
  replace r1 with ((c1 + r1 - (c1 - r1)) / 2) by field ;
  replace r2 with ((c2 + r2 - (c2 - r2)) / 2) by field ;
  destruct Heq as [H1 H2] ; rewrite H1, H2 ; field.
Qed.

(** * dist properties *)

Lemma open_interval_dist_pos: forall lb ub x,
  open_interval lb ub x ->
  0 < interval_dist lb ub x.
Proof.
intros lb ub x [x_lb x_ub] ;
 apply Rmin_pos_lt ; lra.
Qed.

Lemma interval_dist_pos: forall lb ub x,
  interval lb ub x -> 0 <= interval_dist lb ub x.
Proof.
intros lb ub x [x_lb x_ub] ; apply Rmin_pos ; lra.
Qed.

Lemma open_interval_dist_bound:
  forall lb ub x, interval lb ub x ->
  forall h, Rabs h < interval_dist lb ub x ->
  open_interval lb ub (x + h).
Proof.
intros lb ub x x_in h h_bd ;
 assert (H := Rabs_def2 _ _ h_bd) ;
 destruct H as [x_lb x_ub].
  assert (H1: - (x - lb) < h).
   apply Rle_lt_trans with (- Rmin (x - lb) (ub - x)).
    apply Ropp_le_contravar, Rmin_l.
    assumption.
  assert (H2: h < ub - x).
   apply Rlt_le_trans with (Rmin (x - lb) (ub - x)).
    assumption.
    apply Rmin_r.
  split ; clear -H1 H2 ; lra.
Qed.

(* TODO : move *)

Lemma Ropp_eq_compat_l : forall x y, - x = y -> x = - y.
Proof.
intros x y [] ; symmetry ; apply Ropp_involutive.
Qed.

Lemma interval_dist_bound:
  forall lb ub x : R, interval lb ub x ->
  forall h : R,
  Rabs h <= interval_dist lb ub x -> interval lb ub (x + h).
Proof.
intros lb ub x x_in h [h_bd | heq].
 apply open_interval_interval, open_interval_dist_bound ;
  assumption.
 unfold Rabs in heq ; destruct (Rcase_abs h).
  split ; rewrite (Ropp_eq_compat_l _ _ heq).
   transitivity (x + - (x - lb)) ; [right ; ring |] ;
   apply Rplus_le_compat_l, Ropp_le_contravar, Rmin_l.
   transitivity (ub + - (interval_dist lb ub x)).
    apply Rplus_le_compat_r, x_in.
    transitivity (ub + - 0) ; [| right ; ring].
    apply Rplus_le_compat_l, Ropp_le_contravar,
     interval_dist_pos ; assumption.
  split ; subst.
   transitivity (x + 0) ; [ring_simplify ; apply x_in |].
    apply Rplus_le_compat_l, interval_dist_pos ; assumption.
   transitivity (x + (ub - x)) ; [| right ; ring].
    apply Rplus_le_compat_l, Rmin_r.
Qed.

Lemma Rball_dist_pos: forall c r x,
  Rball c r x -> 0 < Rball_dist c r x.
Proof.
intros ; eapply open_interval_dist_pos, included_Rball_open_interval ;
 eassumption.
Qed.

Lemma Rball_dist_bound: forall c r x,
  Rball c r x -> forall h, Rabs h < Rball_dist c r x ->
  Rball c r (x + h).
Proof.
intros ; apply included_open_interval_Rball2, open_interval_dist_bound.
 eapply open_interval_interval, included_Rball_open_interval ; eassumption.
 assumption.
Qed.

author: coq-community

repo: coqtail-math


text:
Set Warnings "-notation-overridden".

Require Import Category.Lib.
Require Export Category.Theory.Category.
Require Export Category.Theory.Functor.

Generalizable All Variables.
Set Primitive Projections.
Set Universe Polymorphism.
Set Transparent Obligations.

Section Binoidal.

Context {C : Category}.

Reserved Infix "⋉" (at level 15, right associativity).
Reserved Infix "⋊" (at level 15, right associativity).
Reserved Infix "⊗" (at level 30, right associativity).

(* This is effectively "premagmoidal" with separate functoriality in the two
   arguments to the tensor. *)
Class Binoidal := {
  tensor (x y : C) : C where "x ⊗ y" := (tensor x y);

  (* The binoidal tensor is functorial in each argument separately, whereas
     monoidal categories, whose tensor is a functor from C ∏ C ⟶ C, is
     functorial in both arguments jointly. *)
  left_functor y' : AFunctor (λ x, x ⊗ y');
  inj_left (y' : C) : C ⟶ C := FromAFunctor (left_functor y')
    where "x ⋊ y" := (inj_left x y);

  right_functor x' : AFunctor (λ y, x' ⊗ y);
  inj_right (x' : C) : C ⟶ C := FromAFunctor (right_functor x')
    where "x ⋉ y" := (inj_right x y);
}.

Context `{Binoidal}.

Notation "x ⋉ y" := (inj_left x y) (at level 15, right associativity).
Notation "x ⋊ y" := (inj_right x y) (at level 15, right associativity).
Notation "x ⊗ y" := (tensor x y) (at level 30, right associativity).

Corollary inj_left_right {x y} : x ⋉ y = y ⋊ x.
Proof. reflexivity. Qed.

(* A morphism f:x→y in a binoidal category is central if, for every morphism
   f′:x′→y′, the following diagrams commute. *)

Definition central `(f : x ~> y) : Type :=
  ∀ x' y' (f' : x' ~> y'),
    (fmap[inj_left y'] f ∘ fmap[inj_right x] f'
       << x ⊗ x' ~~> y ⊗ y' >>
     fmap[inj_right y] f' ∘ fmap[inj_left x'] f)
  ∧ (fmap[inj_left y] f' ∘ fmap[inj_right x'] f
       << x' ⊗ x ~~> y' ⊗ y >>
     fmap[inj_right y'] f ∘ fmap[inj_left x] f').

Definition composite_ff' {x x' y y'} (f : x ~> y) (f' : x' ~> y') :
  x ⊗ x' ~> y ⊗ y' := fmap[inj_right y] f' ∘ fmap[inj_left x'] f.

#[export]
Program Instance composite_ff'_respects {x x' y y'} :
  Proper (equiv ==> equiv ==> equiv) (@composite_ff' x x' y y').
Next Obligation.
  unfold composite_ff'.
  proper.
  destruct H.
  simpl in *.
  destruct left_functor0, right_functor0; simpl in *.
  now rewrite X, X0.
Qed.

Definition composite_f'f {x x' y y'} (f' : x' ~> y') (f : x ~> y) :
  x' ⊗ x ~> y' ⊗ y := fmap[inj_right y'] f ∘ fmap[inj_left x] f'.

#[export]
Program Instance composite_f'f_respects {x x' y y'} :
  Proper (equiv ==> equiv ==> equiv) (@composite_f'f x x' y y').
Next Obligation.
  unfold composite_f'f.
  proper.
  destruct H.
  simpl in *.
  destruct left_functor0, right_functor0; simpl in *.
  now rewrite X, X0.
Qed.

End Binoidal.

Notation "x ⋉ y" := (@inj_left _ _ y x)
  (at level 15, right associativity) : object_scope.
Notation "x ⋊ y" := (@inj_right _ _ x y)
  (at level 15, right associativity) : object_scope.

Notation "f ⋉ y" := (fmap[@inj_left _ _ y] f)
  (at level 15, right associativity) : morphism_scope.
Notation "x ⋊ f" := (fmap[@inj_right _ _ x] f)
  (at level 15, right associativity) : object_scope.

Notation "(⊗)" := (@tensor _ _) : functor_scope.
Notation "x ⊗ y" := (@tensor _ _ x%object y%object)
  (at level 30, right associativity) : object_scope.
Notation "f ⊗ g" := (composite_ff' f g)
  (at level 30, right associativity) : morphism_scope.

author: jwiegley

repo: category-theory


text:
Require Import Coq.Lists.ListDec Decidable.

From sflib Require Import sflib.
From Paco Require Import paco.

From PromisingLib Require Import Axioms.
From PromisingLib Require Import Basic.
From PromisingLib Require Import DataStructure.
From PromisingLib Require Import DenseOrder.
From PromisingLib Require Import Loc.
From PromisingLib Require Import Language.

Require Import Event.
Require Import Time.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import MemoryFacts.
Require Import TView.
Require Import Local.
Require Import Thread.

Set Implicit Arguments.

Module LowerPromises.
  Inductive message_rel: forall (msg1 msg2: Message.t), Prop :=
  | message_rel_concrete
      val released:
      message_rel (Message.concrete val released) (Message.concrete val None)
  | message_rel_reserve:
      message_rel Message.reserve Message.reserve
  .
  Hint Constructors message_rel.

  Inductive promises_rel (promises1 promises2: Memory.t): Prop :=
  | promises_rel_intro
      (SOUND: forall loc from to msg1
                (GET1: Memory.get loc to promises1 = Some (from, msg1)),
          exists msg2,
            <<GET2: Memory.get loc to promises2 = Some (from, msg2)>>)
      (COMPLETE: forall loc from to msg2
                   (GET2: Memory.get loc to promises2 = Some (from, msg2)),
          exists msg1,
            <<GET1: Memory.get loc to promises1 = Some (from, msg1)>> /\
            <<MSG: message_rel msg1 msg2>>)
  .

  Inductive promises_rel_aux (dom: list (Loc.t * Time.t)) (promises1 promises2: Memory.t): Prop :=
  | promises_rel_aux_intro
      (SOUND: forall loc from to msg1
                (GET1: Memory.get loc to promises1 = Some (from, msg1)),
          exists msg2,
            <<GET2: Memory.get loc to promises2 = Some (from, msg2)>>)
      (COMPLETE1: forall loc from to msg2
                    (IN: List.In (loc, to) dom)
                    (GET2: Memory.get loc to promises2 = Some (from, msg2)),
          <<GET1: Memory.get loc to promises1 = Some (from, msg2)>>)
      (COMPLETE2: forall loc from to msg2
                    (IN: ~ List.In (loc, to) dom)
                    (GET2: Memory.get loc to promises2 = Some (from, msg2)),
          exists msg1,
            <<GET1: Memory.get loc to promises1 = Some (from, msg1)>> /\
            <<MSG: message_rel msg1 msg2>>)
  .

  Lemma promises_rel_aux_exists
        promises
        (FINITE: Memory.finite promises):
    exists dom, promises_rel_aux dom promises promises.
  Proof.
    inv FINITE. exists x. econs; i; eauto.
    exploit H; eauto. ss.
  Qed.

  Lemma promises_rel_aux_nil
        promises1 promises2
        (REL: promises_rel_aux [] promises1 promises2):
    promises_rel promises1 promises2.
  Proof.
    inv REL. econs; i; eauto.
  Qed.

  Lemma promises_rel_trans
        dom promises1 promises2 promises3
        (REL1: promises_rel_aux dom promises1 promises2)
        (REL2: promises_rel promises2 promises3):
    promises_rel promises1 promises3.
  Proof.
    inv REL1. inv REL2. econs; i.
    - exploit SOUND; eauto. i. des; eauto.
    - exploit COMPLETE; eauto. i. des.
      destruct (In_decidable loc_time_decidable (loc, to) dom); eauto.
      exploit COMPLETE2; eauto. i. des.
      inv MSG; inv MSG0; eauto.
  Qed.

  Lemma promises_rel_nonsynch
        promises1 promises2
        (REL: promises_rel promises1 promises2):
    Memory.nonsynch promises2.
  Proof.
    inv REL. ii.
    exploit COMPLETE; eauto. i. des. inv MSG; ss.
  Qed.

  Lemma promises_rel_aux_lower
        promises1 loc to dom
        (BOT: Memory.bot_none promises1)
        (REL: promises_rel_aux ((loc, to)::dom) promises1 promises1):
    <<REL1: promises_rel_aux dom promises1 promises1>> \/
    exists promises2 from val released,
      <<LOWER: Memory.lower promises1 loc from to (Message.concrete val released) (Message.concrete val None) promises2>> /\
      <<REL: promises_rel_aux dom promises1 promises2>> /\
      <<REL2: promises_rel_aux dom promises2 promises2>>.
  Proof.
    inv REL.
    destruct (Memory.get loc to promises1) as [[from msg1]|] eqn:GET1; cycle 1.
    { left. econs; i; eauto.
      exploit COMPLETE2; eauto. ii. inv H; ss.
      inv H0. congr.
    }
    destruct (In_decidable loc_time_decidable (loc, to) dom).
    { left. econs; i; eauto.
      exploit COMPLETE2; eauto. ii. inv H0; ss.
      inv H1. ss.
    }
    destruct msg1 as [val released|]; cycle 1.
    { left. econs; i; eauto.
      destruct (loc_ts_eq_dec (loc, to) (loc0, to0)).
      - ss. des. subst.
        rewrite GET1 in *. inv GET2.
        esplits; eauto.
      - ss. exploit COMPLETE2; eauto. ii. inv H0; ss.
        inv H1. des; ss.
    }
    right.
    exploit (@Memory.lower_exists promises1 loc from to (Message.concrete val released)
                                  (Message.concrete val None)); eauto.
    { exploit Memory.get_ts; eauto. i. des; ss.
      subst. rewrite BOT in GET1. ss. }
    { econs. ss. }
    i. des.
    esplits; eauto.
    - econs; i.
      + erewrite Memory.lower_o; eauto. condtac; ss; eauto.
        des. subst. rewrite GET1 in *. inv GET0. eauto.
      + revert GET2.
        erewrite Memory.lower_o; eauto. condtac; ss; eauto.
        des. subst. congr.
      + revert GET2.
        erewrite Memory.lower_o; eauto. condtac; ss; i.
        * des. subst. inv GET2. esplits; eauto.
        * guardH o.
          exploit COMPLETE2; eauto. ii. des; ss.
          inv H0. unguard. des; ss.
    - econs; i; eauto.
      revert GET2.
      erewrite Memory.lower_o; eauto. condtac; ss; i.
      + des. subst. inv GET2. esplits; eauto.
      + guardH o.
        exploit COMPLETE2; eauto. ii. inv H0; ss.
        inv H1. unguard. des; ss.
  Qed.

  Lemma steps_promises_rel
        lang e1
        (WF1: Local.wf (Thread.local e1) (Thread.memory e1))
        (SC1: Memory.closed_timemap (Thread.sc e1) (Thread.memory e1))
        (CLOSED1: Memory.closed (Thread.memory e1)):
    exists e2,
      <<STEPS: rtc (union (@Thread.opt_promise_step lang)) e1 e2>> /\
      <<REL: promises_rel (Local.promises (Thread.local e1)) (Local.promises (Thread.local e2))>>.
  Proof.
    exploit promises_rel_aux_exists; try eapply WF1. i. des.
    revert e1 WF1 SC1 CLOSED1 x0.
    induction dom; i.
    { esplits; eauto. apply promises_rel_aux_nil; ss. }
    destruct a as [loc to].
    exploit promises_rel_aux_lower; try exact x0; try apply WF1. i. des; eauto.
    exploit Memory.lower_exists_le; try eapply WF1; eauto. i. des.
    cut (exists pf e e2,
            <<STEP: Thread.promise_step pf e e1 e2>> /\
            <<REL: promises_rel_aux dom (Local.promises (Thread.local e1)) (Local.promises (Thread.local e2))>> /\
            <<REL: promises_rel_aux dom (Local.promises (Thread.local e2)) (Local.promises (Thread.local e2))>>).
    { i. des.
      exploit Thread.step_future; eauto.
      { econs; eauto. }
      i. des.
      exploit IHdom; eauto. i. des.
      esplits.
      - econs 2; try exact STEPS. econs. econs. eauto.
      - eapply promises_rel_trans; eauto.
    }
    destruct e1. ss.
    esplits.
    - econs; eauto. econs.
      + econs 3; eauto. econs. ss.
        unfold TimeMap.bot. apply Time.bot_spec.
      + econs. ss.
      + eauto.
    - ss.
    - ss.
  Qed.

  Lemma rtc_opt_promise_step_future
        lang e1 e2
        (STEPS: rtc (union (@Thread.opt_promise_step lang)) e1 e2):
    <<STEPS: rtc (@Thread.tau_step lang) e1 e2>> /\
    <<STATE: (Thread.state e1) = (Thread.state e2)>> /\
    <<TVIEW: (Local.tview (Thread.local e1)) = (Local.tview (Thread.local e2))>>.
  Proof.
    induction STEPS; try by (splits; eauto). des.
    inv H. inv USTEP; eauto. splits.
    - econs 2; [|eauto].
      econs; [econs; econs; eauto|].
      inv STEP. ss.
    - rewrite <- STATE. inv STEP. ss.
    - rewrite <- TVIEW. inv STEP. inv LOCAL. ss.
  Qed.

  Lemma promises_rel_promise_consistent
        lc1 lc2
        (TVIEW: (Local.tview lc1) = (Local.tview lc2))
        (REL: promises_rel (Local.promises lc1) (Local.promises lc2))
        (CONS: Local.promise_consistent lc1):
    Local.promise_consistent lc2.
  Proof.
    inv REL. ii. rewrite <- TVIEW.
    exploit COMPLETE; eauto. i. des. inv MSG.
    eapply CONS; eauto.
  Qed.
End LowerPromises.

author: snu-sf

repo: promising-ldrf-coq


text:
Require Import Ascii String.
From mathcomp.algebra Require Import ssrint.

Extract Inductive ascii => char
        [
          "(* If this appears, you're using Ascii internals. Please don't *) (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> let f b i = if b then 1 lsl i else 0 in Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))"
        ]
        "(* If this appears, you're using Ascii internals. Please don't *) (fun f c -> let n = Char.code c in let h i = (n land (1 lsl i)) <> 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
Extract Constant zero => "'\000'".
Extract Constant one => "'\001'".
Extract Constant shift =>
        "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
Extract Inlined Constant ascii_dec =>  "(=)".

Extract Inductive nat => "int"
        [ "0" "(fun x -> x + 1)" ]
          "(fun zero succ n ->
      if n=0 then zero () else succ (n-1))".

Extract Inductive int => "int"
                           [ "(fun x-> x)" "(fun x-> (0-x))" ]  "(fun zero succ n ->
      if n=0 then zero () else succ (n-1))".

author: sayon

repo: mini-c

save_path: github-repos/coq/sayon-mini-c


text:
(******************************************************************************)
(* Copyright (c) 2018 Yatin Manerkar (Princeton Uni.) & Daniel Lustig (NVIDIA)*)
(*                                                                            *)
(* Permission is hereby granted, free of charge, to any person obtaining a    *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation  *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense,   *)
(* and/or sell copies of the Software, and to permit persons to whom the      *)
(* Software is furnished to do so, subject to the following conditions:       *)
(*                                                                            *)
(* The above copyright notice and this permission notice shall be included in *)
(* all copies or substantial portions of the Software.                        *)
(*                                                                            *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,   *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL    *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING    *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER        *)
(* DEALINGS IN THE SOFTWARE.                                                  *)
(******************************************************************************)

Require Import List.
Require Import Arith.
Require Import String.
Require Import Ascii.

Import ListNotations.
Open Scope string_scope.

Definition tab := String (ascii_of_nat 9) "".
Definition newline := String (ascii_of_nat 10) "".
Definition quote := String (ascii_of_nat 34) "".

Definition stringOfNat (n : nat) : string :=
  (* Anything larger than 9 will be handled by OCaml's string_of_int during
   * extraction.  We don't need to worry about it here within Coq, it's
   * strictly cosmetic. *)
  String (ascii_of_nat (nat_of_ascii "0" + n)) "".

Definition StringOf
  (l : list string)
  : string :=
  fold_left append l "".

Fixpoint beq_string
  (s1 s2 : string)
  : bool :=
  match (s1, s2) with
  | (String h1 t1, String h2 t2) =>
      if beq_nat (nat_of_ascii h1) (nat_of_ascii h2)
      then beq_string t1 t2
      else false
  | (EmptyString, EmptyString) => true
  | _ => false
  end.

Fixpoint string_prefix
  (s1 s2 : string)
  : bool :=
  match (s1, s2) with
  | (String h1 t1, String h2 t2) =>
      if beq_nat (nat_of_ascii h1) (nat_of_ascii h2)
      then string_prefix t1 t2
      else false
  | (EmptyString, _) => true
  | _ => false
  end.

Fixpoint substr
  (n : nat)
  (s : string)
  : string :=
  match (s, n) with
  | (_, 0) => s
  | (EmptyString, S _) => ""
  | (String _ s', S n') => substr n' s'
  end.

Fixpoint find_string
  (s : string)
  (l : list string)
  : bool :=
  match l with
  | [] => false
  | h::t =>
    if beq_string s h
    then true
    else find_string s t
  end.

author: ymanerka

repo: pipeproof

save_path: github-repos/coq/ymanerka-pipeproof


text:
(************************************************************
* Lambda-calculus with references,                          *
* Interpreter in pretty-big-step semantics                  *
*************************************************************)

Set Implicit Arguments.
Require Import LambdaRef.

Implicit Types v : val.
Implicit Types t : trm.
Implicit Types c : ctx.
Implicit Types m : mem.

(************************************************************)
(* * Definitions *)

(** Definition of behaviors *)

Inductive beh :=
  | beh_ret : val -> beh.

Coercion beh_ret : val >-> beh.
Implicit Types b : beh.

(** Outcome of an evaluation *)

Inductive out :=
  | out_ter : mem -> beh -> out
  | out_div : out.

Implicit Types o : out.

(** Grammar of extended terms *)

Inductive ext : Type :=
  | ext_trm : trm -> ext
  | ext_app_1 : out -> trm -> ext
  | ext_app_2 : val -> out -> ext
  | ext_new_1 : out -> ext
  | ext_get_1 : out -> ext
  | ext_set_1 : out -> trm -> ext
  | ext_set_2 : val -> out -> ext.

Coercion ext_trm : trm >-> ext.
Implicit Types e : ext.

(** Generation of fresh names *)

Parameter fresh_for : mem -> loc.
Parameter fresh_for_spec : forall m,
  ~ Heap.indom m (fresh_for m).

(** Semantics (without error rules for the time being) *)

Inductive red : mem -> ctx -> ext -> out -> Prop :=
  | red_val : forall m c v,
      red m c v (out_ter m v)
  | red_var : forall m c x v,
      LibEnv.binds x v c ->
      red m c (trm_var x) (out_ter m v)
  | red_abs : forall m c x t,
      red m c (trm_abs x t) (out_ter m (val_clo c x t))
  | red_app : forall o1 o m c t1 t2,
      red m c t1 o1 ->
      red m c (ext_app_1 o1 t2) o ->
      red m c (trm_app t1 t2) o
  | red_app_1 : forall o2 o m m0 c v1 t2,
      red m c t2 o2 ->
      red m c (ext_app_2 v1 o2) o ->
      red m0 c (ext_app_1 (out_ter m v1) t2) o
  | red_app_2 : forall o m c m0 c0 v2 x t3,
      red m (c & x ~~ v2) t3 o ->
      red m0 c0 (ext_app_2 (val_clo c x t3) (out_ter m v2)) o
  | red_new : forall o1 o m c t1,
      red m c t1 o1 ->
      red m c (ext_new_1 o1) o ->
      red m c (trm_new t1) o
  | red_new_1 : forall l m' m m0 c v,
      l = fresh_for m ->
      m' = Heap.write m l v ->
      red m0 c (ext_new_1 (out_ter m v)) (out_ter m' (val_loc l))
  | red_get : forall o1 o m c t1,
      red m c t1 o1 ->
      red m c (ext_get_1 o1) o ->
      red m c (trm_get t1) o
  | red_get_1 : forall l m c m0 v,
      Heap.binds m l v ->
      red m0 c (ext_get_1 (out_ter m (val_loc l))) (out_ter m v)
  | red_set : forall o1 o m c t1 t2,
      red m c t1 o1 ->
      red m c (ext_set_1 o1 t2) o ->
      red m c (trm_set t1 t2) o
  | red_set_1 : forall o2 o m c m0 v1 t2,
      red m c t2 o2 ->
      red m c (ext_set_2 v1 o2) o ->
      red m0 c (ext_set_1 (out_ter m v1) t2) o
  | red_set_2 : forall l m' m c m0 v,
      Heap.indom m l ->
      m' = Heap.write m l v ->
      red m0 c (ext_set_2 (val_loc l) (out_ter m v)) (out_ter m' v).

(************************************************************)
(* * Induction principle on the height of a derivation *)

(** Ideally, this section would be automatically generated by Coq *)

Section BigredInd.

Inductive redh : nat -> mem -> ctx -> ext -> out -> Prop :=
  | redh_val : forall n m c v,
      redh (S n) m c v (out_ter m v)
  | redh_var : forall n m c x v,
      LibEnv.binds x v c ->
      redh (S n) m c (trm_var x) (out_ter m v)
  | redh_abs : forall n m c x t,
      redh (S n) m c (trm_abs x t) (out_ter m (val_clo c x t))
  | redh_app : forall n o1 o m c t1 t2,
      redh n m c t1 o1 ->
      redh n m c (ext_app_1 o1 t2) o ->
      redh (S n) m c (trm_app t1 t2) o
  | redh_app_1 : forall n o2 o m m0 c v1 t2,
      redh n m c t2 o2 ->
      redh n m c (ext_app_2 v1 o2) o ->
      redh (S n) m0 c (ext_app_1 (out_ter m v1) t2) o
  | redh_app_2 : forall n o m c m0 c0 v2 x t3,
      redh n m (c & x ~~ v2) t3 o ->
      redh (S n) m0 c0 (ext_app_2 (val_clo c x t3) (out_ter m v2)) o
  | redh_new : forall n o1 o m c t1,
      redh n m c t1 o1 ->
      redh n m c (ext_new_1 o1) o ->
      redh (S n) m c (trm_new t1) o
  | redh_new_1 : forall n l m' m c m0 v,
      l = fresh_for m ->
      m' = Heap.write m l v ->
      redh (S n) m0 c (ext_new_1 (out_ter m v)) (out_ter m' (val_loc l))
  | redh_get : forall n o1 o m c t1,
      redh n m c t1 o1 ->
      redh n m c (ext_get_1 o1) o ->
      redh (S n) m c (trm_get t1) o
  | redh_get_1 : forall n l m c m0 v,
      Heap.binds m l v ->
      redh (S n) m0 c (ext_get_1 (out_ter m (val_loc l))) (out_ter m v)
  | redh_set : forall n o1 o m c t1 t2,
      redh n m c t1 o1 ->
      redh n m c (ext_set_1 o1 t2) o ->
      redh (S n) m c (trm_set t1 t2) o
  | redh_set_1 : forall n o2 o m c m0 v1 t2,
      redh n m c t2 o2 ->
      redh n m c (ext_set_2 v1 o2) o ->
      redh (S n) m0 c (ext_set_1 (out_ter m v1) t2) o
  | redh_set_2 : forall n l m' m c m0 v,
      Heap.indom m l ->
      m' = Heap.write m l v ->
      redh (S n) m0 c (ext_set_2 (val_loc l) (out_ter m v)) (out_ter m' v).

Hint Constructors red redh.
Hint Extern 1 (_ < _) => math.

Lemma redh_lt : forall n n' m c e o,
  redh n m c e o -> n < n' -> redh n' m c e o.
Proof.
  introv H. gen n'. induction H; introv L;
   (destruct n' as [|n']; [ false; math | autos* ]).
Qed.

Lemma red_redh : forall m c e o,
  red m c e o -> exists n, redh n m c e o.
Proof. hint redh_lt. introv H. induction H; try induct_height. Qed.

End BigredInd.

(************************************************************)
(* * Facts *)

Hint Constructors red.

Instance val_Inhab : Inhab val.
Proof. apply (Inhab_of_val (val_int 0)). Qed.

Instance loc_Comparable : Comparable loc.
(*Proof. constructor ; apply eq_nat_dec. Qed.*)

(************************************************************)
(* * Interpreter *)

(** Definition of a result *)

Inductive res :=
  | res_return : mem -> beh -> res
  | res_unspec : res
  | res_bottom : res.

Implicit Types r : res.

(** Bind-style operators *)

Definition if_success (r:res) (k:mem->val->res) : res :=
  match r with
  | res_return m (beh_ret v) => k m v
  | _ => r
  end.

Definition if_isclo (v:val) (k:ctx->var->trm->res) : res :=
  match v with
  | val_clo c x t => k c x t
  | _ => res_unspec
  end.

Definition if_true (i:bool) (k:unit->res) : res :=
  if i then k tt else res_unspec.

Definition if_isloc (v:trm) (k:loc->res) : res :=
  match v with
  | val_loc l => k l
  | _ => res_unspec
  end.

Fixpoint run (n:nat) (m:mem) (c:ctx) (t:trm) : res :=
  match n with
  | O => res_bottom
  | S n' =>
    let run' := run n' in
    let ret := res_return m in
    match t with
    | trm_val v => ret v
    | trm_var x =>
       if_true (decide (x \in EnvOps.dom c)) (fun _ =>
         ret (get_or_arbitrary x c))
    | trm_abs x t1 => ret (val_clo c x t1)
    | trm_app t1 t2 =>
       if_success (run' m c t1) (fun m1 v1 =>
         if_success (run' m1 c t2) (fun m2 v2 =>
           if_isclo v1 (fun c' x t3 =>
             run' m2 (c' & x ~~ v2) t3)))
    | trm_new t1 =>
       if_success (run' m c t1) (fun m1 v1 =>
         let l := fresh_for m1 in
         let m2 := Heap.write m1 l v1 in
         res_return m2 (val_loc l))
    | trm_get t1 =>
       if_success (run' m c t1) (fun m1 v1 =>
         if_isloc v1 (fun l =>
           let v := Heap.read m1 l in
           if_true (decide (indom m1 l)) (fun _ =>
             res_return m1 v)))
    | trm_set t1 t2 =>
       if_success (run' m c t1) (fun m1 v1 =>
         if_success (run' m1 c t2) (fun m2 v2 =>
           if_isloc v1 (fun l =>
             res_return (Heap.write m2 l v2) v2)))
    end
  end.

(************************************************************)
(* * Completeness of the interpreter *)

Hint Extern 1 (_ > _) => abstract math.
Hint Extern 1 (_ < _) => abstract math.

Lemma if_true_elim : forall i P k,
  istrue i = P -> P ->
  (if_true i k) = k tt.
Proof.
  introv H F. unfolds. case_if.
  auto.
  rewrite <- H in F. false.
Qed.

Lemma if_success_elim : forall r k m v,
  r = res_return m (beh_ret v) ->
  if_success r k = k m v.
Proof. introv E ; rewrite* E. Qed.

Lemma redh_not_div : forall n m c e,
  ~redh n m c e out_div.
Proof. intro n ; induction* n ; introv H ; inverts* H. Qed.

Lemma runh_complete_ter : forall n m c t m' v,
  redh n m c t (out_ter m' v) ->
  forall k, k > n ->
    run k m c t = res_return m' v.
Proof.
  induction n using peano_induction.
  introv R L. destruct k. math.
  asserts IH: (
    forall m0 c t m' v n',
    redh n' m0 c t (out_ter m' v) ->
    n' < n ->
    run k m0 c t = res_return m' v).
    intros. applys* H. clear H.
  inverts R as; simpl.
  auto.
  introv B. erewrite if_true_elim; eauto.
   fequals. rewrite~ (binds_get_or_arbitrary B).
   rewrite istrue_decide. applys* get_some_inv.
  auto.
  introv R1 R2. inverts R2 as R2 R3. inverts R3 as R3.
   rewrites~ (>> IH R1). simpl.
   rewrites~ (>> IH R2). simpl.
   applys* IH.
  introv R1 R2. inverts R2 as. rewrites~ (>> IH R1).
  introv R1 R2. inverts R2 as B.
   rewrites~ (>> IH R1). simpl.
   erewrite if_true_elim; eauto.
     fequals_rec. applys (binds_read B).
     rewrite istrue_decide. applys* @LibHeap.binds_indom.
  introv R1 R2. inverts R2 as R2 R3. inverts R3 as R3.
   rewrites~ (>> IH R1). simpl.
   rewrites~ (>> IH R2).
Qed.

Theorem run_complete_ter : forall m c t m' v,
  red m c t (out_ter m' v) ->
  exists n0, forall n, n > n0 ->
    run n m c t = res_return m' v.
Proof.
  introv H. lets (n0&R): red_redh (rm H).
  exists n0. introv L.
  applys~ runh_complete_ter R.
Qed.

author: charguer

repo: formalmetacoq

save_path: github-repos/coq/charguer-formalmetacoq


text:
Require Import Coq.Lists.List.

Ltac caseEq x := generalize (refl_equal x); pattern x at -1; case x; intros.

Definition marked(P:Prop) : Prop := P.

Ltac mark H :=
  let t := type of H in
  let n:= fresh in
    (assert (n:marked t); [exact H | clear H; rename n into H]).

Ltac unmark H := unfold marked in H.

Ltac unmark_all := unfold marked in *|-.

Ltac revert_all H :=
  mark H;
  match goal with
    | H0 : _, H : marked _ |- _ => revert H0; revert_all H
    | _ => idtac
  end;
  unmark_all.

Ltac Prop_Ind1 H A :=
  let HA' := fresh A "'" in
    assert (exists A', A = A') as HA' by eauto; destruct HA';
      revert_all H;
      induction H.

Ltac Prop_Ind2 H A B:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
    let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
      revert_all H;
      induction H.

Ltac Prop_Ind3 H A B C:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
    revert_all H;
    induction H.

Ltac Prop_Ind4 H A B C D:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
  let HD' := fresh D "'" in assert (exists D', D = D') as HD' by eauto; destruct HD';
    revert_all H;
    induction H.

Ltac Prop_Ind5 H A B C D E:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
  let HD' := fresh D "'" in assert (exists D', D = D') as HD' by eauto; destruct HD';
  let HE' := fresh E "'" in assert (exists E', E = E') as HE' by eauto; destruct HE';
    revert_all H;
    induction H.

Ltac Prop_Ind H :=
  match (type of H) with
    | ?P ?A ?B ?C ?D ?E => Prop_Ind5 H A B C D E
    | ?P ?A ?B ?C ?D=> Prop_Ind4 H A B C D
    | ?P ?A ?B ?C => Prop_Ind3 H A B C
    | ?P ?A ?B=> Prop_Ind2 H A B
    | ?P ?A => Prop_Ind1 H A
    | _ => idtac
  end.

Ltac Prop_Ind_test H :=
  match (type of H) with
    | ?P ?A ?B ?C ?D ?E => idtac "PI5"; Prop_Ind5 H A B C D E
    | ?P ?A ?B ?C ?D=> idtac "PI4"; Prop_Ind4 H A B C D
    | ?P ?A ?B ?C => idtac "PI3"; Prop_Ind3 H A B C
    | ?P ?A ?B=> idtac "PI2"; Prop_Ind2 H A B
    | ?P ?A => idtac "PI1"; Prop_Ind1 H A
    | _ => idtac
  end.

Ltac Prop_Destruct1 H A :=
  let HA' := fresh A "'" in
    assert (exists A', A = A') as HA' by eauto; destruct HA';
      revert_all H;
      destruct H.

Ltac Prop_Destruct2 H A B:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
    let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
      revert_all H;
      destruct H.

Ltac Prop_Destruct3 H A B C:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
    revert_all H;
    destruct H.

Ltac Prop_Destruct4 H A B C D:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
  let HD' := fresh D "'" in assert (exists D', D = D') as HD' by eauto; destruct HD';
    revert_all H;
    destruct H.

Ltac Prop_Destruct5 H A B C D E:=
  let HA' := fresh A "'" in assert (exists A', A = A') as HA' by eauto; destruct HA';
  let HB' := fresh B "'" in assert (exists B', B = B') as HB' by eauto; destruct HB';
  let HC' := fresh C "'" in assert (exists C', C = C') as HC' by eauto; destruct HC';
  let HD' := fresh D "'" in assert (exists D', D = D') as HD' by eauto; destruct HD';
  let HE' := fresh E "'" in assert (exists E', E = E') as HE' by eauto; destruct HE';
    revert_all H;
    destruct H.

Ltac Prop_Destruct H :=
  match (type of H) with
    | ?P ?A ?B ?C ?D ?E => Prop_Ind5 H A B C D E
    | ?P ?A ?B ?C ?D=> Prop_Ind4 H A B C D
    | ?P ?A ?B ?C => Prop_Ind3 H A B C
    | ?P ?A ?B=> Prop_Ind2 H A B
    | ?P ?A => Prop_Ind1 H A
    | _ => idtac
  end.

Inductive List_P1 {A : Type} (P : A -> Prop) : list A -> Prop :=
  Cons_a : forall c cs', P c -> List_P1 P cs' -> List_P1 P (c :: cs')
| Nil : List_P1 P nil.

Lemma In_List_P1 : forall A (P : A -> Prop) (As : list A),
  (forall a, In a As -> P a) -> List_P1 P As.
  induction As; intros.
  constructor.
  simpl; constructor.
  apply H; simpl; auto.
  apply IHAs; intros; apply H; simpl; auto.
Qed.

Lemma In_List_P1' : forall A (P : A -> Prop) (As : list A),
  List_P1 P As -> (forall a, In a As -> P a).
  induction As; simpl; intros; inversion H; destruct H0; subst; eauto.
Qed.

(*** Definition List_P1 {A : Type} (as' : list A) (P : A -> Prop) : Prop :=
  forall a n, nth_error as' n = Some a -> P a. ***)

Definition List_P2 {A B : Type} (as' : list A) (bs : list B) (P : A -> B -> Prop) : Prop :=
  (forall a n, nth_error as' n = Some a -> exists b, nth_error bs n = Some b /\ P a b) /\
  (forall n, nth_error as' n = None -> nth_error bs n = None).

Lemma nth_error_nil : forall n A, nth_error nil n = @None A.
  intros; destruct n; simpl; reflexivity.
Qed.

Lemma nth_error_in : forall B (Bs : list B) b n, nth_error Bs n = Some b -> In b Bs.
  induction Bs; intros; destruct n; simpl in *|-*; try discriminate.
  injection H; tauto.
  right; eauto.
Qed.

Lemma nth_error_in' : forall B (Bs : list B) b, In b Bs -> exists n, nth_error Bs n = Some b.
  induction Bs; intros; simpl in *|-*.
  tauto.
  destruct H.
  exists 0; simpl; subst; reflexivity.
  destruct (IHBs _ H) as [n nth_n]; exists (S n); assumption.
Qed.

Lemma List_P2_cons : forall (A B : Type) a as' b bs' (P : A -> B -> Prop),
  List_P2 (a :: as') (b :: bs') P -> P a b /\ List_P2 as' bs' P.
  unfold List_P2; intros until P; intro P2_Cons; destruct P2_Cons as [fnd not_fnd].
  repeat split; intros.
  destruct (fnd _ 0 (refl_equal _)) as [b0 [b0_eq Pab']]; simpl in b0_eq;
    injection b0_eq; intros; subst; assumption.
  eapply (fnd _ (S n) H).
  eapply (not_fnd (S n)); simpl; eauto.
Qed.

Lemma cons_List_P2 : forall (A B : Type) a as' b bs' (P : A -> B -> Prop),
  P a b -> List_P2 as' bs' P -> List_P2 (a :: as') (b :: bs') P.
  unfold List_P2; intros; destruct H0; split; destruct n; simpl; intros.
  injection H2; intros; subst; exists b; split; auto.
  eauto.
  discriminate.
  eauto.
Qed.

Ltac P1_nil H := rewrite nth_error_nil in H; discriminate.

Lemma List_P2_nil : forall (A B : Type) a as' (P : A -> B -> Prop),
  ~ List_P2 (a :: as') nil P.
  unfold List_P2; unfold not; intros until P; intros P2; destruct P2 as [fnd _].
  destruct (fnd _ 0 (refl_equal _)) as [b [Error _]]; discriminate Error.
Qed.

Lemma List_P2_nil' : forall (A B : Type) b bs' (P : A -> B -> Prop),
  ~ List_P2 nil (b :: bs') P.
  unfold List_P2; unfold not; intros until P; intros P2; destruct P2 as [_ not_fnd].
  generalize (not_fnd 0 (refl_equal _)) as Error; intros; discriminate Error.
Qed.

Ltac P2_nil H := try (elimtype False; eapply (List_P2_nil _ _ _ _ _ H); fail); try
  (elimtype False; eapply (List_P2_nil' _ _ _ _ _ H); fail).

Inductive List_P2' {A B : Type} (P : A -> B -> Prop) : list A -> list B -> Prop :=
| nil_P2' : List_P2' P nil nil
| cons_P2' : forall a b As Bs, P a b -> List_P2' P As Bs -> List_P2' P (a :: As) (b :: Bs).

Lemma P2_if_P2' : forall A B (as' : list A) (bs : list B) (P : A -> B -> Prop),
  List_P2 as' bs P -> List_P2' P as' bs.
  induction as'; intros; destruct bs; try P2_nil H; econstructor.
  destruct H as [fnd _].
  destruct (fnd _ 0 (refl_equal _)) as [b0 [b0_eq P_b0]].
  simpl in b0_eq; inversion b0_eq; subst; assumption.
  eapply IHas'.
  destruct (List_P2_cons _ _ _ _ _ _ _ H); assumption.
Qed.

Lemma P2'_if_P2 : forall A B (as' : list A) (bs : list B) (P : A -> B -> Prop),
  List_P2' P as' bs -> List_P2 as' bs P.
  intros; Prop_Ind H; intros.
  clear; unfold List_P2; split; intros.
  destruct n; simpl in H; discriminate.
  destruct n; simpl; reflexivity.
  eapply cons_List_P2; eauto.
Qed.

Lemma nil_List_P2 : forall (A B : Type) (P : A -> B -> Prop),
  List_P2 nil nil P.
  unfold List_P2; intros; split; intros; destruct n; simpl in *|-*; try discriminate; reflexivity.
Qed.

Fixpoint zip {A B C : Type} (As : list A) (Bs : list B) (f : A -> B -> C) : option (list C) :=
  match As, Bs with
    a :: As', b :: Bs' => match zip As' Bs' f with
                            Some Cs => Some ((f a b) :: Cs)
                            | _ => None
                          end
    | nil, nil => Some nil
    | _, _ => None
  end.

Fixpoint opt_map {A B : Type} (As : list A) (f : A -> option B) : option (list B) :=
  match As with
    a :: As' => match (opt_map As' f) with
                  | Some Bs => match f a with
                                 Some b => Some (b :: Bs)
                                 | _ => None
                               end
                  | None => None
                end
    | nil => Some nil
  end.

Fixpoint distinct (A : Type) (l : list A) : Prop :=
  match l with
    nil => True
    | cons a l' => (~ In a l') /\ distinct A l'
  end.

Arguments distinct {A} l.

Lemma nth_error_map : forall A B (f : A -> B) As n a,
  nth_error As n = Some a -> nth_error (map f As) n = Some (f a).
  clear; induction As; destruct n; simpl; intros; try discriminate.
  injection H; intros; subst; reflexivity.
  eauto.
Qed.

Lemma nth_error_map' : forall A B (f : A -> B) As n,
  nth_error As n = None -> nth_error (map f As) n = None.
  clear; induction As; destruct n; simpl; intros; try discriminate; auto.
Qed.

Lemma map_nth_error : forall A B (f : A -> B) As n a,
  nth_error (map f As) n = Some a ->  exists a', nth_error As n = Some a' /\ a = f a'.
  clear; induction As; destruct n; simpl; intros; try discriminate.
  injection H; intros; subst. exists a; split; auto.
  eauto.
Qed.

Lemma map_nth_error' : forall A B (f : A -> B) As n,
  nth_error (map f As) n = None -> nth_error As n = None.
  clear; induction As; destruct n; simpl; intros; try discriminate; auto.
Qed.

  Lemma distinct_sym : forall B (Bs Bs' : list B), distinct (Bs ++ Bs') -> distinct (Bs' ++ Bs).
    clear; induction Bs; simpl.
    intros; rewrite <- app_nil_end; assumption.
    intros Bs' H; destruct H; simpl.
    generalize a Bs (IHBs _  H0) H; clear; induction Bs'.
    simpl; intros; rewrite <- app_nil_end in H0; tauto.
    simpl; intros; destruct H; unfold not; split; intros.
    assert (a = a0).
    generalize Bs' a a0 Bs H H2; clear; induction Bs'; simpl; intros.
    destruct H2; auto; elimtype False; eauto.
    destruct H2.
    elimtype False; eauto.
    assert (~ In a0 (Bs' ++ Bs)) by (unfold not; intros; eauto); eauto.
    subst; eauto.
    apply H0; generalize Bs; clear; induction Bs; simpl; intros; eauto.
    eapply IHBs'; eauto.
    unfold not; intros H2; apply H0; generalize Bs' a a0 H2; clear; induction Bs;
      simpl; intros; try tauto.
    destruct H2; try tauto.
    right; eapply IHBs; assumption.
  Qed.

Inductive id_map_1 {A B : Set} : A -> B -> B -> Prop :=
  idm1 : forall a b, id_map_1 a b b.

Inductive id_map_2 {A B C : Set} : A -> B -> C -> C -> Prop :=
  idm2 : forall a b c, id_map_2 a b c c.

Inductive id_map_3 {A B C D : Set} : A -> B -> C -> D -> D -> Prop :=
  idm3 : forall a b c d, id_map_3 a b c d d.

Inductive id_map_4 {A B C D E : Set} : A -> B -> C -> D -> E -> E -> Prop :=
  idm4 : forall a b c d e, id_map_4 a b c d e e.

Inductive id_map_5 {A B C D E F: Set} : A -> B -> C -> D -> E -> F -> F -> Prop :=
  idm5 : forall a b c d e f, id_map_5 a b c d e f f.

  Lemma length_List_P2' : forall A B (as' : list A) (bs : list B) (P : A -> B -> Prop),
    List_P2' P as' bs -> length as' = length bs.
    induction as'; intros; destruct bs; inversion H; auto.
    simpl; eauto.
  Qed.

  Lemma length_List_P2 : forall A B (as' : list A) (bs : list B) (P : A -> B -> Prop),
    List_P2 as' bs P -> length as' = length bs.
    intros; eapply length_List_P2'; apply P2_if_P2'; eassumption.
  Qed.

  Lemma List_P1_app : forall A (as' as'': list A) (P : A -> Prop),
    List_P1 P as' -> List_P1 P as'' -> List_P1 P (as' ++ as'').
    clear; induction as'; intros; simpl; auto; inversion H; subst;
      constructor; auto.
  Qed.

  Lemma List_P2'_app : forall A B (as' as'': list A) (bs bs': list B) (P : A -> B -> Prop),
    List_P2' P as' bs -> List_P2' P as'' bs' -> List_P2' P (as' ++ as'') (bs ++ bs').
    clear; induction as'; intros; inversion H; subst; simpl; auto;
      constructor; auto.
  Qed.

  Lemma List_P2_app : forall A B (as' as'': list A) (bs bs': list B) (P : A -> B -> Prop),
    List_P2 as' bs P -> List_P2 as'' bs' P -> List_P2 (as' ++ as'') (bs ++ bs') P.
    clear; intros; apply P2_if_P2' in H; apply P2_if_P2' in H0; apply P2'_if_P2; apply List_P2'_app; auto.
  Qed.

author: skeuchel

repo: gdtc

save_path: github-repos/coq/skeuchel-gdtc


text:
Require Import Arith.

Fixpoint sum_odd(n:nat) : nat :=
  match n with
  | O => O
  | S m => 1 + m + m + sum_odd m
  end.

Goal forall n, sum_odd n = n * n.
Proof.
  intros.
  induction n.
    reflexivity.

    simpl.
    rewrite IHn.
    rewrite mult_succ_r.
    rewrite (plus_comm (n * n) n).
    rewrite plus_assoc.
    reflexivity.
Qed.

author: spinylobster


text:
Parameter key: Type.
Parameter bytes: Type.
Parameter hostname: Type.

Parameter process: bytes -> bytes.

Inductive event: Type :=
  | Request: hostname -> hostname -> bytes -> event
  | Response: hostname -> hostname -> bytes -> bytes -> event
  | Corrupted: hostname -> event.

Axiom log: Type.

Definition asn := event -> Prop. (* TODO: should be [log -> Prop] *)

Axiom Level_Low : forall A, A -> asn.
Arguments Level_Low [_] a.

Definition isEvent (e: event): asn :=
  fun e' => e = e'. (* TODO: should be [Logged e] *)

Definition RecvRequest (a b: hostname)(req: bytes): asn :=
  fun e => e = Request a b req \/ e = Corrupted(a) \/ e = Corrupted(b).

Definition RecvResponse (a b: hostname)(req resp: bytes): asn :=
  fun e => e = Response a b req resp \/ e = Corrupted(a) \/ e = Corrupted(b).

Inductive Sig: Type -> Type :=
(* Assertions *)
| Assume: asn -> Sig unit
| Assert: asn -> Sig unit
(* Cryptographic operations *)
| MAC: forall A, key -> A -> Sig bytes
| Verify: forall A, key -> A -> bytes -> Sig unit
| Fresh_key: hostname -> hostname -> Sig key
(* Network I/O *)
| Send: forall A, hostname -> A -> Sig unit
| Receive: forall A, Sig A.

Arguments MAC [_] k a.
Arguments Verify [_] k a b.
Arguments Send [_] h msg.

Inductive M (X: Type) :=
  | ret: X -> M X
  | op: forall O, Sig O -> (O -> M X) -> M X.

Arguments ret [_] v.
Arguments op [_] [_] s k.

Notation "'assume!' a" := (op (Assume a) (@ret _)) (at level 10).
Notation "'assert!' a" := (op (Assert a) (@ret _)) (at level 10).
Notation "'mac!' k m" := (op (MAC k m) (@ret _)) (at level 10, k,m at next level).
Notation "'verify!' k v m" := (op (Verify k v m) (@ret _)) (at level 10, k,v,m at next level).
Notation "'fresh_key!' a b" := (op (Fresh_key a b) (@ret _)) (at level 10, a, b at next level).
Notation "'send!' a m" := (op (Send a m) (@ret _)) (at level 10, a, m at next level).
Notation "'receive!' T" := (op (Receive T) (@ret _)) (at level 10, T at next level).

Fixpoint bind {X Y} (m: M X)(mf: X -> M Y): M Y :=
  match m with
  | ret v => mf v
  | op s k => op s (fun o => bind (k o) mf)
  end.

Notation "'let!' x := c1 'in' c2" := (@bind _ _ c1 (fun x => c2))
    (at level 61, x pattern, c1 at next level, right associativity).

Notation "e1 ;; e2" := (@bind _ _ e1 (fun _ => e2))
    (at level 61, right associativity).

Inductive requestMAC := Req (req: bytes).
Inductive responseMAC := Resp (req: bytes)(resp: bytes).

Definition client (a b: hostname)(k: key)(req: bytes): M unit :=
  assume! (isEvent (Request a b req)) ;;
  let! mac := mac! k (Req req) in
  send! b (req, mac) ;;
  let! (resp, mac) := receive! (bytes * bytes) in
  verify! k (Resp req resp) mac ;;
  assert! (RecvResponse a b req resp).

Definition server (a b: hostname)(k: key): M unit :=
  let! (req, mac) := receive! (bytes * bytes) in
  verify! k (Req req) mac ;;
  assert! (RecvRequest a b req) ;;
  let resp := process req in
  assume! (isEvent (Response a b req resp)) ;;
  let! mac := mac! k (Resp req resp) in
  send! a (resp, mac).

Axiom triple : forall X, asn -> M X -> (X -> asn) -> Prop.

Notation "'{{' P } } e {{ v ; Q } }" := (@triple _ P e (fun v => Q))
      (at level 20, format "'[hv' {{  P  } }  '/  ' e  '/'  {{  v ;  Q  } } ']'").

Parameter spec_triple: forall (P P': asn) X (Q Q': X -> asn) (m: M X),
    triple _ P m Q ->
    (forall e, P' e -> P e) ->
    (forall x e, Q x e -> Q' x e) ->
    triple _ P' m Q'.

Parameter spec_ret: forall X x,
    triple _ (fun _ => True) (@ret X x) (fun x' _ => x = x').
Parameter spec_bind: forall X Y (e1: M X)(e2: X -> M Y) P (Q: X -> asn) R,
    {{ P }} e1 {{ v ; Q v }} ->
    (forall v, triple _ (Q v) (e2 v) R) ->
    (* {{ P }} (let! v := e1 in e2 v) {{ R }} *)
    triple _ P (let! v := e1 in e2 v) R.

Parameter spec_assert: forall P,
  {{ P }} assert! P {{ _ ; fun _ => True }}.
Parameter spec_assume: forall P Q,
  {{ P }} assume! Q {{ _ ; fun e => P e /\ Q e }}.

(* Opponent API *)

Parameter spec_mac: forall k A (a: A),
    {{ Level_Low (k, a) }} mac! k a {{ m ; Level_Low m }}.
Parameter spec_verify: forall k A (a: A) m,
    {{ Level_Low (k, a, m) }} verify! k a m {{ _ ; fun _ => True }}.
Parameter spec_fresh_key: forall a b,
    {{ Level_Low (a, b) }} fresh_key! a b {{ k ; Level_Low k }}.

Parameter spec_send: forall A (a: A) h,
    {{ Level_Low (a, h) }} send! h a {{ _ ; fun _ => True }}.
Parameter spec_receive: forall A,
    {{ fun _ => True }} receive! A {{ a ; Level_Low a }}.

Record aRPC := { impl_client: bytes -> M unit;
                 impl_server: M unit;
                 release_client: M key;
                 release_server: M key }.

Definition setup (a b: hostname): M aRPC :=
  let! k := fresh_key! a b in
  ret (Build_aRPC (fun req => client a b k req)
                  (server a b k)
                  (assume! (isEvent (Corrupted a)) ;; ret k)
                  (assume! (isEvent (Corrupted b)) ;; ret k)).

Record spec_aRPC (rpc: aRPC) :=
  { spec_client: forall req,
      {{ Level_Low req }} rpc.(impl_client) req {{ _ ; fun _ => True }} ;
    spec_server:
      {{ fun _ => True }} rpc.(impl_server) {{ _ ; fun _ => True }} ;
    spec_release_client:
      {{ fun _ => True }} rpc.(release_client)  {{ k ; Level_Low k }};
    spec_release_server:
      {{ fun _ => True }} rpc.(release_server) {{ k ; Level_Low k }} }.

(* NOT USEFUL! *)
(*
Axiom IO : Type.

Parameter attacker: (hostname -> hostname -> M (* { rpc : *) aRPC (* | spec_aRPC rpc } *)) -> IO -> M unit.

Theorem correctness: forall io, triple _
                                       (fun _ => True)
                                       (attacker setup io)
                                       (fun _ _ => True).
*)

author: BtheCat

repo: babel-MAC

save_path: github-repos/coq/BtheCat-babel-MAC


text:
Require Import List.
Import ListNotations.

Definition stack (X : Type) := list (list X * list X).

(* ** Post Grammars *)

Notation sig := nat.
(* a rule maps a non-terminal symbol to a word *)
Definition rule : Type := sig * list sig.
(* a context-free grammar consist of a start symbol and a list of rules *)
Definition cfg : Type := sig * list rule.
Definition rules (G : cfg) := snd G.
Definition startsym (G : cfg) := fst G.

(* single step context-free derivation *)
Inductive rew_cfg : cfg -> list sig -> list sig -> Prop :=
  | rewR R x a y v : In (a, v) (rules R) -> rew_cfg R (x++[a]++y) (x++v++y).

(* reflexive, transitive closure of single step context-free derivation *)
Inductive rewt (S: cfg) (x: list sig) : list sig -> Prop :=
  | rewtRefl : rewt S x x
  | rewtRule y z : rewt S x y -> rew_cfg S y z -> rewt S x z.

(* a word is terminal if it contains no non-terminals *)
Definition terminal G x := ~ exists y, rew_cfg G x y.

(* the language of a grammar consists of all derivable terminal words *)
Definition L (G : cfg) x := rewt G [startsym G] x /\ terminal G x.

(* The Context-free Palindrome Problem is
  given a context-free grammar to determine whether
  its language contains a palindrome. *)
Definition CFP : cfg -> Prop :=
  fun G => exists x, L G x /\ x = List.rev x.

(* The Context-free Intersection Problem is
  given two context-free grammars to determine whether
  their intersection is not empty. *)
Definition CFI : cfg * cfg -> Prop :=
  fun '(G1, G2) => exists x, L G1 x /\ L G2 x.

author: uds-psl

repo: coq-library-undecidability


text:
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

Definition one_shot_example : val := λ: <>,
  let: "x" := ref NONE in (
  (* tryset *) (λ: "n",
    CAS "x" NONE (SOME "n")),
  (* check  *) (λ: <>,
    let: "y" := !"x" in λ: <>,
    match: "y" with
      NONE => #()
    | SOME "n" =>
       match: !"x" with
         NONE => assert: #false
       | SOME "m" => assert: "n" = "m"
       end
    end)).

Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
Definition Pending : one_shotR := Cinl (Excl ()).
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).

Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.

Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !probG Σ, !one_shotG Σ}.

Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
  (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.

Lemma wp_one_shot (Φ : val → iProp Σ) :
  (∀ f1 f2 : val,
    (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
  ⊢ WP one_shot_example #() {{ Φ }}.
Proof.
  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
  rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
  iMod (own_alloc Pending) as (γ) "Hγ"; first done.
  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
  { iNext. iLeft. by iSplitL "Hl". }
  iModIntro. iApply "Hf"; iSplit.
  - iIntros (n) "!#". wp_let.
    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
    + wp_cas_suc. iMod (own_update with "Hγ") as "Hγ".
      { by apply cmra_update_exclusive with (y:=Shot n). }
      iMod ("Hclose" with "[-]"); last eauto.
      iNext; iRight; iExists n; by iFrame.
    + wp_cas_fail. iMod ("Hclose" with "[-]"); last eauto.
      rewrite /one_shot_inv; eauto 10.
  - iIntros "!# /=". wp_seq. wp_bind (! _)%E.
    iInv N as ">Hγ" "Hclose".
    iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
       ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
      + iExists NONEV. iFrame. eauto.
      + iExists (SOMEV #m). iFrame. eauto. }
    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
    iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
      ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
      + iSplit. iLeft; by iSplitL "Hl". eauto.
      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
    iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
    wp_let. iIntros "!#". wp_seq.
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
    { by wp_match. }
    wp_match. wp_bind (! _)%E.
    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m') "[Hl Hγ]".
    { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
    wp_load.
    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
    iMod ("Hclose" with "[Hl]") as "_".
    { iNext; iRight; by eauto. }
    iModIntro. wp_match. iApply wp_assert.
    wp_op. by case_bool_decide.
Qed.

Lemma ht_one_shot (Φ : val → iProp Σ) :
  {{ True }} one_shot_example #()
    {{ ff,
      (∀ n : Z, {{ True }} Fst ff #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
    }}.
Proof.
  iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
  - iIntros (n) "!# _". wp_proj. iApply "Hf1".
  - iIntros "!# _". wp_proj.
    iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.

author: jtassarotti

repo: polaris

save_path: github-repos/coq/jtassarotti-polaris


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Definition synth (y : natural) : natural := plus Zero (plus Zero y).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import Fiat.Parsers.ContextFreeGrammar.Core.
Require Import Fiat.Parsers.GenericRecognizerMin.
Require Import Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes.
Require Import Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes.
Require Import Fiat.Parsers.MinimalParseOfParse.
Require Import Fiat.Common.
Require Import Fiat.Parsers.ContextFreeGrammar.Valid.
Require Import Fiat.Parsers.GenericRecognizer.
Local Open Scope string_like_scope.

Section convenience.
  Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}.
  Context {data : @boolean_parser_dataT Char _}
          {cdata : @boolean_parser_completeness_dataT' Char _ _ G _}
          {rdata : @parser_removal_dataT' _ G _}
          {gendata : generic_parser_dataT Char}
          {gencdata : generic_parser_correctness_dataT}
          (gvalid : grammar_valid G).

  Local Ltac t :=
    match goal with
    | [ H : ?R true ?v, H' : ?R (bool_of_sum ?x) ?v |- _ ]
      => destruct x; simpl in *
    | [ H : ?R (bool_of_sum ?x) ?v |- ?R true ?v ]
      => destruct x; simpl in *
    end;
    try solve [ assumption
              | exfalso;
                solve [ eapply parse_nt_is_correct_disjoint; eassumption
                      | eapply parse_item_is_correct_disjoint; eassumption
                      | eapply parse_production_is_correct_disjoint; eassumption
                      | eapply parse_productions_is_correct_disjoint; eassumption
                      | auto with nocore ] ].

  Definition parse_item_sound
             (str : String) (it : item Char)
  : parse_item_is_correct str it true (parse_item str it)
    -> parse_of_item G str it.
  Proof.
    intro pit.
    pose proof (parse_item_correct str it).
    t.
    eapply parse_of_item__of__minimal_parse_of_item; eassumption.
  Defined.

  Definition parse_item_complete
             (str : String) (it : item Char)
             (p : parse_of_item G str it)
  : parse_item_is_correct str it true (parse_item str it).
  Proof.
    apply minimal_parse_of_item__of__parse_of_item in p.
    pose proof (parse_item_correct str it).
    t.
  Qed.

  Definition parse_nonterminal_sound
             (str : String) (nt : String.string)
  : parse_nt_is_correct str (of_nonterminal nt) true (parse_nonterminal str nt)
    -> parse_of_item G str (NonTerminal nt).
  Proof.
    intro pit.
    pose proof (parse_nonterminal_correct str nt).
    t.
    eapply parse_of_item_nonterminal__of__minimal_parse_of_nonterminal; eassumption.
  Defined.

  Definition parse_nonterminal_complete
             (str : String) (nt : String.string)
             (p : parse_of_item G str (NonTerminal nt))
  : parse_nt_is_correct str (of_nonterminal nt) true (parse_nonterminal str nt).
  Proof.
    apply minimal_parse_of_nonterminal__of__parse_of_item_nonterminal in p.
    pose proof (parse_nonterminal_correct str nt).
    t.
  Qed.

  Definition parse_of_nonterminal_complete
             (str : String) (nt : String.string)
             (H : List.In nt (Valid_nonterminals G))
             (p : parse_of G str (Lookup G nt))
  : parse_nt_is_correct str (of_nonterminal nt) true (parse_nonterminal str nt).
  Proof.
    apply (parse_nonterminal_complete (ParseNonTerminal _ H p)).
  Qed.
End convenience.

author: mit-plv

repo: fiat

save_path: github-repos/coq/mit-plv-fiat


text:
Lemma plus_comm : forall n m, n + m = m + n.
Proof.
  intros n. induction n; intros; eauto.
  induction m; eauto. simpl.
  rewrite (IHn (S m)). rewrite <- IHm. simpl.
  replace (m + n) with (n + m) by apply IHn; eauto.
Qed.

Lemma plus_assoc : forall n m k, n + (m + k) = n + m + k.
Proof.
  intros; induction n; simpl; eauto.
Qed.

Lemma mul_comm : forall n m, n * m = m * n.
Proof.
  intros n. induction n; eauto. induction m; eauto.
  simpl. rewrite (IHn (S m)); rewrite <- IHm. simpl.
  rewrite (IHn m). repeat rewrite plus_assoc. rewrite (plus_comm m n); eauto.
Qed.

Lemma plus_mul_dist : forall n m k, n * (m + k) = n * m + n * k.
Proof.
  intros; induction k.
  + rewrite plus_comm. rewrite (mul_comm _ 0). simpl.
    rewrite plus_comm. eauto.
  + rewrite plus_comm. rewrite (mul_comm n (_ + _)).
    rewrite (mul_comm _ (S _)). simpl.
    rewrite mul_comm. rewrite (plus_comm k m). rewrite IHk.
    rewrite (plus_assoc (n * m) _). rewrite (plus_comm _ n).
    rewrite plus_assoc. rewrite (mul_comm n k). eauto.
Qed.

Lemma mul_assoc : forall n m k, n * (m * k) = n * m * k.
Proof.
  intros; induction n; simpl; eauto.
  rewrite (mul_comm (_ + _) k); rewrite plus_mul_dist; rewrite (mul_comm k _).
  rewrite (mul_comm k _). rewrite IHn; eauto.
Qed.

Lemma mul_n_Sm : forall n m, n * S m = n + n * m.
Proof.
  intros. rewrite (mul_comm _ (S _)). simpl.
  replace (n * m) with (m * n); try reflexivity.
  apply mul_comm.
Qed.

Corollary plus_zero : forall n, n + 0 = n.
Proof.
  induction n; eauto.
Qed.

Corollary mul_zero : forall n, n * 0 = 0.
Proof.
  induction n; eauto.
Qed.

Ltac simpl_arith :=
  repeat match goal with
  | [ |- context [?n + S ?m]] => rewrite <- (plus_n_Sm n m)
  | [ |- context [S ?n + ?m]] =>
    replace (S n + m) with (S (n + m)) by eauto
  | [ |- context [?n * S ?m]] => rewrite (mul_n_Sm n m)
  | [ |- context [S ?n * ?m]] =>
    replace (S n * m) with (m + n * m) by eauto
  | [ |- context [?n + 0]] => rewrite (plus_zero n)
  | [ |- context [0 + ?n]] => replace (0 + n) with n by eauto
  | [ |- context [?n * 0]] => rewrite (mul_zero n)
  | [ |- context [0 * ?n]] => replace (0 * n) with 0 by eauto
  end
.

Lemma strong_natind_lim : forall (P : nat -> Prop) (lim : nat),
  (forall n, (forall k, k < n -> P k) -> P n)
  -> (forall n, n < lim -> P n).
Proof.
  intros P lim; revert P. induction lim.
  + intros. destruct n; inversion H0.
  + intros. inversion H0; subst; clear H0.
    - specialize (IHlim P H). exact (H lim IHlim).
    - assert (n < lim). { assumption. } clear H2.
      exact (IHlim P H n H0).
Qed.

Lemma strong_natind : forall (P : nat -> Prop),
  (forall n, (forall k, k < n -> P k) -> P n) -> forall n, P n.
Proof.
  intros. assert (n < S n). { eauto. }
  exact (strong_natind_lim P (S n) H n H0).
Qed.

Lemma plus_minus_cancel: forall n m, m + n - m = n.
Proof.
  intro n. induction n; intros; induction m; eauto.
Qed.

repo: coq-number-theory