(*-*-coding: utf-8;-*-*)

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Arith.
Require Import Omega.

(****)

(** * General definitions *)

Inductive optionT (A : Type) : Type :=
  | SomeT : A -> optionT A
  | NoneT : optionT A.

Implicit Arguments NoneT [A].

Definition is_transitive (A : Type) (r : A -> A -> Prop) :=
  forall x y z : A, r x y -> r y z -> r x z.

Definition is_injective (A B : Type) (f : A -> B) :=
  forall x y, f x = f y -> x = y.

(****)

(** ** Well-foundation *)

Section well_foundation.

Variable A : Type.
Variable R : A -> A -> Prop.

Inductive accessible : A -> Prop :=
   accessible_intro :
     forall x, (forall y, R x y -> accessible y) -> accessible x.

Lemma accessible_inversion :
  forall x, accessible x -> forall y, R x y -> accessible y.
intros x H1; case H1; trivial.
Defined.

Definition is_well_founded := forall x, accessible x.

Lemma well_founded_induction :
  is_well_founded ->
  forall P : A -> Prop,
  (forall x, (forall y, R x y -> P y) -> P x) -> forall x, P x.
intros H0 P H1 x; apply (@accessible_ind P); auto.
Qed.

End well_foundation.

(****)

(** * Core definitions and properties *)

(** ** Worlds and values *)

Module Type WORLDS.

Parameter world : Type.
Parameter world_sub : world -> world -> Prop.
Axiom world_sub_trans : is_transitive world_sub.
Axiom world_sub_well_founded : is_well_founded world_sub.

Parameter value : Type.
Parameter element : Type.

Parameter elem_to_val : element -> value -> Prop.
Axiom elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Axiom elem_to_val_function :
  forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.

End WORLDS.

(****)

Module Core (W : WORLDS).

Export W.

(** ** Configurations *)
Record config : Type := { c_w : world; c_v : value }.

Definition config_sub c c' := world_sub (c_w c) (c_w c') /\ c_v c' = c_v c.

Lemma config_sub_trans : is_transitive config_sub.
intros c c' c'' (H1, H2) (H3, H4); split;
  [ exact (world_sub_trans H1 H3)
  | rewrite <- H2; trivial ].
Qed.

(****)

(** ** Semantics of the logic *)

Definition type := config -> Prop.

Definition Implies (s t : type) : type := fun c => s c -> t c.
Definition Conj (s t : type) : type := fun c => s c /\ t c.
Definition Disj (s t : type) : type := fun c => s c \/ t c.
Definition Later (t : type) : type :=
  fun c => forall c', config_sub c c' -> t c'.
Definition T : type := fun _ => True.
Definition F : type := fun _ => False.
Definition Forall (A : Type) (f : A -> type) : type :=
  fun c => forall x, f x c.
Definition Exists (A : Type) (f : A -> type) : type :=
  fun c => exists x, f x c.
Definition EW (t : type) : type :=
  fun c => forall v, t (Build_config (c_w c) v).
Definition SW (t : type) : type :=
  fun c => exists v, t (Build_config (c_w c) v).

Notation "s ⇒ t" := (Implies s t) (at level 85, right associativity).
Notation "s ∧ t" := (Conj s t) (at level 81, left associativity).
Notation "s ∨ t" := (Disj s t) (at level 81, left associativity).
Notation "∆ t" := (Later t) (at level 75, right associativity).
Notation "∃ x , t" := (Exists (fun x => t)) (at level 200, x ident).
Notation "∀ x , t" :=
  (Forall (fun x => t)) (at level 200, x ident, right associativity).

Definition Sequent (s t : type) := forall c, (s ⇒ t) c.

Notation "s ⊢ t" := (Sequent s t) (at level 86, right associativity).

(****)

(** ** Logic rules *)

Lemma id : forall t, t ⊢ t.
intros t c H; trivial.
Qed.

Lemma cut : forall t1 t2 t3, t1 ⊢ t2 -> t2 ⊢ t3 -> t1 ⊢ t3.
intros t1 t2 t3 H1 H2 c H3; apply H2; apply H1; trivial.
Qed.

Lemma conj_r : forall s t1 t2, s ⊢ t1 -> s ⊢ t2 -> s ⊢ t1 ∧ t2.
intros s t1 t2 H1 H2 c H3; split; [ apply H1 | apply H2 ]; trivial.
Qed.

Lemma conj_l_1 : forall t1 t2, t1 ∧ t2 ⊢ t1.
intros t1 t2 c (H1, H2); trivial.
Qed.

Lemma conj_l_2 : forall t1 t2, t1 ∧ t2 ⊢ t2.
intros t1 t2 c (H1, H2); trivial.
Qed.

Lemma disj_l : forall s t1 t2, t1 ⊢ s -> t2 ⊢ s -> t1 ∨ t2 ⊢ s.
intros s t1 t2 H1 H2 c [H3 | H3]; [ apply H1 | apply H2]; trivial.
Qed.

Lemma disj_r_1 : forall t1 t2, t1 ⊢ t1 ∨ t2.
intros t1 t2 c H1; left; trivial.
Qed.

Lemma disj_r_2 : forall t1 t2, t2 ⊢ t1 ∨ t2.
intros t1 t2 c H1; right; trivial.
Qed.

Lemma false_l : forall t, F ⊢ t.
intros t c H; contradiction.
Qed.

Lemma true_r : forall t, t ⊢ T.
intros t c H; red; trivial.
Qed.

Lemma implies_i : forall s t1 t2, s ∧ t1 ⊢ t2 -> s ⊢ t1 ⇒ t2.
intros s t1 t2 H1 c H2 H3; apply H1; split; trivial.
Qed.

Lemma implies_e : forall s t1 t2, s ⊢ t1 ⇒ t2 -> s ∧ t1 ⊢ t2.
intros s t1 t2 H1 c (H2, H3); apply H1; trivial.
Qed.

Lemma forall_r :
  forall A (f : A -> type) t, (forall x, t ⊢ f x) -> t ⊢ Forall f.
firstorder.
Qed.

Lemma forall_l : forall A a (f : A -> type), Forall f ⊢ f a.
firstorder.
Qed.

Lemma exists_l :
  forall A (f : A -> type) t, (forall x, f x ⊢ t) -> Exists f ⊢ t.
firstorder.
Qed.

Lemma exists_r : forall A a (f : A -> type), f a ⊢ Exists f.
firstorder.
Qed.

Lemma later_lift : forall s t, s ⊢ t -> ∆s ⊢ ∆t.
intros s t H1 c H2 c' H3; apply H1; apply H2; trivial.
Qed.

Lemma later_double : forall s, ∆s ⊢ ∆∆s.
intros s c H1 c' H2 c'' H3; apply H1; apply (config_sub_trans H2 H3).
Qed.

Lemma later_fix : forall p, ∆p ⊢ p -> T ⊢ p.
intros t H1 (w, v) H2;
apply (well_founded_induction world_sub_well_founded)
with (P := fun w => t (Build_config w v));
clear w H2; intros w H2; apply H1; intros (w', v') (H3, E); simpl in E;
subst v'; auto.
Qed.

Lemma later_conj : forall s t, ∆s ∧ ∆t ⊢ ∆(s ∧ t).
intros s t c (H1, H2) c' H3; split; [ apply H1 | apply H2 ]; trivial.
Qed.

Lemma later_true : T ⊢ ∆T.
intros c H1 c' H2; trivial.
Qed.

Lemma later_forall : forall A (f : A -> type), (∀x, ∆(f x)) ⊢ ∆ (Forall f).
intros A f c H1 c' H2 x; apply H1; trivial.
Qed.

Lemma everywhere_lift : forall s t, s ⊢ t -> EW s ⊢ EW t.
intros s t H1 c H2 v; apply H1; apply H2.
Qed.

Lemma everywhere_double : forall t, EW t ⊢ EW (EW t).
intros t c H1 v H2; trivial.
Qed.

Lemma everywhere_d : forall t, EW t ⊢ t.
intros t (w, v) H1; apply H1.
Qed.

Lemma everywhere_conj : forall s t, EW s ∧ EW t ⊢ EW (s ∧ t).
intros s t c H1 v; split; [ apply (proj1 H1) | apply (proj2 H1) ].
Qed.

Lemma everywhere_true : T ⊢ EW T.
repeat red; trivial.
Qed.

Lemma later_everywhere : forall t, EW (∆t) ⊢ ∆(EW t).
intros t c H1 c' H2 v; apply (H1 v); repeat split; exact (proj1 H2).
Qed.

Lemma everywhere_later : forall t, ∆(EW t) ⊢ EW (∆t).
intros t (w, v) H1 v'' (w', v') H2;
apply (fun H => H1 (Build_config w' v) H v');
repeat split; exact (proj1 H2).
Qed.

Lemma everywhere_implies : forall s t, EW (s ⇒ t) ⊢ SW s ⇒ SW t.
intros s t c H1 (v, H2); exists v; apply H1; trivial.
Qed.

Lemma somewhere_l : forall s t, s ⊢ EW t -> SW s ⊢ EW t.
intros s t H1 c (v, H2); exact (H1 _ H2).
Qed.

(****)

(** ** Derived rules *)

Lemma implies_l : forall s t, (s ⇒ t) ∧ s ⊢ t.
intros s t; apply implies_e; apply id.
Qed.

Lemma implies_to_sequent : forall s t, T ⊢ s ⇒ t -> s ⊢ t.
intros s t H1; apply cut with (t2 := T ∧ s);
  [ apply conj_r; [ apply true_r | apply id ]
  | apply implies_e; trivial ].
Qed.

Lemma conj_sym : forall s t, s ∧ t ⊢ t ∧ s.
intros s t; apply conj_r; [ apply conj_l_2 | apply conj_l_1 ].
Qed.

Lemma conj_assoc_1 : forall t1 t2 t3, t1 ∧ (t2 ∧ t3) ⊢ (t1 ∧ t2) ∧ t3.
intros t1 t2 t3; apply conj_r;
  [ apply conj_r;
      [ apply conj_l_1
      | apply cut with (t2 := t2 ∧ t3);
          [ apply conj_l_2
          | apply conj_l_1 ] ]
  | apply cut with (t2 := t2 ∧ t3); apply conj_l_2 ].
Qed.

Lemma conj_assoc_2 : forall t1 t2 t3, (t1 ∧ t2) ∧ t3 ⊢ t1 ∧ (t2 ∧ t3).
intros t1 t2 t3; apply conj_r;
  [ apply cut with (t2 := t1 ∧ t2); apply conj_l_1
  | apply conj_r;
      [ apply cut with (t2 := t1 ∧ t2);
          [ apply conj_l_1
          | apply conj_l_2 ]
      | apply conj_l_2 ] ].
Qed.

Lemma conj_contract : forall t, t ⊢ t ∧ t.
intro t; apply conj_r; apply id.
Qed.

Lemma disj_sym : forall s t, s ∨ t ⊢ t ∨ s.
intros s t; apply disj_l; [ apply disj_r_2 | apply disj_r_1 ].
Qed.

Lemma disj_assoc_1 : forall t1 t2 t3, t1 ∨ (t2 ∨ t3) ⊢ (t1 ∨ t2) ∨ t3.
intros t1 t2 t3; apply disj_l;
  [ apply cut with (t2 := t1 ∨ t2); apply disj_r_1
  | apply disj_l;
      [ apply cut with (t2 := t1 ∨ t2);
          [ apply disj_r_2
          | apply disj_r_1 ]
      | apply disj_r_2 ] ].
Qed.

Lemma disj_assoc_2 : forall t1 t2 t3, (t1 ∨ t2) ∨ t3 ⊢ t1 ∨ (t2 ∨ t3).
intros t1 t2 t3; apply disj_l;
  [ apply disj_l;
      [ apply disj_r_1
      | apply cut with (t2 := t2 ∨ t3);
          [ apply disj_r_1
          | apply disj_r_2 ] ]
  | apply cut with (t2 := t2 ∨ t3); apply disj_r_2 ].
Qed.

Lemma later_r : forall s t, ∆s ⊢ t -> ∆s ⊢ ∆t.
intros p q H1; apply cut with (1 := @later_double p);
apply later_lift; trivial.
Qed.

(****)

(** ** Tactics useful for reasoning with the embedded logic *)

Lemma peek_1 :
  forall t1 t2 t1' t2' s, t1 ∧ t2 ⊢ t1' ∧ t2' -> t1 ∧ t2 ∧ s ⊢ t1' ∧ s ∧ t2'.
intros t1 t2 t1' t2' s H;
apply conj_r;
  [ apply conj_r;
      [ refine (cut (@conj_l_1 _ _) _);
        apply cut with (1 := H);
        apply conj_l_1
      | apply conj_l_2 ]
  | refine (cut (@conj_l_1 _ _) _);
    apply cut with (1 := H);
    apply conj_l_2 ].
Qed.

Ltac peek_rec n s0 t0 rem :=
  match eval compute in n with
    0   => apply (rem _ _ _ _ (@id (s0 ∧ t0)))
  | S ?n =>
     match s0 with
       ?t1 ∧ ?t2 =>
          peek_rec n t1 t2
           (fun s t s' t' (H : s ∧ t ⊢ s' ∧ t') =>
              rem _ _ _ _ (peek_1 (s := t0) H))
     | _        =>
          apply (rem _ _ _ _ (@conj_sym s0 t0))
     end
  end.

Ltac peek_hyp n :=
  match goal with
    |-  ?s ∧ ?t ⊢ ?concl =>
      peek_rec n s t
        (fun s t s' t' (H : s ∧ t ⊢ s' ∧ t') => (@cut _ _ concl H))
  | |-  _ ⊢ _ =>
      idtac
  end.

Lemma conj_add :
  forall s t1 t2, t1 ⊢ t2 -> s ∧ t1 ⊢ s ∧ t2.
intros s t1 t2 H1; apply conj_r;
  [ apply conj_l_1
  | apply cut with (2 := H1); apply conj_l_2 ].
Qed.

Ltac leftapp t :=
  first
    [ refine (cut t _)
    | refine (cut (conj_add t) _)
    | refine (cut (@t _) _)
    | refine (cut (conj_add (@t _)) _)
    | refine (cut (@t _ _) _)
    | refine (cut (conj_add (@t _ _)) _)
    | refine (cut (@t _ _ _) _)
    | refine (cut (conj_add (@t _ _ _)) _)
    | refine (cut (@t _ _ _ _) _)
    | refine (cut (@t _ _ _ _ _) _)
    | refine (cut (@t _ _ _ _ _ _) _) ].

Ltac rightapp t :=
  first
    [ refine (cut _ t)
    | refine (cut _ (conj_add t))
    | refine (cut _ (@t _))
    | refine (cut _ (conj_add (@t _)))
    | refine (cut _ (@t _ _))
    | refine (cut _ (conj_add (@t _ _)))
    | refine (cut _ (@t _ _ _))
    | refine (cut _ (conj_add (@t _ _ _)))
    | refine (cut _ (@t _ _ _ _))
    | refine (cut _ (@t _ _ _ _ _))
    | refine (cut _ (@t _ _ _ _ _ _)) ].

Lemma exists_extrusion :
  forall A (f : A -> type) s t,
  (forall x, s ∧ f x ⊢ t) -> s ∧ (Exists f) ⊢ t.
intros A f s t H1;
leftapp conj_sym;
apply implies_e; apply exists_l; intro x; apply implies_i;
leftapp conj_sym; trivial.
Qed.

Ltac normalize2 :=
  match goal with
  | |- _ ∧ T ⊢ _ =>
      leftapp conj_l_1; normalize2
  | |- _ ∧ (_ ∧ _) ⊢ _ =>
      leftapp conj_assoc_1; apply implies_e; normalize2
  | |- _ ∧ Exists _ ⊢ _ =>
      apply exists_extrusion;
      let x := fresh "x" in
      (intro x; normalize2; generalize x; clear x)
  | |- T ∧ _ ⊢ _ =>
      leftapp conj_l_2; normalize2
  | |- _ ⊢ _ ⇒ _ =>
      apply implies_i; normalize2
  | |- _ =>
      idtac
  end.

Ltac normalize :=
  match goal with
  | |- _ ∧ _ ⊢ _ =>
      apply implies_e; normalize
  | |- Exists _ ⊢ _ =>
      apply exists_l;
      let x := fresh "x" in
      (intro x; normalize; generalize x; clear x)
  | |- _ =>
      normalize2
  end.

(****)

(** ** Generalized Löb rule *)

Lemma later_fix_2 :
  forall s t, s ⊢ ∆s -> s ∧ ∆t ⊢ t -> s ⊢ t.
intros s t G1 H1; apply implies_to_sequent; apply later_fix;
assert (H2 : ∆(s ⇒ t) ⊢ ∆s ⇒ ∆t);
  [ normalize;
    leftapp later_conj; apply later_lift; apply implies_l
  | leftapp H2; normalize; refine (cut _ H1);
    apply conj_r;
      [ apply conj_l_2
      | leftapp G1;
        apply cut with (t2 := ∆t);
          [ apply implies_l
          | apply later_lift; apply id ] ] ].
Qed.

(****)

(** ** Equivalence (derived construction) *)

Definition Equiv s t : type := (s ⇒ t) ∧ (t ⇒ s).

Notation "s ⇔ t" := (Equiv s t) (at level 85, right associativity).

Lemma equiv_refl : forall t, T ⊢ t ⇔ t.
intro t; unfold Equiv; apply conj_r; normalize; apply id.
Qed.

Lemma equiv_trans : forall t1 t2 t3, (t1 ⇔ t2) ∧ (t2 ⇔ t3) ⊢ t1 ⇔ t3.
intros t1 t2 t3; unfold Equiv; apply conj_r; normalize;
  [ peek_hyp 2; apply implies_e; apply cut with (t2 := t2);
      [ apply implies_e; leftapp conj_l_1; leftapp conj_l_1; apply id
      | normalize; peek_hyp 1; apply implies_l ]
  | peek_hyp 3; apply implies_e; apply cut with (t2 := t2);
      [ apply implies_e; leftapp conj_l_2; apply id
      | normalize; peek_hyp 1; apply implies_l ] ].
Qed.

Lemma equiv_sym : forall s t, s ⇔ t ⊢ t ⇔ s.
intros s t; unfold Equiv; apply conj_r; [ apply conj_l_2 | apply conj_l_1 ].
Qed.

(****)

(** ** Type equality *)

Definition teq s t := EW (s ⇔ t).

Lemma teq_sym : forall s t, teq s t ⊢ teq t s.
unfold teq; intros s t; apply everywhere_lift; apply equiv_sym.
Qed.

Lemma teq_trans : forall t1 t2 t3, teq t1 t2 ∧ teq t2 t3 ⊢ teq t1 t3.
unfold teq; intros t1 t2 t3; leftapp everywhere_conj; apply everywhere_lift;
apply equiv_trans.
Qed.

(****)

(** ** Singleton types *)

Definition tjust (e : element) : type := fun c => elem_to_val e (c_v c).

Lemma later_tjust : forall e, tjust e ⊢ ∆tjust e.
intros e c H1 c' H2; unfold tjust; rewrite (proj2 H2); trivial.
Qed.

Lemma later_tjust_2 : forall e t, tjust e ⇒ ∆t ⊢ ∆(tjust e ⇒ t).
intros e t c H1 c' H2 H3; apply H1; trivial;
red; rewrite <- (proj2 H2); trivial.
Qed.

Lemma somewhere_tjust : forall e, T ⊢ SW (tjust e).
intros e c H1; exact (elem_to_val_surjective e).
Qed.

Lemma tjust_subst :
  forall A (f : A -> element) (g : A -> type) x x',
  is_injective f -> tjust (f x) ∧ tjust (f x') ⊢ g x ⇒ g x'.
unfold tjust; intros A f g x x' H0 c (E1, E2) H1;
rewrite <- (H0 _ _ (elem_to_val_function E1 E2)); trivial.
Qed.

(****)

Definition thas e t := EW (tjust e ⇒ t).

Lemma later_thas : forall e t, thas e (∆t) ⊢ ∆(thas e t).
intros e t; unfold thas; rightapp later_everywhere; apply everywhere_lift;
apply later_tjust_2.
Qed.

Lemma thas_lift : forall e s t, s ⊢ t -> thas e s ⊢ thas e t.
intros e s t H1; unfold thas; apply everywhere_lift; normalize;
rightapp H1; apply implies_l.
Qed.

Lemma thas_e :
  forall e t, thas e t ⊢ SW (tjust e ∧ t).
intros e t H1; unfold thas;
apply cut with (t2 := EW (tjust e ⇒ tjust e ∧ t));
  [ apply everywhere_lift; normalize; leftapp (@conj_contract (tjust e));
    normalize; apply implies_e; leftapp implies_l;
    normalize; apply conj_sym
  | leftapp everywhere_implies;
    apply implies_to_sequent;
    leftapp (somewhere_tjust e);
    normalize; peek_hyp 1; apply implies_l ].
Qed.

Lemma change_type :
  forall e t t', ∆teq t t' ∧ ∆thas e t ⊢ ∆thas e t'.
intros l t t';
leftapp later_conj; apply later_lift;
leftapp everywhere_conj; unfold thas; apply everywhere_lift;
unfold Equiv; normalize; leftapp conj_assoc_2; leftapp implies_l;
peek_hyp 2; peek_hyp 1; leftapp conj_assoc_2; leftapp implies_l;
apply conj_l_2.
Qed.

Definition scalar_type (t : type) :=
  forall w e v v',
  elem_to_val e v -> elem_to_val e v' ->
  t (Build_config w v) -> t (Build_config w v').

Lemma thas_exists_1 :
  forall A e (f : A -> type), (∃x, thas e (f x)) ⊢ thas e (Exists f).
intros A e f; apply exists_l; intro x; apply thas_lift; apply exists_r.
Qed.

Lemma thas_exists_2 :
  forall A e (f : A -> type),
  (forall x, scalar_type (f x)) ->
  thas e (Exists f) ⊢ ∃x, thas e (f x).
unfold thas; intros A e f H0;
unfold EW, Exists, Implies, tjust; simpl; intros c H1;
generalize (elem_to_val_surjective e);
intros (v, H2); generalize (H1 _ H2); intros (x, H3);
exists x; intros v' H4; exact (H0 x _ _ _ _ H2 H4 H3).
Qed.

(****)

Definition necessary t := t ⊢ ∆t.

Lemma necessary_fold : forall t, necessary t -> t ⊢ ∆t.
trivial.
Qed.

Lemma conj_necessary :
  forall s t, necessary s -> necessary t -> necessary (s ∧ t).
intros s t H1 H2; leftapp H2; leftapp conj_sym; leftapp H1;
leftapp later_conj; apply later_lift; apply conj_sym.
Qed.

Lemma true_necessary : necessary T.
exact later_true.
Qed.

Lemma exists_necessary :
  forall (A : Type) (f : A -> type),
  (forall x, necessary (f x)) -> necessary (Exists f).
intros A f H1; red;
apply exists_l; intro x; leftapp H1; apply later_lift; apply exists_r.
Qed.

Lemma later_necessary : forall t, necessary (∆ t).
intro t; red; apply later_r; apply id.
Qed.

Lemma everywhere_necessary : forall t, necessary t -> necessary (EW t).
red; intros t H1; rightapp later_everywhere; apply everywhere_lift; exact H1.
Qed.

Lemma tjust_necessary : forall e, necessary (tjust e).
exact later_tjust.
Qed.

Lemma thas_necessary : forall e t, necessary t -> necessary (thas e t).
intros e t H1; red; rightapp later_thas; apply thas_lift; trivial.
Qed.

Hint Resolve necessary_fold conj_necessary true_necessary exists_necessary
             later_necessary everywhere_necessary tjust_necessary
             thas_necessary.

(****)

(** ** Necessity *)

Definition nec t := t ∧ ∆t.

Lemma nec_true : T ⊢ nec T.
unfold nec; apply conj_r; [ apply id | apply later_true ].
Qed.

Lemma nec_lift : forall s t, s ⊢ t -> nec s ⊢ nec t.
intros s t H1; unfold nec; apply conj_r;
  [ leftapp conj_l_1; trivial
  | leftapp conj_l_2; apply later_lift; trivial ].
Qed.

Lemma nec_d : forall t, nec t ⊢ t.
intros t; unfold nec; apply conj_l_1.
Qed.

Lemma nec_necessary : forall t, necessary (nec t).
intro t; unfold necessary, nec; leftapp conj_l_2;
leftapp conj_contract; leftapp later_necessary; leftapp later_conj; apply id.
Qed.

Hint Resolve nec_necessary.

Lemma nec_and_necessity : forall t, necessary t -> t ⊢ nec t.
intros t H; unfold nec; apply conj_r; [ apply id | trivial ].
Qed.

Lemma Grzegorczyk_axiom :
  forall t, nec (nec (t ⇒ nec t) ⇒ t) ⊢ t.
intro t; apply implies_to_sequent; apply later_fix;
normalize; leftapp (fun t => @conj_contract (nec t)); normalize;
leftapp nec_d; apply implies_e; apply cut with (t2 := nec (t ⇒ nec t));
  [ leftapp nec_and_necessity; auto;
    apply nec_lift;
    apply cut with (t2 := ∆t);
      [ leftapp nec_necessary; leftapp later_conj; apply later_lift;
        apply implies_l
      | normalize; peek_hyp 1; apply id ]
  | normalize; peek_hyp 1; apply implies_l ].
Qed.

(****)

(** ** Recursive types *)

Definition contractive (f : type -> type) :=
  forall s t, ∆ teq s t ⊢ teq (f s) (f t).

Definition contractive' (f : type -> type) :=
  forall t t', ∆teq t t' ⊢ f t ⇒ f t'.

Lemma contractive'_to_contractive : forall f, contractive' f -> contractive f.
intros f H s t; apply cut with (t2 := EW (∆teq s t));
  [ rightapp everywhere_later; apply later_lift;
    unfold teq; apply everywhere_double
  | unfold teq at 2, Equiv; apply everywhere_lift; apply conj_r;
      [ apply H
      | rightapp H; apply later_lift; apply teq_sym ] ].
Qed.

Lemma unique_fixpoint :
  forall f, contractive f ->
  forall s t, T ⊢ teq s (f s) -> T ⊢ teq t (f t) -> T ⊢ teq s t.
intros f H1 s t H2 H3;
assert (H4 : nec (teq s (f s) ∧ teq t (f t)) ⊢ teq s t);
  [ apply implies_to_sequent; apply later_fix; normalize;
    leftapp (fun t => @conj_contract (nec t)); normalize;
    leftapp nec_d; apply implies_e; apply cut with (t2 := teq (f s) (f t));
      [ leftapp nec_necessary; leftapp later_conj;
        rightapp H1; apply later_lift; apply implies_l
      | normalize; leftapp teq_sym; peek_hyp 2; peek_hyp 1;
        leftapp conj_assoc_2; leftapp teq_trans; apply teq_trans ]
  | rightapp H4; leftapp nec_true; apply nec_lift; apply conj_r; trivial ].
Qed.

Section fixpoint.

Variable f : type -> type.

Fixpoint rec_def
     (c : config) (r : accessible world_sub (c_w c)) {struct r} : Prop :=
  f (fun c' => forall (H : world_sub (c_w c) (c_w c')),
               @rec_def c' (accessible_inversion r H))
    c.

Lemma rec_def_unfolding :
  forall c (r : accessible world_sub (c_w c)),
  @rec_def c r <->
  f (fun c' => forall (H : world_sub (c_w c) (c_w c')),
               @rec_def c' (accessible_inversion r H)) c.
intros (w, v) r; simpl in r; case r; simpl; intros x r'; apply iff_refl.
Qed.

Lemma rec_def_invariance :
  contractive f ->
  forall c (r r' : accessible world_sub (c_w c)),
  @rec_def c r <-> @rec_def c r'.
intros H0 (w, v); generalize v; clear v;
induction (world_sub_well_founded w) as [w H1 H2];
intros v r r'; apply iff_trans with (1 := rec_def_unfolding r);
apply iff_trans with (2 := iff_sym (rec_def_unfolding r'));
refine (H0 _ _ (Build_config w v) _ _);
intros c' H3 v'; split;
  [ intros H4 H5; apply (fun p => proj1 (H2 _ H5 v' _ p) (H4 H5))
  | intros H4 H5; apply (fun p => proj2 (H2 _ H5 v' p _) (H4 H5)) ].
Qed.

End fixpoint.

Definition Rec (f : type -> type) : type :=
  fun c => @rec_def f c (world_sub_well_founded (c_w c)).

Lemma fixpoint_property :
  forall f : type -> type, contractive f -> T ⊢ teq (Rec f) (f (Rec f)).
intros f H; apply later_fix; intros (w, v) H1 v'; unfold Rec at 1;
refine
  (iff_trans
     (@rec_def_unfolding f (Build_config w v') (world_sub_well_founded w)) _);
refine (H _ _ (Build_config w v) _ v');
intros c' H2 v''; split;
  [ intro H4; generalize (H4 (proj1 H2));
    refine (proj1 (rec_def_invariance H _ _))
  | intros H4 H5; generalize H4; refine (proj2 (rec_def_invariance H _ _)) ].
Qed.

Lemma unfolding : forall f : type -> type, contractive f -> Rec f ⊢ f (Rec f).
intros f H; apply implies_to_sequent;
leftapp (fixpoint_property H); unfold teq; leftapp everywhere_d;
unfold Equiv; apply conj_l_1.
Qed.

Lemma folding : forall f : type -> type, contractive f -> f (Rec f) ⊢ Rec f.
intros f H; apply implies_to_sequent;
leftapp (fixpoint_property H); unfold teq; leftapp everywhere_d;
unfold Equiv; apply conj_l_2.
Qed.

(****)

(** ** End of core definitions and properties *)

End Core.

(****)

(** * Dealing with the store *)

(** ** Assumption for dealing with the store *)

Module Type STORE_HYPS.

Parameter value : Type.
Parameter element : Type.
Parameter elem_to_val : element -> value -> Prop.
Parameter location : Type.
Parameter loc_to_elem : location -> element.

Axiom elem_to_val_surjective : forall e, exists v, elem_to_val e v.
Axiom elem_to_val_function :
  forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.

Axiom loc_to_elem_injective : is_injective loc_to_elem.

Axiom eq_loc_dec : forall l l' : location, {l = l'} + {l <> l'}.

End STORE_HYPS.

(** ** Store typing *)

Module Store (H : STORE_HYPS).

Export H.

Module Store_world.

Definition value := value.
Definition element := element.
Definition elem_to_val := elem_to_val.
Definition elem_to_val_surjective := elem_to_val_surjective.
Definition elem_to_val_function := elem_to_val_function.

(****)

(** ** Stratified types and store typings *)

Fixpoint stype (n : nat) : Type :=
  match n with
    0   => unit
  | S n => prodT (stype n)
                 (prodT value (location -> optionT (stype n)) -> Prop)
  end.

Definition store_typing n := location -> optionT (stype n).

Inductive stype_sub : forall n n', stype n -> stype n' -> Prop :=
    ps_refl :
      forall n (t : stype n), stype_sub t t
  | ps_incl :
      forall n n' (t : stype n) (t' : stype n')
             (s : prodT value (store_typing n') -> Prop),
      stype_sub t t' -> stype_sub (n' := S n') t (pairT t' s).

Lemma stype_sub_trans :
  forall n n' n'' (t : stype n) (t' : stype n') (t'' : stype n''),
  stype_sub t t' -> stype_sub t' t'' -> stype_sub t t''.
intros n n' n'' t t' t'' H1 H2; generalize H1; clear H1; induction H2;
  [ trivial
  | intro H1; apply ps_incl; auto ].
Qed.

Lemma stype_sub_rank :
  forall n n' (t : stype n) (t' : stype n'),
  stype_sub t t' -> n <= n'.
intros n n' t t' H; induction H; auto.
Qed.

Definition st_sub n n' (ψ : store_typing n) (ψ' : store_typing n') :=
  forall l,
  match ψ l with
    NoneT =>
      True
  | SomeT t =>
      match ψ' l with
        NoneT    => False
      | SomeT t' => stype_sub t' t
      end
  end.

Lemma st_sub_trans :
  forall n n' n'' (ψ : store_typing n) (ψ' : store_typing n')
         (ψ'' : store_typing n''),
  st_sub ψ ψ' -> st_sub ψ' ψ'' -> st_sub ψ ψ''.
intros n n' n'' ψ ψ' ψ'' H1 H2 l;
generalize (H1 l) (H2 l); clear H1 H2; case (ψ l); trivial;
intro t; case (ψ' l); try contradiction;
intro t'; case (ψ'' l); try contradiction;
intros t'' H1 H2; exact (stype_sub_trans H2 H1).
Qed.

Definition st_weaken n (ψ : store_typing (S n)) : store_typing n :=
  fun l =>
  match ψ l with
    NoneT    => NoneT
  | SomeT t  => SomeT (fstT t)
  end.

Lemma st_weaken_and_sub :
  forall n (ψ : store_typing (S n)), st_sub ψ (st_weaken ψ).
intros n ψ l; unfold st_weaken; case (ψ l); trivial; clear ψ;
unfold stype; fold stype; intros (t, s); simpl;
apply (@ps_incl n n t t s); apply ps_refl.
Qed.

Definition st_extend n (ψ : store_typing n) l t : store_typing n :=
  fun l' => if eq_loc_dec l' l then t else ψ l'.

Lemma st_extend_and_sub :
  forall n (ψ : store_typing n) l t,
  ψ l = NoneT -> st_sub ψ (st_extend ψ l t).
intros n ψ l t E l'; unfold st_extend; case (eq_loc_dec l' l);
  [ intro E'; subst l'; rewrite E; trivial
  | intros _; case (ψ l'); trivial;
    intro t'; apply ps_refl ].
Qed.

(****)

(** ** Worlds *)

Record world' : Type :=
  { w_t : nat; w_st : store_typing w_t }.

Definition world := world'.
Definition Build_world := Build_world'.

Definition world_sub w w' := w_t w > w_t w' /\ st_sub (w_st w) (w_st w').

Lemma world_sub_trans : is_transitive world_sub.
intros w w' w'' (H1, H2) (H3, H4); repeat split;
  [ omega
  | exact (st_sub_trans H2 H4) ].
Qed.

Lemma world_sub_well_founded : is_well_founded world_sub.
intros (n, ψ); cut (exists n', n < n');
  [ intros (n', H1); generalize n ψ H1; clear n ψ H1; induction n';
      [ intros n ψ H1; assert False; [ omega | contradiction ]
      | intros n ψ H1; apply accessible_intro; intros (n'', ψ') (H2, H3);
        apply IHn'; simpl in H2; omega ]
  | exists (S n); auto ].
Qed.

End Store_world.

Module C := Core (Store_world).

Export C.

(****)

(** ** Projection / embedding between types to stypes *)

Fixpoint approx n (t : type) {struct n} : stype n :=
  match n return stype n with
    0 =>
      tt
  | (S n) =>
      pairT (approx n t)
        (fun c : prodT value (store_typing n) =>
           let (v, ψ) := c in t (Build_config (Build_world ψ) v))
  end.

Definition to_type n (t : stype n) : type.
induction n;
  [ intros _; exact F
  | simpl; intros (H1, H2) c;
    case (lt_eq_lt_dec n (w_t (c_w c)));
      [ intro s; case s; clear s;
          [ intros _; exact False
          | intro E; subst n; exact (H2 (pairT (c_v c) (w_st (c_w c)))) ]
      | intros _; exact (IHn H1 c) ] ].
Defined.

Lemma approx_prop :
  forall n t c, (w_t (c_w c)) < n -> (t ⇔ to_type (approx n t)) c.
intros n t c; red; induction n; simpl;
  [ intros H1; assert False; [ omega | contradiction ]
  | intros H1; unfold Implies, Conj; case (lt_eq_lt_dec n (w_t (c_w c)));
      [ intro H; case H; clear H;
          [ intros H2; assert False; [ omega | contradiction ]
          | intros E; clear H1 IHn;
            induction c as [(n', ψ)]; simpl in E;
            generalize ψ; clear ψ; case E; auto ]
      | intros H2; apply IHn; trivial ] ].
Qed.

Lemma approx_and_equality :
  forall t c, (∆ teq t (to_type (approx (w_t (c_w c)) t))) c.
intros t c c' H1 v; apply approx_prop; exact (proj1 (proj1 H1)).
Qed.

(****)

(** ** Store typing predicate *)

Definition Get (l : location) (t : type) : type :=
  fun c => match w_st (c_w c) l with
             SomeT t' => t = to_type t'
           | _        => False
           end.

Notation "l ↦ t" := (Get l t) (at level 75, right associativity).

Lemma stype_sub_and_tequiv :
  forall n n' (t : stype n) (t' : stype n') c,
  stype_sub (n:=n') (n':=n) t' t ->
  n' > (w_t (c_w c)) ->
  (to_type t ⇔ to_type t') c.
intros n n' t t' c H1 H2; induction H1;
  [ apply equiv_refl; red; trivial
  | apply equiv_trans with (t2 := to_type t'); split;
      [ clear IHstype_sub; assert (H3 := stype_sub_rank H1);
        split;
          [ red; simpl; case (lt_eq_lt_dec n' (w_t (c_w c)));
              [ intro H; case H; clear H;
                  [ contradiction
                  | intro E; assert False; [ omega | contradiction ] ]
              | trivial ]
          | red; simpl; case (lt_eq_lt_dec n' (w_t (c_w c)));
              [ intro H; case H; clear H;
                  [ intro E; assert False; [ omega | contradiction ]
                  | intro E; assert False; [ omega | contradiction ] ]
              | trivial ] ]
      | apply IHstype_sub; trivial ] ].
Qed.

(* XXX Primitif *)
Lemma get_and_later_1 :
  forall l t1, l ↦ t1 ⊢ ∆(∃t2, l ↦ t2).
intros l t1 ((n, ψ), v); unfold Implies, Get; simpl;
intro H1; cut (exists t3, ψ l = SomeT t3);
  [ intros (t3, E1); generalize H1; clear H1; rewrite E1; intro E; subst t1;
    intros ((n', ψ'), v') ((H1, H2), _);
    generalize (H2 l); simpl; rewrite E1;
    clear H2; intro H2; cut (exists t4, ψ' l = SomeT t4);
      [ intros (t4, E2); generalize H2; clear H2; rewrite E2;
        intros H2; exists (to_type t4); simpl; rewrite E2; trivial
      | induction (ψ' l); try contradiction;
        exists a; trivial ]
  | induction (ψ l); try contradiction;
    exists a; trivial ].
Qed.

(* XXX Primitif *)
Lemma get_and_later_2 :
  forall l t1, l ↦ t1 ⊢ ∆(∀t2, l ↦ t2 ⇒ ∆teq t1 t2).
intros l t1 ((n, ψ), v); unfold Implies, Get; simpl;
intros H1 c H2 t2 H3;
generalize H1 (proj2 (proj1 H2) l); clear H1 H2;
simpl; case (ψ l); try contradiction;
intros t3 E; subst t1; generalize H3; clear H3;
case (w_st (c_w c) l); try contradiction;
intros t4 E H1 (w, v') H2 v''; subst t2;
exact (stype_sub_and_tequiv (c := Build_config w v'') H1 (proj1 (proj1 H2))).
Qed.

(* XXX Primitif *)
Lemma everywhere_get : forall l t, l ↦ t ⊢ EW (l ↦ t).
intros l t w H1 r; trivial.
Qed.

(****)

(** ** Pure types *)

Definition pure p := p ⊢ EW p.

Lemma pure_fold : forall p, pure p -> p ⊢ EW p.
trivial.
Qed.

Hint Resolve pure_fold.

Lemma conj_pure : forall p q, pure p -> pure q -> pure (p ∧ q).
intros p q H1 H2; red; leftapp H2; peek_hyp 1; leftapp H1;
leftapp everywhere_conj; apply everywhere_lift; apply conj_sym.
Qed.

Lemma everywhere_pure : forall p, pure (EW p).
exact everywhere_double.
Qed.

Lemma true_pure : pure T.
exact everywhere_true.
Qed.

Lemma exists_pure :
  forall A (f : A -> type), (forall x, pure (f x)) -> pure (Exists f).
intros A f H; red; apply exists_l; intro x; apply cut with (1 := H x);
apply everywhere_lift; apply exists_r.
Qed.

Lemma later_pure : forall p, pure p -> pure (∆p).
intros p H1; red; rightapp everywhere_later; apply later_lift; exact H1.
Qed.

Lemma get_pure : forall l t, pure (l ↦ t).
exact everywhere_get.
Qed.

Hint Resolve conj_pure everywhere_pure true_pure exists_pure
             later_pure get_pure.

Lemma thas_pure : forall v p, pure (thas v p).
intros l p; unfold thas; auto.
Qed.

Lemma teq_pure : forall t t', pure (teq t t').
intros t t'; unfold teq; auto.
Qed.

Hint Resolve thas_pure teq_pure.

(* XXXX More? *)

(****)

(** ** XXXXX Extra property of thas *)

Lemma thas_tjust :
  forall l f, (forall l, pure (f l)) ->
  thas (loc_to_elem l) (∃l, tjust (loc_to_elem l) ∧ f l) ⊢ f l.
intros l f H1; leftapp thas_e; rightapp everywhere_d;
apply somewhere_l; normalize; intro l';
leftapp H1; apply implies_e; peek_hyp 1;
apply tjust_subst with (g := fun l => EW (f l));
exact loc_to_elem_injective.
Qed.

(****)

(** ** Reference type *)

Definition tref (t : type) : type :=
  ∃l, tjust (loc_to_elem l) ∧ ∃t', l ↦ t' ∧ ∆teq t t'.

Lemma tref_necessary : forall t, necessary (tref t).
unfold necessary, tref; intros t; normalize; intros l t';
peek_hyp 2; leftapp tjust_necessary;
peek_hyp 2; leftapp (@conj_contract (l ↦ t')); normalize;
leftapp get_and_later_1; peek_hyp 1; leftapp get_and_later_2;
do 2 (leftapp conj_assoc_2; leftapp later_conj);
peek_hyp 2; leftapp later_double; leftapp later_conj; apply later_lift;
normalize; intro t'';
rightapp (exists_r (a := l)); rightapp (exists_r (a := t''));
rightapp conj_assoc_2; apply conj_r;
  [ leftapp conj_l_1; leftapp conj_l_1; apply id
  | peek_hyp 1; leftapp (@forall_l _ t'');
    peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
    peek_hyp 2; leftapp conj_l_1;
    leftapp later_conj; apply later_lift; apply teq_trans ].
Qed.

Hint Resolve tref_necessary.

Lemma tref_contractive : contractive tref.
apply contractive'_to_contractive;
intros t t'; unfold tref; normalize; intros l t'';
rightapp (exists_r (a := l));
rightapp (exists_r (a := t''));
repeat apply conj_r;
  [ peek_hyp 2; apply conj_l_2
  | peek_hyp 1; apply conj_l_2
  | peek_hyp 1; leftapp conj_l_1; peek_hyp 1; leftapp conj_l_1;
    leftapp later_conj; apply later_lift; peek_hyp 1; leftapp teq_sym;
    peek_hyp 1; apply teq_trans ].
Qed.

Lemma thas_tref :
  forall l t,
  thas (loc_to_elem l) (tref t) ⊢ ∃t', l ↦ t' ∧ ∆teq t t'.
intros l t; unfold tref;
apply (@thas_tjust l (fun l => ∃t', l ↦ t' ∧ ∆teq t t')); auto.
Qed.

(****)

(** ** The memory *)

Definition memory := location -> element.

Definition mem_set (mem : memory) (l : location) (e : element) : memory :=
  fun l' => if (eq_loc_dec l' l) then e else mem l'.

Lemma mem_set_eq : forall m l e, mem_set m l e l = e.
intros m l e; unfold mem_set; case (eq_loc_dec l l); trivial;
intro H; case H; trivial.
Qed.

Lemma mem_set_not_eq : forall m l l' e, l' <> l -> mem_set m l e l' = m l'.
intros m l l' e H; unfold mem_set; case (eq_loc_dec l' l); trivial;
intros E; case (H E).
Qed.

Definition validmem (m : memory) := ∀l, ∀t, l ↦ t ⇒ ∆thas (m l) t.

(****)

(** ** Type preservation *)

Lemma memory_type_preservation :
  forall l t e, l ↦ t ∧ ∆thas e t ⊢ ∆ ∀t', l ↦ t' ⇒ ∆thas e t'.
intros l t e;
leftapp later_double; peek_hyp 1; leftapp get_and_later_2;
leftapp later_conj; apply later_lift; normalize; intro t';
apply forall_r; intro t''; normalize;
peek_hyp 1; leftapp (@forall_l _ t'');
peek_hyp 1; leftapp conj_assoc_2; leftapp implies_l;
peek_hyp 1; apply change_type.
Qed.

Lemma unchanged_memory :
  forall m n (ψ : store_typing (1 + n)) v,
  (validmem m) (Build_config (Build_world ψ) v) ->
  exists ψ' : store_typing n,
  world_sub (Build_world ψ) (Build_world ψ') /\
  (validmem m) (Build_config (Build_world ψ') v).
intros m n ψ v H1; exists (st_weaken ψ); split;
  [ split; auto;
    simpl; apply st_weaken_and_sub
  | intros l t H2; cut (exists t', ψ l = SomeT t');
      [ intros (t', H3);
        assert (H4 : (l ↦ to_type t') (Build_config (Build_world ψ) v));
          [ unfold Get; simpl; rewrite H3; trivial
          | apply
              (fun H => memory_type_preservation (conj H4 (H1 _ _ H4)) H H2);
            repeat split; auto;
            simpl; apply st_weaken_and_sub ]
      | red in H2; simpl in H2; unfold st_weaken in H2;
        induction (ψ l); try contradiction;
        exists a; trivial ] ].
Qed.

Lemma memory_update :
  forall m l e t n (ψ : store_typing (1 + n)) v,
  necessary t ->
  (validmem m) (Build_config (Build_world ψ) v) ->
  (thas (loc_to_elem l) (tref t)) (Build_config (Build_world ψ) v) ->
  (thas e t) (Build_config (Build_world ψ) v) ->
  exists ψ' : store_typing n,
  world_sub (Build_world ψ) (Build_world ψ') /\
  (validmem (mem_set m l e)) (Build_config (Build_world ψ') v).
intros m l e t n ψ v H1 H2 H3 H4; exists (st_weaken ψ); split;
  [ split; auto;
    simpl; apply st_weaken_and_sub
  | intros l' t' H5; case (eq_loc_dec l' l);
      [ intro E; subst l'; rewrite mem_set_eq;
        generalize (thas_tref H3); clear H3; intros (t'', (H6, H7));
        assert (H8 := change_type (conj H7 (thas_necessary H1 H4)));
        apply (fun H => memory_type_preservation (conj H6 H8) H H5);
        repeat split; auto;
        simpl; apply st_weaken_and_sub
      | intro H6; rewrite (mem_set_not_eq m e H6); clear l t H1 H3 H4 H6;
        cut (exists t, ψ l' = SomeT t);
          [ intros (t, H3);
            assert (H4 : (l' ↦ to_type t) (Build_config (Build_world ψ) v));
              [ unfold Get; simpl; rewrite H3; trivial
              | apply (fun H =>
                         memory_type_preservation (conj H4 (H2 _ _ H4)) H H5);
                repeat split; auto;
                simpl; apply st_weaken_and_sub ]
          | red in H5; simpl in H5; unfold st_weaken in H5;
            induction (ψ l'); try contradiction;
            exists a; trivial ] ] ].
Qed.

Lemma memory_allocation :
  forall m l e t n (ψ : store_typing (1 + n)) v,
  necessary t ->
  (validmem m) (Build_config (Build_world ψ) v) ->
  ψ l = NoneT ->
  (thas e t) (Build_config (Build_world ψ) v) ->
  exists ψ' : store_typing n,
  world_sub (Build_world ψ) (Build_world ψ') /\
  (validmem (mem_set m l e)) (Build_config (Build_world ψ') v) /\
  (thas (loc_to_elem l) (tref t)) (Build_config (Build_world ψ') v).
intros m l e t n ψ v H1 H2 H3 H4;
pose (ψ' := st_extend (st_weaken ψ) l (SomeT (approx n t))); exists ψ';
assert (G1 : world_sub (Build_world ψ) (Build_world ψ'));
  [ split; auto;
    simpl; apply st_sub_trans with (ψ' := st_weaken ψ);
       [ apply st_weaken_and_sub
       | unfold ψ'; apply st_extend_and_sub;
         unfold st_weaken; rewrite H3; trivial ]
  | repeat (split; auto);
      [ intros l' t' H5; case (eq_loc_dec l' l);
          [ intro E; subst l'; rewrite mem_set_eq;
            unfold ψ' in H5; red in H5; simpl in H5; unfold st_extend in H5;
            induction (eq_loc_dec l l);
              [ clear a; simpl in H5; subst t';
                assert (G2 := @approx_and_equality t
                                 (Build_config (Build_world ψ') v));
                assert (G3 : config_sub (Build_config (Build_world ψ) v)
                                        (Build_config (Build_world ψ') v));
                  [ split; trivial
                  | assert (G4 := later_double (thas_necessary H1 H4) G3);
                    exact (change_type (conj G2 G4)) ]
              | case b; trivial ]
          | intro H6; rewrite (mem_set_not_eq m e H6); clear H1 H3 H4;
            cut (exists t'', ψ l' = SomeT t'');
              [ intros (t'', H3);
                assert (H4 : (l' ↦ to_type t'')
                             (Build_config (Build_world ψ) v));
                  [ unfold Get; simpl; rewrite H3; trivial
                  | apply (fun H => memory_type_preservation
                                      (conj H4 (H2 _ _ H4)) H H5);
                    split; auto ]
              | red in H5; simpl in H5; unfold ψ' in H5;
                unfold st_weaken in H5; unfold st_extend in H5;
                induction (eq_loc_dec l' l);
                  [ case (H6 a)
                  | induction (ψ l'); try contradiction;
                    exists a; trivial ] ] ]
      | intros v' H5; exists l; split; trivial;
        exists (to_type (approx n t)); split;
          [ red; simpl; unfold ψ'; unfold st_extend;
            case (eq_loc_dec l l); trivial;
            intro H; case H; trivial
          | exact (@approx_and_equality t
                      (Build_config (Build_world ψ') v')) ] ] ].
Qed.

Lemma memory_access :
  forall w w' v l t m,
  (thas (loc_to_elem l) (tref t)) (Build_config w v) ->
  (validmem m) (Build_config w v) ->
  world_sub w w' ->
  (thas (m l) t) (Build_config w' v).
intros w w' v l t m H1 H2 H3;
generalize (thas_tref H1); intros (t', (H4, H5));
apply (change_type (conj (later_lift (@teq_sym _ _) H5) (H2 _ _ H4)));
split; trivial.
Qed.

(** ** End of store definitions and properties *)

End Store.

(****)

(** * Van Neuman machines *)

Module Store_hyps.

Parameter register : Type.
Definition element := nat.
Definition location := element.
Definition value := register -> element.

Axiom eq_reg_dec : forall r r' : register, {r = r'} + {r <> r'}.

Definition reg_set (v : value) r e :=
  fun r' => if (eq_reg_dec r' r) then e else v r'.

Lemma reg_set_eq : forall v r e, reg_set v r e r = e.
intros v r e; unfold reg_set; case (eq_reg_dec r r); trivial;
intro E; case E; trivial.
Qed.

Lemma reg_set_not_eq :
  forall v r1 r2 e, r2 <> r1 -> reg_set v r1 e r2 = v r2.
intros v r1 r2 e; unfold reg_set; case (eq_reg_dec r2 r1); trivial;
intros E H1; case (H1 E).
Qed.

Definition loc_to_elem (n : location) := n.

Lemma loc_to_elem_injective :
  forall l l', loc_to_elem l = loc_to_elem l' -> l = l'.
trivial.
Qed.

Lemma eq_loc_dec : forall l l' : location, {l = l'} + {l <> l'}.
exact eq_nat_dec.
Qed.

Module Vect.

Parameter r0 : register.

Definition vect e : value := fun r => e.

Definition elem_to_val e v := v = vect e.

Lemma elem_to_val_surjective : forall e, exists v, elem_to_val e v.
intros e; exists (vect e); red; trivial.
Qed.

Lemma elem_to_val_function :
  forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
unfold elem_to_val; intros e e' v H1 H2; subst v;
change e with (vect e r0); rewrite H2; trivial.
Qed.

(* This implies that all types are scalar types! *)
Lemma elem_to_val_rev_fun :
  forall e v v', elem_to_val e v -> elem_to_val e v' -> v = v'.
unfold elem_to_val; intros; subst; trivial.
Qed.

End Vect.

Module Proj.

Parameter r0 : register.

Definition vect e : value := fun r => e.

Definition elem_to_val e (v : value) := v r0 = e.

Lemma elem_to_val_surjective : forall e, exists v, elem_to_val e v.
intros e; exists (vect e); red; trivial.
Qed.

Lemma elem_to_val_function :
  forall e e' v, elem_to_val e v -> elem_to_val e' v -> e = e'.
unfold elem_to_val; intros; subst; trivial.
Qed.

End Proj.

Definition elem_to_val := Vect.elem_to_val.
Definition elem_to_val_surjective := Vect.elem_to_val_surjective.
Definition elem_to_val_function := Vect.elem_to_val_function.

End Store_hyps.

Module S := Store (Store_hyps).

Export S.

(****)

(** ** Safety *)

Parameter step : value -> memory -> value -> memory -> Prop.

Fixpoint safen (n : nat) (v : value) (m : memory) {struct n} : Prop :=
  match n with
    0   => True
  | S n => (exists v', exists m', step v m v' m') /\
           forall v' m', step v m v' m' -> safen n v' m'
  end.

Definition safemem m : type := fun c => safen (w_t (c_w c)) (c_v c) m.

Definition safe : type := ∀m, validmem m ⇒ safemem m.

(****)

Definition tslot r t : type := fun c => (thas (c_v c r) t) c.

(* XXX Primitive *)
Lemma later_tslot : forall r t, tslot r (∆t) ⊢ ∆tslot r t.
intros r t (w, v) H1 (w', v') (H2, E); red; rewrite E;
exact (later_thas H1 (conj H2 E)).
Qed.

(* XXX Primitive *)
Lemma tslot_lift : forall r s t, s ⊢ t -> tslot r s ⊢ tslot r t.
intros r s t H1 w H2; exact (thas_lift H1 H2).
Qed.

Lemma tslot_necessary : forall r t, necessary t -> necessary (tslot r t).
intros r t H1; red; rightapp later_tslot; apply tslot_lift; trivial.
Qed.

Hint Resolve tslot_necessary.

Lemma tslot_exists_1 :
  forall A r (f : A -> type), (∃x, tslot r (f x)) ⊢ tslot r (Exists f).
intros A r f c; exact (@thas_exists_1 _ (c_v c r) f c).
Qed.

Lemma tslot_exists_2 :
  forall A r (f : A -> type),
  (forall x, scalar_type (f x)) ->
  tslot r (Exists f) ⊢ ∃x, tslot r (f x).
intros A r f H0 c; exact (@thas_exists_2 _ (c_v c r) _ H0 c).
Qed.

(* LOW *)
Lemma tslot_thas :
  forall r t w v,
  (tslot r t) (Build_config w v) -> (thas (v r) t) (Build_config w v).
trivial.
Qed.

(****)

(** ** Code pointer *)

Parameter pc : register.

Definition tcodeptr (t : type) : type :=
  ∃l, tjust l ∧ ∆EW(tslot pc (tjust l) ⇒ t ⇒ safe).

Lemma tcodeptr_necessary : forall p, necessary (tcodeptr p).
unfold tcodeptr; auto.
Qed.

Lemma tcodeptr_contravariant :
  forall s t, ∆EW(s ⇒ t) ⊢ tcodeptr t ⇒ tcodeptr s.
intros s t; unfold tcodeptr; normalize; intro l;
rightapp (exists_r (a := l)); peek_hyp 1; apply conj_r;
  [ apply conj_l_2
  | leftapp conj_l_1; leftapp later_conj; apply later_lift;
    leftapp everywhere_conj; apply everywhere_lift; normalize;
    peek_hyp 2; peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
    peek_hyp 2; peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
    apply implies_l ].
Qed.

Lemma tcodeptr_contractive : contractive tcodeptr.
apply contractive'_to_contractive; intros s t; unfold tcodeptr; normalize;
intros l; rightapp (exists_r (a := l)); apply conj_r;
  [ leftapp conj_l_1; apply conj_l_2
  | peek_hyp 1; leftapp conj_l_1; leftapp later_conj; apply later_lift;
    leftapp everywhere_conj; apply everywhere_lift; normalize;
    peek_hyp 2; peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
    unfold Equiv; peek_hyp 2; peek_hyp 2;
    leftapp conj_assoc_2; leftapp implies_l;
    leftapp conj_assoc_2; leftapp implies_l;
    apply conj_l_2 ].
Qed.

(****)

(** ** Machine Instructions *)

Definition machine_instruction := value -> memory -> value -> memory -> Prop.

Definition encodes n (i : machine_instruction) :=
  forall v1 m1, m1 (v1 pc) = n ->
  forall v2 m2, (step v1 m1 v2 m2 <-> i v1 m1 v2 m2).

Definition load r1 r2 (n : nat) : machine_instruction :=
  fun v1 m1 v2 m2 =>
    v2 = reg_set (reg_set v1 pc (1 + v1 pc)) r1 (m1 (n + v1 r2)) /\
    m2 = m1.

Definition store r1 (n : nat) r2 : machine_instruction :=
  fun v1 m1 v2 m2 =>
    v2 = reg_set v1 pc (1 + v1 pc) /\
    m2 = mem_set m1 (n + v1 r1) (v1 r2).

Definition addimm r1 r2 (n : nat) : machine_instruction :=
  fun v1 m1 v2 m2 =>
    v2 = reg_set (reg_set v1 pc (1 + v1 pc)) r1 (n + v1 r2) /\
    m2 = m1.

Definition jump r : machine_instruction :=
  fun v1 m1 v2 m2 =>
    v2 = reg_set v1 pc (v1 r) /\
    m2 = m1.

(****)

(** ** Typing Rules *)

Definition tplus (l : location) k (l' : location) : type :=
  fun w => k + l = l'.

Definition toffset k t :=
  ∃l, tjust (loc_to_elem l) ∧ ∃l', tplus l k l' ∧ thas l' t.

Lemma tjust_subst_2 :
  forall A (f : A -> element) (g : A -> type) x x',
  is_injective f -> T ⊢ g x -> tjust (f x) ∧ tjust (f x') ⊢ g x'.
intros A f g x x' H1 H2; apply implies_to_sequent;
leftapp H2; apply implies_i; peek_hyp 1; apply implies_e;
apply (@tjust_subst A); trivial.
Qed.

Lemma tplus_subst :
  forall (f : location -> type) l l' n,
  tplus l n l' ⊢ f (n + l) ⇒ f l'.
unfold tplus; intros f l l' n c E; subst l'; red; trivial.
Qed.

Lemma tplus_subst_2 :
  forall (f : location -> type) l l' n,
  T ⊢ f (n + l) -> tplus l n l' ⊢ f l'.
intros f l l' n H1; apply implies_to_sequent;
leftapp H1; apply implies_i; peek_hyp 1; apply implies_e; apply tplus_subst.
Qed.

Lemma simplify_typing_rule :
  forall i s t,
  (forall l s',
   l ↦ s' ∧ ∆teq (tjust i) s' ∧
   tslot pc (tjust (loc_to_elem l)) ∧ t ⊢
   ∆EW (tslot pc (tjust (1 + l)) ⇒ s ⇒ safe) ⇒ safe) ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr s) ⊢ tcodeptr t.
intros i t' t H1;
unfold tref, toffset, tcodeptr at 2; normalize;
intros l s; rightapp (exists_r (a := loc_to_elem l)); apply conj_r;
  [ do 3 leftapp conj_l_1; apply id
  | peek_hyp 1; leftapp later_double;
    peek_hyp 2; leftapp (@conj_contract (l ↦ s));
    normalize; leftapp get_and_later_1; peek_hyp 1; leftapp get_and_later_2;
    do 3 (leftapp conj_assoc_2; leftapp later_conj);
    peek_hyp 1; leftapp later_tjust; leftapp later_conj; apply later_lift;
    normalize; intros l1 l2 s';
    peek_hyp 6; do 5 (peek_hyp 2; apply implies_e);
    (match goal with |- _ ⊢ ?q => set (p := q) end);
    pattern l1 in (value of p); subst p;
    apply (@tjust_subst_2 location); try exact loc_to_elem_injective;
    apply implies_i; leftapp conj_l_2;
    (match goal with |- _ ⊢ ?q => set (p := q) end);
    pattern l2 in (value of p); subst p;
    apply tplus_subst_2; normalize;
    leftapp (@forall_l _ s'); peek_hyp 1;
    leftapp (@conj_contract (l ↦ s')); normalize;
    peek_hyp 2; peek_hyp 1; leftapp conj_assoc_2; leftapp implies_l;
    peek_hyp 2; peek_hyp 1; leftapp conj_assoc_2; leftapp later_conj;
    leftapp (later_lift (@teq_trans (tjust i) s s'));
    peek_hyp 2;
    leftapp
       (@thas_tjust (1 + l) (fun l => ∆EW (tslot pc (tjust l) ⇒ t' ⇒ safe)));
    auto;
    leftapp pure_fold; auto;
    apply everywhere_lift; normalize;
    peek_hyp 2; apply implies_e; trivial ].
Qed.

Lemma memory_contents :
  forall l s t m,
  l ↦ t ∧ ∆teq s t ∧ validmem m ⊢ ∆SW (tjust (m l) ∧ s).
intros l s t m; unfold validmem;
leftapp (@forall_l _ l); leftapp (@forall_l _ t);
peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
peek_hyp 1; leftapp (later_lift (@teq_sym s t));
peek_hyp 1; leftapp change_type;
apply later_lift; apply thas_e.
Qed.

Lemma simplify_typing_rule_2 :
  forall i (s t : type),
  (forall (l : element) (v : value) n (ψ : store_typing (1 + n))
          (m : memory),
   v pc = l -> m l = i ->
   t (Build_config (Build_world ψ) v) ->
   (validmem m) (Build_config (Build_world ψ) v) ->
   (exists v' : value, (exists m' : memory, step v m v' m')) /\
   forall v' m', step v m v' m' ->
   exists ψ' : store_typing n,
   st_sub ψ ψ' /\ v' pc = 1 + l /\
   s (Build_config (Build_world ψ') v') /\
   validmem m' (Build_config (Build_world ψ') v')) ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr s) ⊢ tcodeptr t.
intros i s t H1; apply simplify_typing_rule; intros l t1;
unfold safe at 2; normalize; apply forall_r; intro m; normalize;
leftapp (@conj_contract (validmem m)); normalize;
peek_hyp 6; peek_hyp 6; leftapp conj_assoc_2; peek_hyp 2; leftapp conj_assoc_2;
leftapp (@memory_contents l (tjust i) t1 m);
intros ((n, ψ), v); induction n; red; red; simpl; trivial; clear IHn;
intros ((((H2, H3), H4), H5), H6);
lapply (H6 (Build_config (Build_world (st_weaken ψ)) v));
  [ intros (v', (H7, H8)); clear H6;
    assert (H6 := elem_to_val_function H7 H8); clear v' H7 H8;
    generalize (thas_e H2); simpl; intros (v', (H7, H8)); clear H2;
    assert (H2 := elem_to_val_function H7 H8); clear v' H7 H8;
    generalize (H1 _ _ _ _ _ H2 H6 H3 H5); clear H2 H3 H5 H6;
    intros (H2, H3); split; trivial; clear H2;
    do 8 red in H4; simpl in H4;
    intros v' m' H2; generalize (H3 _ _ H2);
    intros (ψ', (G1, (G2, (G3, G4))));
    apply (H4 (Build_config (Build_world ψ') v)); trivial;
      [ repeat split; auto
      | red; simpl; rewrite G2; repeat red; trivial ]
  | repeat split; auto;
    simpl; apply st_weaken_and_sub ].
Qed.

Lemma tplus_pure : forall l l' k, pure (tplus l k l').
intros l l' k c H1 v; trivial.
Qed.

Hint Resolve tplus_pure.

Lemma thas_toffset :
  forall l k t, thas l (toffset k t) ⊢ thas (k + l) t.
intros l k t; unfold toffset;
leftapp (@thas_tjust l (fun l' => ∃l'', tplus l' k l'' ∧ thas l'' t)); auto;
normalize; intros l'; apply implies_e;
(match goal with |- _ ⊢ ?q => set (p := q) end);
pattern l' in (value of p); subst p;
apply tplus_subst_2; normalize; apply id.
Qed.

Lemma everywhere_forall :
  forall A (f : A -> type), (∀x, EW(f x)) ⊢ EW (Forall f).
intros A f c H1 v x; apply H1.
Qed.

Lemma forall_pure :
  forall A (f : A -> type), (forall x, pure (f x)) -> pure (Forall f).
intros A f H; red; rightapp everywhere_forall; apply forall_r;
intro x; leftapp (@forall_l _ x); apply H.
Qed.

Hint Resolve forall_pure.

(*XXX*)
Lemma implies_pure :
  forall s t, pure s -> pure t -> pure (s ⇒ t).
intros s t H1 H2; intros ((n, ψ), v) H3 v' H4;
apply H2; apply H3; exact (H1 _ H4 v).
Qed.

Hint Resolve implies_pure.

Lemma validmem_pure : forall m, pure (validmem m).
intros m; unfold validmem; auto.
Qed.

Lemma simple_load_rule :
  forall i r1 r2 k t,
  encodes i (load r1 r2 k) -> r1 <> pc -> necessary t ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr (tslot r1 t)) ⊢
  tcodeptr (tslot r2 (toffset k (tref t))).
intros i r1 r2 k t H1 H2 H3; apply simplify_typing_rule_2;
intros l v n ψ m E1 E2 H4 H5;
rewrite <- E1 in E2; generalize (H1 _ _ E2); clear H1; intro H1;
split;
  [ exists (reg_set (reg_set v pc (1 + v pc)) r1 (m (k + v r2)));
    exists m; apply (fun v m => proj2 (H1 v m)); split; trivial
  | intros v' m' H6;
    generalize (proj1 (H1 _ _) H6); clear H6; intros (E3, E4); subst v' m';
    generalize (unchanged_memory H5); intros (ψ', (H6, H7));
    exists ψ'; repeat split;
      [ exact (proj2 H6)
      | rewrite reg_set_not_eq; auto;
        rewrite reg_set_eq; rewrite E1; trivial
      | red; simpl; rewrite reg_set_eq;
        apply (memory_access (w' := Build_world ψ') (thas_toffset H4) H5);
        trivial
      | apply (validmem_pure H7) ] ].
Qed.

Definition notindom r (φ : type) :=
  forall w v l, φ (Build_config w v) -> φ (Build_config w (reg_set v r l)).

Lemma load_rule :
  forall i r1 r2 k t φ,
  encodes i (load r1 r2 k) -> r1 <> pc -> necessary t -> necessary φ ->
  notindom r1 φ -> notindom pc φ ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr (φ ∧ tslot r1 t)) ⊢
  tcodeptr (φ ∧ tslot r2 (toffset k (tref t))).
intros i r1 r2 k t φ H1 H2 H3 H4 H5 H6; apply simplify_typing_rule_2;
intros l v n ψ m E1 E2 (H7, H8) H9;
rewrite <- E1 in E2; generalize (H1 _ _ E2); clear H1; intro H1;
split;
  [ exists (reg_set (reg_set v pc (1 + v pc)) r1 (m (k + v r2)));
    exists m; apply (fun v m => proj2 (H1 v m)); split; trivial
  | intros v' m' G1;
    generalize (proj1 (H1 _ _) G1); clear G1; intros (E3, E4); subst v' m';
    generalize (unchanged_memory H9); intros (ψ', (G2, G3));
    exists ψ'; repeat split;
      [ exact (proj2 G2)
      | rewrite reg_set_not_eq; auto;
        rewrite reg_set_eq; rewrite E1; trivial
      | apply H5; apply H6; apply (H4 _ H7); split; trivial
      | red; simpl; rewrite reg_set_eq;
        apply (memory_access (w' := Build_world ψ') (thas_toffset H8) H9);
        trivial
      | apply (validmem_pure G3) ] ].
Qed.

Lemma store_rule :
  forall i r1 r2 k t φ,
  encodes i (store r1 k r2) -> necessary t -> necessary φ ->
  notindom pc φ ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr φ) ⊢
  tcodeptr (φ ∧ tslot r1 (toffset k (tref t)) ∧ tslot r2 t).
intros i r1 r2 k t φ H1 H2 H3 H4; apply simplify_typing_rule_2;
intros l v n ψ m E1 E2 ((H5, H6), H7) H8;
rewrite <- E1 in E2; generalize (H1 _ _ E2); clear H1; intro H1;
split;
  [ exists (reg_set v pc (1 + v pc)); exists (mem_set m (k + v r1) (v r2));
    apply (fun v m => proj2 (H1 v m)); split; trivial
  | intros v' m' G1;
    generalize (proj1 (H1 _ _) G1); clear G1; intros (E3, E4); subst v' m';
    red in H6; simpl in H6;
    generalize (memory_update H2 H8 (thas_toffset H6) H7);
    intros (ψ', (G2, G3)); exists ψ'; repeat split;
      [ exact (proj2 G2)
      | rewrite reg_set_eq; rewrite E1; trivial
      | apply H4; apply (H3 _ H5); split; trivial
      | apply (validmem_pure G3) ] ].
Qed.

Definition int := T.

Lemma addimm_rule :
  forall i r1 r2 k t φ,
  encodes i (addimm r1 r2 k) -> r1 <> pc -> necessary t -> necessary φ ->
  notindom r1 φ -> notindom pc φ ->
  tref (tjust i) ∧ ∆toffset 1 (tcodeptr (φ ∧ tslot r1 int)) ⊢
  tcodeptr (φ ∧ tslot r2 int).
intros i r1 r2 k t φ H1 H2 H3 H4 H5 H6; apply simplify_typing_rule_2;
intros l v n ψ m E1 E2 (H7, H8) H9;
rewrite <- E1 in E2; generalize (H1 _ _ E2); clear H1; intro H1;
split;
  [ exists (reg_set (reg_set v pc (1 + v pc)) r1 (k + v r2));
    exists m; apply (fun v m => proj2 (H1 v m)); split; trivial
  | intros v' m' G1;
    generalize (proj1 (H1 _ _) G1); clear G1; intros (E3, E4); subst v' m';
    generalize (unchanged_memory H9); intros (ψ', (G2, G3));
    exists ψ'; repeat split;
      [ exact (proj2 G2)
      | rewrite reg_set_not_eq; auto;
        rewrite reg_set_eq; rewrite E1; trivial
      | apply H5; apply H6; apply (H4 _ H7); split; trivial
      | apply (validmem_pure G3) ] ].
Qed.

Lemma jump_rule :
  forall i r φ,
  encodes i (jump r) -> r <> pc -> necessary φ ->
  notindom pc φ -> tref (tjust i) ∧ ∆toffset 1 (tcodeptr F) ⊢
  tcodeptr (φ ∧ tslot r (tcodeptr φ)).
intros i r φ H1 H2 H3 H4; apply simplify_typing_rule;
intros l t; unfold safe at 2; normalize; apply forall_r; intro m; normalize;
leftapp (@conj_contract (validmem m)); normalize;
peek_hyp 7; peek_hyp 7; leftapp conj_assoc_2; peek_hyp 2; leftapp conj_assoc_2;
leftapp (@memory_contents l (tjust i) t m);
intros ((n, ψ), v); induction n; red; red; simpl; trivial; clear IHn;
intros (((((H5, H6), H7), H8), H9), H0);
lapply (H0 (Build_config (Build_world (st_weaken ψ)) v));
  [ intros (v', (G1, G2)); clear H0;
    assert (H0 := elem_to_val_function G1 G2); clear v' G1 G2;
    generalize (thas_e H5); simpl; intros (v', (G1, G2)); clear H5;
    assert (H5 := elem_to_val_function G1 G2); clear v' G1 G2;
    unfold loc_to_elem in H5; subst i l;
    generalize (H1 _ _ (refl_equal _)); clear H1; intro H1; split;
      [ exists (reg_set v pc (v r)); exists m;
        apply (fun v m => proj2 (H1 v m)); split; trivial
      | intros v' m' G1;
        generalize (proj1 (H1 _ _) G1); clear G1; intros (E3, E4); subst v' m';
        generalize (unchanged_memory H9); intros (ψ', (G2, G3));
        clear H8;
        assert (H8 := fun H => @thas_tjust (v r)
                        (fun l => ∆EW (tslot pc (tjust l) ⇒ φ ⇒ safe)) H _ H7);
        simpl in H8; do 8 red in H8; simpl in H8;
        apply H8 with (c' := Build_config (Build_world ψ') v); auto;
          [ split; trivial
          | red; simpl; rewrite reg_set_eq; repeat red; trivial
          | apply H4; apply (H3 _ H6); split; trivial
          | apply (validmem_pure G3) ] ]
  | repeat split; auto;
    simpl; apply st_weaken_and_sub ].
Qed.

(****)

(** ** Soundness *)

Require Import List.

Definition program := list nat.

Fixpoint nth (n : nat) (p : program) {struct p} : option nat :=
  match n, p with
  | O,   i :: _ => Some i
  | O,   _      => None
  | S m, nil    => None
  | S m, _ :: r => nth m r
  end.

Definition loaded (p : program) (l : location) (v : value) (m : memory) :=
  forall k,
  match nth k p with
    None   => True
  | Some i => m (k + l) = i
  end.

Fixpoint program_type_rec (p : program) (k : nat) {struct p} : type :=
  match p with
    nil      => T
  | cons i r => toffset k (tref (tjust i)) ∧ program_type_rec r (1 + k)
  end.

Definition program_type p := program_type_rec p 0.

Definition prog_st n (p : program) (l : location) : store_typing n :=
  fun l' =>
    if le_lt_dec l l' then
      match nth (l' - l) p with
        Some i => SomeT (approx n (tjust i))
      | None   => NoneT
      end
    else
      NoneT.

Lemma thas_conj : forall l s t, thas l s ∧ thas l t ⊢ thas l (s ∧ t).
intros l s t; unfold thas; leftapp everywhere_conj; apply everywhere_lift;
normalize; apply conj_r;
  [ peek_hyp 2; peek_hyp 1;
    leftapp conj_assoc_2; leftapp implies_l; apply conj_l_2
  | leftapp conj_assoc_2; leftapp implies_l; apply conj_l_2 ].
Qed.

Lemma everywhere_somewhere : forall p, SW p ⊢ EW (SW p).
intros p c H1 v; trivial.
Qed.

Lemma somewhere_pure : forall p, pure (SW p).
exact everywhere_somewhere.
Qed.

Hint Resolve somewhere_pure.

Lemma tplus_r : forall t l k, t ⊢ tplus l k (k + l).
repeat red; trivial.
Qed.

Lemma thas_toffset_2 :
  forall l k t, thas (k + l) t ⊢ thas l (toffset k t).
intros l k t; unfold thas; leftapp everywhere_double; apply everywhere_lift;
normalize; unfold toffset; rightapp (@exists_r _ l); apply conj_r;
  [ apply conj_l_2
  | leftapp conj_l_1; rightapp (@exists_r _ (k + l)); apply conj_r;
      [ apply tplus_r
      | apply id ] ].
Qed.

Lemma program_well_typed :
  forall p l v m n,
  loaded p l v m -> v pc = l ->
  exists ψ : store_typing n,
  (validmem m) (Build_config (Build_world ψ) v) /\
  (tslot pc (program_type p)) (Build_config (Build_world ψ) v).
intros p l v m n H1 H2; unfold tslot; simpl; rewrite H2;
exists (prog_st n p l); split;
  [ intros l' t H3; red in H3; simpl in H3; unfold prog_st in H3;
    induction (le_lt_dec l l'); try contradiction;
    assert (H4 := H1 (l' - l)); induction (nth (l' - l) p); try contradiction;
    subst a0 t;
    assert (H3 : (∆thas (m l') (tjust (m (l' - l + l))))
                 (Build_config (Build_world (prog_st n p l)) v));
      [ replace (l' - l + l) with l';
          [ do 4 red; trivial
          | unfold location, Store_hyps.element; omega ]
      | assert (H4 := @approx_and_equality (tjust (m (l' - l + l)))
                        (Build_config (Build_world (prog_st n p l)) v));
        exact (change_type (conj H4 H3)) ]
  | unfold program_type;
    cut
      (forall p' k,
       (forall i, nth i p' = nth (i + k) p) ->
       thas l (program_type_rec p' k)
         (Build_config (Build_world (prog_st n p l)) v));
      [ intro H; apply H; intro i; rewrite <- (plus_n_O i); trivial
      | induction p';
          [ repeat red; trivial
          | simpl; intros k H3; apply thas_conj; split;
              [ apply thas_toffset_2; intros v' H4; red;
                apply (@exists_r _ (k + l)); split; trivial;
                apply (@exists_r _ (to_type (approx n (tjust a)))); split;
                  [ red; simpl; unfold prog_st;
                    case (le_lt_dec l (k + l)); try (intros; omega);
                    intros _; replace (k + l - l) with k; try omega;
                    generalize (H3 0); simpl; intro E; rewrite <- E; trivial
                  | exact (@approx_and_equality (tjust a)
                             (Build_config (Build_world (prog_st n p l)) v')) ]
              | apply IHp'; intro i;
                replace (i + S k) with (S (i + k)); try omega;
                exact (H3 (1 + i)) ] ] ] ].
Qed.

Theorem soundness :
  forall p l v m n,
  loaded p l v m -> v pc = l -> program_type p ⊢ tcodeptr T ->
  safen n v m.
intros p l v m n H1 H2 H3;
generalize (program_well_typed (1 + n) H1 H2); intros (ψ, (H4, H5));
assert (H6 : thas (v pc) (program_type p) ⊢
             ∆EW (tslot pc (tjust (v pc)) ⇒ safe));
  [ leftapp (thas_lift (e := v pc) H3);
    leftapp
      (@thas_tjust (v pc) (fun l => ∆EW (tslot pc (tjust l) ⇒ T ⇒ safe)));
    auto;
    apply later_lift; apply everywhere_lift;
    normalize; leftapp implies_l;
    apply implies_to_sequent; apply implies_i; peek_hyp 1; apply implies_l
  | generalize (unchanged_memory H4); intros (ψ', (H7, H8));
    apply (fun H => H6 _ H5 (Build_config (Build_world ψ') v) H v);
      [ split; auto
      | repeat red; trivial
      | trivial ] ].
Qed.

(****)

(** ** Isomorphisms regarding code pointers *)

Lemma forall_exists :
  forall A B (f : A -> B -> type),
  (∃x, ∀y, f x y) ⊢ ∀y, ∃x, f x y.
intros A B f; normalize; intro x; apply forall_r; intro y;
rightapp (exists_r (a := x)); apply (@forall_l _ y (f x)).
Qed.

Lemma toto :
  forall A (f : A -> type), tcodeptr (Exists f) ⊢ ∀x, tcodeptr (f x).
intros A f; unfold tcodeptr; normalize; intro l;
apply forall_r; intro x; rightapp (exists_r (a := l)); apply conj_r;
  [ apply conj_l_1
  | leftapp conj_l_2; apply later_lift; apply everywhere_lift;
    normalize; peek_hyp 2; peek_hyp 2; leftapp conj_assoc_2; leftapp implies_l;
    apply implies_e; leftapp (@exists_r _ x f); apply implies_i;
    peek_hyp 1; apply implies_l ].
Qed.

Require Import Classical.

Lemma excluded_middle : forall t, T ⊢ t ∨ (t ⇒ F).
intros t c H; exact (classic (t c)).
Qed.

Lemma forall_and_exists_tjust :
  forall A (x0 : A) (f : location -> A -> type),
  (∀x, ∃l, tjust l ∧ f l x) ⊢ ∃l, tjust l ∧ ∀x, f l x.
intros A x0 f; apply implies_to_sequent;
leftapp (excluded_middle (∃l, tjust l)); apply disj_l;
  [ normalize; intro l; rightapp (exists_r (a := l)); apply conj_r;
      [ apply conj_l_1
      | apply forall_r; intro x;
        leftapp (@forall_l _ x); normalize; intro l';
        apply implies_e; peek_hyp 1;
        apply (@tjust_subst _ loc_to_elem (fun l => f l x) l' l);
        exact loc_to_elem_injective ]
  | normalize; leftapp (@forall_l _ x0);
    assert (H : (∃l, tjust l ∧ f l x0) ⊢ ∃l, tjust l);
      [ normalize; intro l; leftapp conj_l_1; apply exists_r
      | leftapp H; leftapp implies_l; apply false_l ] ].
Qed.

Lemma titi :
  forall A (x0 : A) (f : A -> type),
  (∀x, tcodeptr (f x)) ⊢ tcodeptr (Exists f).
intros A x0 f; unfold tcodeptr;
leftapp (@forall_and_exists_tjust
            _ x0 (fun l x => ∆EW (tslot pc (tjust l) ⇒ f x ⇒ safe)));
normalize; intro l; rightapp (exists_r (a := l)); apply conj_r;
  [ apply conj_l_1
  | leftapp conj_l_2;
    leftapp
      (later_forall (f := fun x => EW (tslot pc (tjust l) ⇒ f x ⇒ safe)));
    apply later_lift;
    leftapp
      (everywhere_forall (f := fun x => tslot pc (tjust l) ⇒ f x ⇒ safe));
    apply everywhere_lift;
    normalize; intro x; do 2 apply implies_e;
    refine (@forall_l _ x _) ].
Qed.

(****************************************************************************)
(*XXXX
- datastructures
- nonexpansiveness, what is contractive and nonexpansive
- Kinds
...
*)