text:
From stdpp Require Export binders strings.
From stdpp Require Import gmap.
From iris.algebra Require Export ofe.
From iris.heap_lang Require Export locations.
From iris.prelude Require Import options.
From melocoton Require Import stdpp_extra.
From melocoton.language Require Import language.
From melocoton.c_interface Require Import defs.
From melocoton.c_lang Require Export lang metatheory.

Local Notation state := (gmap loc heap_cell).

Lemma map_unmap_val l : unmap_val (map Val l) = Some l.
Proof.
  induction l.
  - easy.
  - cbn. rewrite IHl. easy.
Qed.

Local Lemma to_of_class_C e : to_class_C (of_class_C e) = Some e.
Proof.
  destruct e.
  - easy.
  - cbn. rewrite map_unmap_val. easy.
Qed.

Lemma unmap_val_map le lv : unmap_val le = Some lv → map Val lv = le.
Proof.
  induction le in lv|-*.
  - intros H. injection H. intros <-. easy.
  - cbn. destruct a. 2-12:congruence.
    destruct (unmap_val le) eqn:Heq. 2:congruence.
    intros H. injection H. intros <-. cbn. f_equal. now apply IHle.
Qed.

Local Lemma of_to_class_C e c : to_class_C e = Some c → of_class_C c = e.
Proof.
  destruct e; cbn; try congruence.
  - intros H. injection H. intros <-. easy.
  - destruct e. 2-12: congruence. destruct v. destruct l. 1-3: congruence.
    destruct unmap_val eqn:Heq. 2:congruence.
    intros H. injection H. intros <-. cbn. f_equal. now apply unmap_val_map.
Qed.

Local Lemma fill_class (K : list ectx_item) (e:expr) :
  is_Some (to_class_C (fill K e)) → K = nil ∨ ∃ v, to_class_C e = Some (ExprVal v).
Proof.
  intros [v Hv]. revert v Hv. induction K as [|k1 K] using rev_ind; intros v Hv. 1:now left. right.
  rewrite fill_app in Hv.
  destruct k1; cbn in Hv; try congruence.
  + destruct (fill K e) eqn:Heq; cbn in Hv; try congruence. destruct v0. destruct l; cbn in Hv; try congruence.
    revert Hv. edestruct unmap_val eqn:Heq2; try congruence. intros H. injection H. intros <-.
    cbn in IHK. destruct (IHK _ eq_refl) as [->|Hr].
    - cbn in Heq. subst. eexists. cbn. reflexivity.
    - easy.
  + destruct vf. destruct l; cbn in Hv; try congruence. revert Hv. edestruct unmap_val eqn:Heq; try congruence.
    intros H. injection H. intros <-. apply unmap_val_map in Heq.
    assert (In (fill K e) (map Val l)) as [vv [Hvv' Hvv]]%in_map_iff.
    1: rewrite Heq; apply in_app_iff; right; now left.
    destruct (IHK (ExprVal vv)) as [Hl|Hr].
    - rewrite <- Hvv'. easy.
    - subst. cbn in *. subst. eexists. cbn. reflexivity.
    - easy.
Qed.

Local Notation to_val e :=
  (match to_class_C e with Some (ExprVal v) => Some v | _ => None end).

Local Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof.
  intros. eapply (of_to_class_C e (ExprVal v)).
  repeat case_match; by simplify_eq.
Qed.

Local Lemma to_val_funcall fn vs :
  to_val (FunCall fn vs) = None.
Proof.
  repeat (case_match; simplify_eq; cbn in * ); eauto.
Qed.

Local Hint Resolve to_val_funcall : core.

Local Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
Proof.
  intros [? HH]. case_match; simplify_eq.
  case_match; simplify_eq.
  pose proof (mk_is_Some _ _ H) as H2.
  apply fill_class in H2 as [->|[? ->]]; last done.
  rewrite /= H //.
Qed.

Local Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
Proof.
  intros HH. destruct (to_val (fill K e)) eqn:Heq; try done.
  destruct (fill_val K e); try done. congruence.
Qed.

Local Lemma fill_comp_item k K e : fill (k :: K) e = fill K (fill_item k e).
Proof. reflexivity. Qed.

Local Lemma fill_tail k K e e' :
  to_val e = None →
  to_val e' = None →
  fill_item k e = fill K e' →
  K = [] ∨ ∃ K', K = K' ++ [k] ∧ e = fill K' e'.
Proof.
  intros He He'.
  destruct K.
  + intros _. now left.
  + destruct (@exists_last _ (e0::K)) as (L & l & Hl); first congruence.
    rewrite Hl. unfold fill.
    rewrite foldl_snoc. cbn. intros H. pose proof H as H_copy.
    apply fill_item_no_val_inj in H_copy as ->.
    2: easy.
    2: { destruct (to_val (foldl (flip fill_item) e' L)) eqn:Heq; last done.
         edestruct (fill_val L e'). 1: eexists; apply Heq. congruence. }
    right. eexists. split; first done. now apply fill_item_inj in H.
Qed.

Local Lemma fill_inj K : Inj (=) (=) (fill K).
Proof.
  intros e1 e2.
  induction K as [|Ki K IH] in e1, e2 |- *; rewrite /Inj; first done.
  rewrite !fill_comp_item. by intros ?%IH%fill_item_inj.
Qed.

Local Lemma fill_ctx K s vv K' e :
  fill K' e = fill K (of_class_C (ExprCall s vv)) →
  (∃ v, e = Val v) ∨ (∃ K2, K = K2 ++ K').
Proof. cbn.
  induction K' as [|[] K' IH] in K,e|-*; intros H; first last.
  1-13: destruct  (IH _ _ H) as [(v & Hv)|(K2 & ->)]; try (cbn in *; congruence).
  1-13:  destruct (to_val e) eqn:Heq; first (apply of_to_val in Heq; by left; eexists).
  1-13:  rewrite fill_comp_item in H.
  1-13:  rewrite fill_app in H; apply fill_inj in H.
  1-13:  apply fill_tail in H as H2; try (simplify_eq; eauto; congruence).
  1-13:  destruct H2 as [->|(K3 & -> & HK3)]; try (cbn in *; congruence).
  1-16:  try (right; exists K3; by rewrite <- app_assoc).
  - exfalso. cbn in H. assert (In e (map Val vv)) as Hin.
    + assert (map Val va ++ e :: ve = map Val vv) as <- by congruence.
      apply in_app_iff. right. now left.
    + apply in_map_iff in Hin. destruct Hin as (v & Hv & Hin). rewrite <- Hv in Heq. cbn in Heq. congruence.
  - cbn in H. assert (e = Val (LitV (LitFunPtr s))) as ->; (cbn in *; congruence).
  - cbn. right. eexists. by erewrite app_nil_r.
Qed.

Lemma melocoton_lang_mixin_C :
  @LanguageMixin expr val function (list ectx_item) state
                 of_class_C to_class_C
                 nil comp_ectx fill
                 apply_function head_step.
Proof. split.
  + apply to_of_class_C.
  + apply of_to_class_C.
  + intros *. inversion 1.
  + intros p f vs σ1 e2 σ2. split.
    - intros H. inversion H; subst. inversion H; subst. repeat econstructor; [apply H2|].
      rewrite <- H6. f_equal. eapply map_inj in H1; congruence.
    - intros ([args ee] & H1 & H2 & ->). econstructor; eauto.
  + intros K K' e s' vv Heq.
    destruct (fill_ctx K' s' vv K e) as [(v&HL)|(K2&HK2)].
    - apply Heq.
    - right. exists v. rewrite HL. easy.
    - left. exists K2. easy.
  + intros p1 p2 e1 σ1 e2 σ2 H Hnc.
    inversion H; subst. all: try by econstructor.
    cbn in Hnc. rewrite map_unmap_val in Hnc. congruence.
  + done.
  + intros e; rewrite /comp_ectx app_nil_r //.
  + intros e. easy.
  + intros K1 K2 e. rewrite fill_app //.
  + intros K a b. apply fill_inj.
  + apply fill_class.
  + intros p.
    intros K K' e1 e1' σ1 e2 σ2 Hfill Hred Hstep; revert K' Hfill.
    induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
    destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
    { rewrite fill_app in Hstep. apply head_ctx_step_val in Hstep.
      apply fill_val in Hstep. destruct Hstep as [? Hstep].
      by repeat (case_match; simplify_eq). }
    rewrite !fill_app /= in Hfill.
    assert (Ki = Ki') as ->.
    { eapply fill_item_no_val_inj, Hfill.
      2: { by eapply val_head_stuck, fill_not_val in Hstep. }
      eapply fill_not_val. by destruct e1. }
    simplify_eq. destruct (IH K') as [K'' ->]; auto.
    exists K''. rewrite /comp_ectx assoc //.
  + intros p K e σ1 e2 σ2.
    destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
    rewrite fill_app /=.
    intros [v' ?]%head_ctx_step_val%fill_val. right. exists v'.
    by repeat (case_match; simplify_eq).
Qed.

Canonical Structure C_lang := Language melocoton_lang_mixin_C.

author: logsem

repo: melocoton

save_path: github-repos/coq/logsem-melocoton


text:
(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import Arith Omega Max List.

Require Import notations tac_utils list_utils nat_utils pos.

Set Implicit Arguments.

Section vector.

  Variable X : Type.

  Inductive vec : nat -> Type :=
    | vec_nil  : vec 0
    | vec_cons : forall n, X -> vec n -> vec (S n).

  Let vec_split_type n :=
    match n with
      | 0   => Prop
      | S n => (X * vec n)%type
    end.

  Definition vec_split n (v : vec n) : vec_split_type n :=
    match v in vec k return vec_split_type k with
      | vec_nil  => False
      | @vec_cons n x v => (x,v)
    end.

  Definition vec_head n (v : vec (S n)) := match v with @vec_cons _ x _ => x end.
  Definition vec_tail n (v : vec (S n)) := match v with @vec_cons _ _ w => w end.

(*

  Definition vec_head n (v : vec (S n)) := fst (vec_split v).
  Definition vec_tail n (v : vec (S n)) := snd (vec_split v).

*)

  Let vec_head_tail_type n : vec n -> Prop :=
    match n with
      | 0   => fun v => v = vec_nil
      | S n => fun v => v = vec_cons (vec_head v) (vec_tail v)
    end.

  Let vec_head_tail_prop n v :  @vec_head_tail_type n v.
  Proof. induction v; simpl; auto. Qed.

  Fact vec_0_nil (v : vec 0) : v = vec_nil.
  Proof. apply (vec_head_tail_prop v). Qed.

  Fact vec_head_tail n (v : vec (S n)) : v = vec_cons (vec_head v) (vec_tail v).
  Proof. apply (vec_head_tail_prop v). Qed.

  Fact vec_n0_cons n (v : vec (S n)) : exists x w, v = vec_cons x w.
  Proof.
    exists (vec_head v), (vec_tail v).
    apply vec_head_tail.
  Qed.

  Fixpoint vec_get n (v : vec n) k {struct v} : k < n -> X.
  refine(
    match v in vec q return k < q -> X with
    | vec_nil          => fun H => _
    | @vec_cons n' x w  => match k as q return q < S n' -> X with
                 | 0    => fun _ => x
  	         | S k' => fun H => vec_get _ w k' _
  	    end
    end).
    apply lt_n_0 in H; destruct H.
    apply lt_S_n; assumption.
  Defined.

  Arguments vec_get [ n ] _ _ _.

  Fact vec_get_eq n v x y (Hx : x < n) (Hy : y < n) : x = y -> vec_get v x Hx = vec_get v y Hy.
  Proof.
    intro; subst y.
    revert x Hx Hy.
    induction v; intros a H H'.
    contradict H; omega.
    unfold vec_get; fold vec_get.
    destruct a; trivial.
  Qed.

  Fact vec_get_ext n v w : (forall i Hi, @vec_get n v i Hi = vec_get w i Hi) -> v = w.
  Proof.
    revert w; induction v as [ | n x v IHv ]; intros w H.
    rewrite (vec_0_nil w); auto.
    revert H; rewrite (vec_head_tail w); intros H; f_equal.
    apply (H _ (lt_0_Sn _)).
    apply IHv.
    intros i Hi; generalize (H _ (lt_n_S _ _ Hi)); simpl.
    eqgoal; f_equal; apply vec_get_eq; auto.
  Qed.

  Fact vec_get_cons n x v : forall i (H : S i < S n) (H' : i < n),  vec_get (vec_cons x v) _ H = vec_get v _ H'.
  Proof.
    destruct v as [ | n x' w ]; intros i H.
    contradict H; omega.
    simpl; induction i; intros; trivial.
    apply vec_get_eq; auto.
  Qed.

  Fact vec_get_cons' k (x : X) v i Hi : @vec_get (S k) (vec_cons x v) (S i) Hi = vec_get v i (lt_S_n _ _ Hi).
  Proof.
    apply vec_get_cons.
  Qed.

  Fact vec_get_0 k v H : @vec_get (S k) v 0 H = vec_head v.
  Proof.
    rewrite (vec_head_tail v); reflexivity.
  Qed.

  Fixpoint vec_end n x (v : vec n) : vec (S n) :=
    match v with
      | vec_nil => vec_cons x vec_nil
      | @vec_cons n' y w => vec_cons y (vec_end x w)
    end.

  Fact vec_get_end_0 n x v : forall i (H : i < S n) (H' : i < n), vec_get (@vec_end n x v) _ H = vec_get v _ H'.
  Proof.
    induction v; intros i H H'; try omega.
    simpl vec_end.
    destruct i; simpl; auto.
  Qed.

  Fact vec_get_end_1 n x v : forall (H : n < S n), vec_get (@vec_end n x v) _ H = x.
  Proof.
    induction v; intros H; auto.
    simpl vec_end.
    rewrite vec_get_cons with (H' := lt_S_n _ _ H).
    apply IHv.
  Qed.

  Fixpoint vec_app n (v : vec n) m (w : vec m) : vec (n+m) :=
    match v in vec k return vec (k+m) with
      | vec_nil        => w
      | @vec_cons n x v => vec_cons x (vec_app v w)
    end.

  Fact vec_get_app_l n v m w i (H1 : i < n+m) (H2 : i < n) :
     vec_get (@vec_app n v m w) i H1 = vec_get v _ H2.
  Proof.
    revert i H1 H2.
    induction v as [ | n x v IHv ]; simpl; intros [ | i ] H1 H2;
      try omega; auto.
  Qed.

  Let vec_get_app_r_lt n m i : i < n+m -> n <= i -> i-n < m.
  Proof. abstract omega. Qed.

  Let vec_get_app_rec n v m w i (H1 : i < m) :
      vec_get (@vec_app n v m w) _ (plus_lt_compat_l _ _ _ H1)
    = vec_get w _ H1.
  Proof.
    induction v as [ | n x v IHv ]; simpl.
    apply vec_get_eq; auto.
    rewrite <- IHv.
    apply vec_get_eq; auto.
  Qed.

  Fact vec_get_app_r n v m w i (H1 : i < n+m) (H2 : n <= i) :
    vec_get (@vec_app n v m w) i H1 = vec_get w _ (vec_get_app_r_lt _ H1 H2).
  Proof.
    assert (i-n < m) as H3. abstract omega.
    generalize (vec_get_app_rec v w H3).
    eqgoal; f_equal; apply vec_get_eq; auto.
    omega.
  Qed.

  Fixpoint vec_change n (v : vec n) i (x : X) {struct v}: vec n :=
    match v in vec k, i return vec k with
      | vec_nil        , _   => vec_nil
      | @vec_cons _ _ w , 0   => vec_cons x w
      | @vec_cons _ y w , S i => vec_cons y (vec_change w i x)
  end.

  Fact vec_get_change_eq n a v : forall i (H : i < n), vec_get (vec_change v i a) _ H = a.
  Proof.
    induction v; intros i H.
    exfalso; apply lt_n_0 in H; auto.
    destruct i; simpl; trivial.
  Qed.

  Fact vec_get_change_neq: forall n x v i j (D: i <> j) (H : j < n), vec_get (vec_change v i x) _ H = vec_get v _ H.
  Proof.
    induction v as [ | n y v IHv ]; intros i j D H.
    exfalso; apply lt_n_0 in H; auto.
    destruct i; destruct j; trivial.
    contradict D; trivial.
    simpl; apply IHv.
    contradict D; subst; auto.
  Qed.

  Definition vec_set n : forall (f : forall x, x < n -> X), vec n.
  Proof.
    induction n as [ | n IHn ]; intros f.
    exact vec_nil.
    apply vec_cons with (1 := f _ (lt_O_Sn _)).
    apply IHn.
    intros x Hx.
    apply (f (S x)).
    apply lt_n_S; assumption.
  Defined.

  Fact vec_get_set n f x Hx : vec_get (@vec_set n f) x Hx = f x Hx.
  Proof.
    revert f x Hx; induction n as [ | n IHn ]; intros f x Hx; simpl.
    omega.
    destruct x as [ | x ].
    f_equal; apply le_pirr.
    rewrite IHn; f_equal; apply le_pirr.
  Qed.

  Fact vec_set_get n v : vec_set (@vec_get n v) = v.
  Proof.
    apply vec_get_ext.
    intros; rewrite vec_get_set; auto.
  Qed.

  Fixpoint vec_rev_init (f : nat -> X) n {struct n}: vec n :=
    match n return vec n with
    | 0   => vec_nil
    | S m => vec_cons (f n) (vec_rev_init f _)
    end.

  Definition vec_init f n := vec_rev_init (fun m => f (n-m)) n.

  Fact vec_get_rev_init f n : forall i (H : i < n), vec_get (vec_rev_init f n) _ H = f (n-i).
  Proof.
    induction n; intros i H.
    contradict H; omega.
    destruct i; simpl; trivial.
  Qed.

  Fact vec_get_init f n i (H : i < n) : vec_get (vec_init f n) i H = f i.
  Proof.
    unfold vec_init; intros; rewrite vec_get_rev_init.
    f_equal; omega.
  Qed.

  Definition vec_repeat x := vec_init (fun _ => x).

  Proposition vec_repeat_prop x : forall n i (Hi : i < n), vec_get (vec_repeat x n) _ Hi = x.
  Proof. apply vec_get_init. Qed.

  Section vec_fall.

    Variable P : X -> Prop.

    Definition vec_fall n (v : vec n) := forall x H, P (vec_get v x H).

    Theorem vec_fall_nil : vec_fall vec_nil.
    Proof. intros ? ?; exfalso; omega. Qed.

    Theorem vec_fall_cons n x (l : vec n) : vec_fall (vec_cons x l) <->  (P x /\ vec_fall l).
    Proof.
      split.

      intros H1; split.
      generalize (H1 _ (lt_O_Sn _)); auto.
      intros i Hi.
      generalize (lt_n_S _ _ Hi); intros Hx'.
      generalize (H1 _ Hx').
      simpl.
      match goal with |- P ?x -> P ?y => cutrewrite (x=y); auto end.
      apply vec_get_eq; auto.
      intros [ H1 H2 ] [ | y ] Hy; simpl; auto.
    Qed.

  End vec_fall.

End vector.

Hint Resolve vec_get_eq.

Arguments vec_get [ X n ] _ _ _.

Section vector_max.

  Fixpoint vec_max n l : nat :=
    match l with
      | vec_nil _      => 0
      | vec_cons  a l => max a (vec_max _ l)
    end.

  Fact vec_get_max n l : forall i (H : i < n), vec_get l i H <= vec_max l.
  Proof.
   induction l; intros i H.
   contradict H; omega.
   induction i; simpl.
   apply le_max_l.
   apply le_trans with (2 := le_max_r _ _).
   apply IHl.
  Qed.

  Fact vec_max_eq_n0 n (l : vec _ n) : 0 < n -> { i : nat & { H : i < n | vec_get l i H = vec_max l }}.
  Proof.
    induction l; intros Hn.
    contradict Hn; omega.
    induction n.
    exists 0. exists (le_refl _).
    rewrite (vec_0_nil l); simpl; rewrite max_l; omega.
    clear IHn. destruct IHl as [ i [ Hi IH ] ]; [ omega | idtac ].
    destruct (max_dec x (vec_max l)) as [ H | H ].
    exists 0. exists Hn. simpl. omega.
    exists (S i). exists (lt_n_S _ _ Hi).
    unfold vec_max; fold vec_max.
    rewrite vec_get_cons with (H' := Hi), IH. auto.
  Qed.

  Fact vec_max_eq_0 (l : vec _ 0) : vec_max l = 0.
  Proof. rewrite (vec_0_nil _); reflexivity. Qed.

  Fact vec_max_lub n : forall (l : vec _ n) m, (forall x Hx, vec_get l x Hx <= m) -> vec_max l <= m.
  Proof.
    induction n; intros l m H.
    rewrite vec_max_eq_0. omega.
    assert (0 < S n) as Hn.
      omega.
    destruct (vec_max_eq_n0 l Hn) as [ i [ Hi H' ] ].
    rewrite <- H'. apply H.
  Qed.

End vector_max.

Section vector_sum.

  Fixpoint vec_sum n l : nat :=
    match l with
      | vec_nil _     => 0
      | vec_cons a l => a + vec_sum _ l
    end.

  Fact vec_set_sum n (f : forall i, i < n -> nat) : finite_sum f = vec_sum (vec_set f).
  Proof.
    revert f; induction n; simpl; auto.
  Qed.

End vector_sum.

(* notations *)

Arguments vec_nil [ X ].

Infix "##" := vec_cons (at level 60, right associativity).

Section vec_pos.

  Variable (X : Type).

  (* If I use pos_S_invert instead of pos_S_inv then vec_pos cannot
     be used in the definition of the recalg_rect fixpoint *)

  Fixpoint vec_pos n (v : vec X n) : pos n -> X.
  Proof.
    refine (match v with
             | vec_nil => fun p => _
             | @vec_cons _ n x v => fun p => _
            end); invert pos p.
    exact x.
    exact (vec_pos _ v p).
  Defined.

  Fact vec_pos0 n (v : vec X (S n)) : vec_pos v pos0 = vec_head v.
  Proof.
    rewrite (vec_head_tail v).
    reflexivity.
  Qed.

  Fact vec_get_pos n v p H : vec_get v (pos2nat p) H = @vec_pos n v p.
  Proof.
    revert p H; induction v as [ | n x v Hv ]; intros p H; invert pos p; auto.
    apply Hv.
  Qed.

  Fact vec_get_pos_eq n v i Hi p : i = pos2nat p -> vec_get v i Hi = @vec_pos n v p.
  Proof.
    intros; subst; apply vec_get_pos.
  Qed.

  Fact vec_pos_tail n (v : vec X (S n)) p : vec_pos (vec_tail v) p = vec_pos v (pos_nxt _ p).
  Proof.
    rewrite vec_head_tail at 2; simpl; auto.
  Qed.

  Fact vec_pos1 n (v : vec X (S (S n))) : vec_pos v pos1 = vec_head (vec_tail v).
  Proof.
    rewrite <- vec_pos0, vec_pos_tail; auto.
  Qed.

  Fact vec_pos_ext n (v w : vec X n) : (forall p, vec_pos v p = vec_pos w p) -> v = w.
  Proof.
    revert v w; induction n as [ | n IHn ]; intros v w H.
    rewrite (vec_0_nil v), (vec_0_nil w); auto.
    revert H; rewrite (vec_head_tail v), (vec_head_tail w); f_equal.
    intros H; f_equal.
    apply (H pos0).
    apply IHn.
    intros p; apply (H (pos_nxt _ p)).
  Qed.

  Fixpoint vec_set_pos n : (pos n -> X) -> vec X n :=
    match n return (pos n -> X) -> vec X n with
      | 0   => fun _ => @vec_nil _
      | S n => fun g => vec_cons (g pos0) (vec_set_pos (fun p => g (pos_nxt _ p)))
    end.

  Fact vec_pos_set n (g : pos n -> X) p : vec_pos (vec_set_pos g) p = g p.
  Proof.
    revert g p; induction n as [ | n IHn ]; intros g p; pos_inv p; auto.
    apply IHn.
  Qed.

  Fact vec_pos_app_lft n m (v : vec X n) (w : vec X m) p : vec_pos (vec_app v w) (pos_lft _ p) = vec_pos v p.
  Proof.
    revert p; induction v; simpl; intros p; pos_inv p; simpl; auto.
  Qed.

  Fact vec_pos_app_rt n m (v : vec X n) (w : vec X m) p : vec_pos (vec_app v w) (pos_rt _ p) = vec_pos w p.
  Proof.
    induction v; simpl; auto.
  Qed.

  Definition vec_lft { n m } (v : vec X (n+m)) : vec X n := vec_set_pos (fun p => vec_pos v (pos_lft _ p)).
  Definition vec_rt { n m } (v : vec X (n+m)) : vec X m := vec_set_pos (fun p => vec_pos v (pos_rt _ p)).

  Fact vec_app_lft_rt n m (v : vec X (n+m)) : v = vec_app (vec_lft v) (vec_rt v).
  Proof.
    apply vec_pos_ext.
    intros p.
    unfold vec_lft, vec_rt.
    destruct (pos_split p) as [ (q & ?) | (q & ?) ]; subst p.
    rewrite vec_pos_app_lft, vec_pos_set; auto.
    rewrite vec_pos_app_rt, vec_pos_set; auto.
  Qed.

End vec_pos.

Fact vec_pos_sum n v p : vec_pos v p <= @vec_sum n v.
Proof.
  revert p; induction v; intros p; pos_inv p; simpl.
  omega.
  apply le_trans with (1 := IHv _); omega.
Qed.

Fact vec_sum_app n m v w : vec_sum (vec_app v w) = @vec_sum n v + @vec_sum m w.
Proof.
  induction v; simpl; auto.
  rewrite IHv; omega.
Qed.

Fact vec_sum_length n v : (forall p, 0 < vec_pos v p) -> n <= @vec_sum n v.
Proof.
  induction v; simpl; auto.
  intros H.
  generalize (H pos0) (fun p => H (pos_nxt _ p)); simpl; intros H1 H2.
  apply IHv in H2; omega.
Qed.

Fact vec_sum_min n v k : k <= n -> (forall i Hi, i < k -> 0 < vec_get v i Hi) -> k <= @vec_sum n v.
Proof.
  revert k.
  induction v; intros [ | k ] Hk H; simpl; auto.
  omega.
  apply le_S_n, IHv in Hk.
  generalize (H 0 (lt_0_Sn _)); simpl; omega.
  intros i H1 H2.
  specialize (H _ (lt_n_S _ _ H1) (lt_n_S _ _ H2)); simpl in H.
  revert H; eqgoal.
Qed.

Definition option_lift X Y (f : X -> Y) x :=
  match x with None => None | Some x => Some (f x) end.

Fact nth_error_map X Y (f : X -> Y) l i : nth_error (map f l) i = option_lift f (nth_error l i).
Proof.
  revert l; induction i; intros []; simpl; auto.
Qed.

Definition tail_error X (l : list X) :=
  match l with
    | nil  => None
    | _::l => Some l
  end.

Definition vec_list X n (v : vec X n) := map (vec_pos v) (pos_list n).

(* Fact vec_list_map X Y (f : X -> Y) n  : *)

Section vec_list.

  Variable X : Type.

  Fact vec_list_0 (v : vec X 0) : vec_list v = nil.
  Proof.
    rewrite (vec_0_nil v); auto.
  Qed.

  Fact vec_list_S n x (v : vec X n) : vec_list (x##v) = x::vec_list v.
  Proof.
    unfold vec_list; simpl; f_equal.
    rewrite map_map; simpl; auto.
  Qed.

  Fact vec_list_tail n (v : vec X (S n)) : tail_error (vec_list v) = Some (vec_list (vec_tail v)).
  Proof.
    rewrite (vec_head_tail v) at 1.
    simpl; rewrite map_map; simpl; auto.
  Qed.

  Fact vec_list_get n (v : vec X _) i (H : i < n) : nth_error (vec_list v) i = Some (vec_get v i H).
  Proof.
    revert v i H; induction n as [ | n IHn ]; intros v i H.
    omega.
    rewrite (vec_head_tail _).
    destruct i as [ | i ].
    unfold vec_list; simpl; auto.
    unfold vec_list; simpl.
    rewrite map_map; simpl.
    rewrite <- IHn; auto.
  Qed.

  Fact vec_list_split n (v : vec X n) k (Hk : k < n) : exists l r, vec_list v = l++vec_get v k Hk::r /\ k = length l.
  Proof.
    revert v k Hk; induction n as [ | n IHn ]; intros v k Hk.
    omega.
    rewrite (vec_head_tail v).
    destruct k as [ | k ].

    exists nil, (vec_list (vec_tail v)).
    rewrite vec_list_S; auto.

    destruct (IHn (vec_tail v) k (lt_S_n _ _ Hk)) as (l & r & H).
    exists (vec_head v::l), r.
    rewrite vec_list_S; simpl; split; f_equal; tauto.
  Qed.

End vec_list.

Section vector_map.

  Variables A B: Type.

  Section def.

    Variable f : A -> B.

    Fixpoint vec_map n (l : vec A n) {struct l} : vec B n :=
      match l in vec _ n return vec _ n with
        | vec_nil      => @vec_nil B
        | vec_cons a q => vec_cons (f a) (vec_map q)
      end.

  End def.

  Arguments vec_map f [ n ] _.

  Fact vec_get_map f n l : forall i (H : i < n), vec_get (vec_map f l) _ H = f (vec_get l _ H).
  Proof.
    induction l; intros i H.
    contradict H; omega.
    destruct i; simpl; trivial.
  Qed.

  Fact vec_map_get_ext f g n l : (forall i (H : i < n), f (vec_get l _ H) = g (vec_get l _ H)) -> vec_map f l = vec_map g l.
  Proof.
    induction l; intros H.
    trivial.
    simpl. f_equal.
    assert (0 < S n) as H'.
      omega.
    apply (H _ H').
    apply IHl.
    intros i H'.
    assert (S i < S n) as H''.
      omega.
    generalize (H _ H''); simpl.
    match goal with
      |- ?a = ?b -> _ = _ => transitivity a; [ idtac | transitivity b ]
    end; auto; f_equal; auto.
  Qed.

  Fact vec_pos_map f n v (p : pos n) : vec_pos (vec_map f v) p = f (vec_pos v p).
  Proof.
    revert p; induction v; intros p; pos_inv p; simpl; auto.
  Qed.

End vector_map.

Arguments vec_get_map [ A B ] f [ n ] _ _ _.

Fact vec_map_map A B C (f : A -> B) (g : B -> C) n (v : vec A n) :
    vec_map g (vec_map f v) = vec_map (fun x => g (f x)) v.
Proof.
  induction v; simpl; f_equal; auto.
Qed.

Section vector_instanciate.

  Variable A B : Type.

  Definition vec_inst n (l : vec (A->B) n) (a : A) := vec_map (fun f => f a) l.

  Fact vec_get_inst n l : forall a i (H : i < n), vec_get (vec_inst l a) i H = vec_get l i H a.
  Proof. intros; apply vec_get_map. Qed.

End vector_instanciate.

Section vec_swap.

  Variable (X : Type) (n : nat).

  Definition vec_swap (v : vec X (S (S n))) := vec_set_pos (fun p => vec_pos v (pos_swap p)).

  Fact vec_pos0_swap v : vec_pos (vec_swap v) pos0 = vec_pos v pos1.
  Proof.
    unfold vec_swap; rewrite vec_pos_set; auto.
  Qed.

  Fact vec_pos1_swap v : vec_pos (vec_swap v) pos1 = vec_pos v pos0.
  Proof.
    unfold vec_swap; rewrite vec_pos_set; auto.
  Qed.

  Fact vec_pos_swap v p : vec_pos (vec_swap v) (pos_nxt _ (pos_nxt _ p)) = vec_pos v (pos_nxt _ (pos_nxt _ p)).
  Proof.
    unfold vec_swap; rewrite vec_pos_set; auto.
  Qed.

  Fact vec_head_swap v : vec_head (vec_swap v) = vec_head (vec_tail v).
  Proof.
    rewrite <- vec_pos0; unfold vec_swap; rewrite vec_pos_set; simpl.
    rewrite <- vec_pos_tail, vec_pos0; auto.
  Qed.

  Fact vec_tail_swap v : vec_tail (vec_swap v) = vec_head v ## vec_tail (vec_tail v).
  Proof.
    apply vec_pos_ext; intros p.
    rewrite vec_pos_tail.
    pos_inv p.
    rewrite vec_pos0; auto.
    rewrite vec_pos_set.
    simpl; do 2 rewrite vec_pos_tail; auto.
  Qed.

End vec_swap.

Section vec_reif.

  Variable (n : nat) (X : Type) (R : pos n -> X -> Prop).

  Definition vec_reif : (forall p, exists x, R p x) -> exists v, forall p, R p (vec_pos v p).
  Proof.
    intros H.
    apply pos_reification in H.
    destruct H as (f & Hf).
    exists (vec_set_pos f).
    intro; rewrite vec_pos_set; auto.
  Qed.

End vec_reif.

Fixpoint vec_reif_t X n : forall R : pos n -> X -> Prop, (forall p, {x | R p x}) -> {v | forall p, R p (vec_pos v p) }.
Proof.
  refine (match n with
    | 0   => fun R _  => exist _ vec_nil _
    | S n => fun R HR => match HR pos0 with
      | exist _ x Hx => match vec_reif_t X n (fun p x => R (pos_nxt _ p) x) _ with
        | exist _ v Hv => exist _ (x##v) _
      end
    end
  end).
  intros p; pos_inv p.
  intros; apply HR.
  intros p; pos_inv p; auto.
Defined.

Section pos_choice.

  Fact pos_simple_choice U k (P Q : pos k -> U -> Prop) :
        (forall p, { u | P p u } + { forall u, Q p u })
     -> { u | forall p, P p (vec_pos u p) }
      + { p | forall u, Q p u }.
  Proof.
    revert P Q.
    induction k as [ | k IHk ]; intros P Q HPQ.
    left; exists vec_nil; intro p; pos_inv p.
    destruct (HPQ pos0) as [ (u & Hu) | H0 ].
    destruct (IHk (fun p => P (pos_nxt _ p)) (fun p => Q (pos_nxt _ p)))
      as [ (f & Hf) | (p & Hp) ].
    intros; apply HPQ.
    left; exists (u##f).
    intros p; pos_inv p; simpl; auto.
    right; exists (pos_nxt _ p); auto.
    right; exists pos0; auto.
  Qed.

  Fact pos_double_choice U V k (P Q : pos k -> U -> V -> Prop) :
        (forall p, { u : _ & { v | P p u v } } + { forall u v, Q p u v })
     -> { u : _ & { v | forall p, P p (vec_pos u p) (vec_pos v p) } }
      + { p | forall u v, Q p u v }.
  Proof.
    revert P Q.
    induction k as [ | k IHk ]; intros P Q HPQ.
    left; exists vec_nil, vec_nil; intro p; pos_inv p.
    destruct (HPQ pos0) as [ (u & v & Huv) | H0 ].
    destruct (IHk (fun p => P (pos_nxt _ p)) (fun p => Q (pos_nxt _ p)))
      as [ (f & g & Hfg) | (p & Hp) ].
    intros; apply HPQ.
    left; exists (u##f), (v##g).
    intros p; pos_inv p; simpl; auto.
    right; exists (pos_nxt _ p); auto.
    right; exists pos0; auto.
  Qed.

  Definition pos_reif2_t U V k (P : pos k -> U -> V -> Prop) :
       (forall p, { u : _ & { v | P p u v } }) -> { f : _ & { g | forall p, P p (vec_pos f p) (vec_pos g p) } }.
  Proof.
    intros HP.
    destruct (pos_double_choice P (fun _ _ _ => False)) as [ | (p & Hp) ]; auto.
    destruct (HP p) as (u & v & _); tauto.
  Qed.

End pos_choice.

Section vec_sub.

  Definition vec_sub X n (v : vec X n) i : i < n -> { w : vec X i | forall j H1 H2, vec_get w j H1 = vec_get v j H2 }.
  Proof.
    intros Hi.
    assert (forall p : pos i, pos2nat p < n) as H.
      intro p; apply lt_trans with (2 := Hi), (pos2nat_prop p).
    exists (vec_set_pos (fun p => vec_get v (pos2nat p) (H p))).
    intros j H1 H2.
    rewrite vec_get_pos_eq with (p := nat2pos H1),
            vec_pos_set.
    apply vec_get_eq; rewrite pos2nat_nat2pos; auto.
    rewrite pos2nat_nat2pos; auto.
  Qed.

  Definition vec_positive_sub n (v : vec nat n) : { i : _ & { H : i < n & { w : vec nat i | vec_get v _ H = 0
                                                                    /\ forall j H1 H2, vec_get v j H1 = S (vec_get w j H2) } } }
                                                + { forall i Hi, 0 < vec_get v i Hi }.
  Proof.
    induction v as [ | n [ | x ] v IHv ].
    right; intros; omega.
    left; exists 0, (lt_0_Sn _), vec_nil; simpl; split; auto; intros; omega.
    destruct IHv as [ (i & Hi & w & H1 & H2) | IHv ].
    left; exists (S i), (lt_n_S _ _ Hi), (x##w); split; simpl.
    revert H1; eqgoal; auto.
    intros [ | ] ?; auto.
    right. intros [|] ?; simpl; auto; omega.
  Qed.

End vec_sub.

Section vec_strict_pos.

  Definition vec_strict_pos n (v : vec nat n) : (forall p, 0 < vec_pos v p) + { p | 0 = vec_pos v p }.
  Proof.
    induction v as [ n | n [ | x ] v IHv ].
    left; intros p; pos_inv p.
    right; exists pos0; auto.
    destruct IHv as [ IHv | (p & Hp) ].
    left; intros p; pos_inv p; simpl; auto; omega.
    right; exists (pos_nxt _ p); auto.
  Qed.

End vec_strict_pos.

author: DmxLarchey

repo: Coq-is-total


text:
(**
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Solange Coupet-Grimal and William Delobel, 2006-01-09

Axiomatic definition of RPO, and hypotheses taken to prove
strict order, monotonicity, well-foundedness
*)

From CoLoR Require Import VPrecedence ListUtil VTerm RelMidex LogicUtil AccUtil.
From Coq Require Import Relations Morphisms Basics.
From CoLoR Require AccUtil ListUtil MultisetListOrder ListLex.

Module Type RPO_Model.

  Declare Module Export P : VPrecedenceType.

  Parameter tau : Sig -> relation term -> relation terms.

  Parameter tau_dec : forall f R ts ss,
    (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) ->
    {tau f R ts ss} + {~tau f R ts ss}.

  Parameter status_eq : forall f g, f =F= g -> tau f = tau g.

  Parameter lt : relation term.

  Parameter lt_roots : forall f g, g <F f ->
    forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) ->
      lt (Fun g ts) (Fun f ss).

  Parameter lt_status : forall f g, f =F= g ->
    forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) ->
      tau f lt ts ss -> lt (Fun g ts) (Fun f ss).

  Parameter lt_subterm : forall f ss t,
    ex (fun s => In s ss /\ (s = t \/ lt t s)) -> lt t (Fun f ss).

  Parameter lt_decomp : forall s t, lt s t ->
    ((ex (fun f => ex (fun g => ex (fun ss => ex (fun ts =>
      ltF f g /\
      (forall s, In s ss -> lt s (Fun g ts)) /\
      s = Fun f ss /\
      t = Fun g ts
    )))))
    \/
    ex (fun f => ex (fun g => ex (fun ss => ex (fun ts =>
      f =F= g /\
      (forall s, In s ss -> lt s (Fun g ts)) /\
      tau f lt ss ts /\
      s = Fun f ss /\
      t = Fun g ts)))))
    \/
    ex (fun f => ex (fun ts => ex (fun t' =>
      In t' ts /\ (s = t' \/ lt s t')) /\ t = Fun f ts)).

  Parameter SPO_to_status_SPO : forall f (r : relation term) ss,
    (forall s, In s ss -> (forall t u, r s t -> r t u -> r s u)
      /\ (r s s -> False)) ->
    (forall ts us, tau f r ss ts -> tau f r ts us -> tau f r ss us)
    /\ (tau f r ss ss -> False).

  Parameter mono_axiom : forall f (r : relation term),
    forall ss ts, one_less r ss ts -> tau f r ss ts.

  Import AccUtil ListUtil.

  Definition lifting R := forall l, Accs lt l -> Restricted_acc (Accs lt) R l.

  Parameter leF_dec : rel_dec leF.

  Parameter wf_ltF : well_founded ltF.

  Parameter status_lifting : forall f, lifting (tau f lt).

(*
  Parameter status_homomorphic : forall F ss ts f,
    (forall s t, In s ss -> In t ts -> lt s t -> lt (F s) (F t)) ->
    tau f lt ss ts -> tau f lt (map F ss) (map F ts).
*)

  Ltac lt_inversion_cases H :=
    match type of H with
      | lt ?s ?t =>
        let Hr := (fresh "case_roots") in
          let Hs := (fresh "case_status") in
            let Ht := (fresh "case_subterm") in
              let Hdum := (fresh "case_hdum") in
              (elim (lt_decomp s t H);
                [intro Hdum; elim Hdum; clear Hdum;
                  [intro Hr | intro Hs] | intro Ht])
      | _ => fail 10 "Hyp should be ~ lt s t"
    end.

  Ltac inversion_case_root H :=
    let f := fresh "f" in let g := fresh "g" in
      let ss := fresh "ss" in let ts := fresh "ts" in
        let ltFfg := fresh "ltFfg" in let Hsub := fresh "Hsub" in
          let s_is := fresh "s_is" in let t_is := fresh "t_is" in
            (elim H; clear H; intros f H;
              elim H; clear H; intros g H;
                elim H; clear H; intros ss H;
                  elim H; clear H; intros ts H;
                    elim H; clear H; intros ltFfg H;
                      elim H; clear H; intros Hsub H;
                        elim H; clear H; intros s_is t_is).

  Ltac inversion_case_status H :=
    let f := fresh "f" in let g := fresh "g" in
      let ss := fresh "ss" in let ts := fresh "ts" in
        let eqFfg := fresh "eqFfg" in let Hsub := fresh "Hsub" in
          let Hstat := fresh "Hstat" in let s_is := fresh "s_is" in
            let t_is := fresh "t_is" in
              (elim H; clear H; intros f H;
                elim H; clear H; intros g H;
                  elim H; clear H; intros ss H;
                    elim H; clear H; intros ts H;
                      elim H; clear H; intros eqFfg H;
                        elim H; clear H; intros Hsub H;
                          elim H; clear H; intros Hstat H;
                            elim H; clear H; intros s_is t_is).

  Ltac inversion_case_subterm H :=
    let f := fresh "f" in let ts := fresh "ts" in
      let Hex := fresh "Hex" in let t' := fresh "t'" in
        let Ht' := fresh "Ht'" in let t'_in_ts := fresh "t'_in_ts" in
          let t_is := fresh "t_is" in
            (elim H; clear H; intros f H;
              elim H; clear H; intros ts H;
                elim H; clear H; intros Hex t_is;
                  elim Hex; clear Hex; intros t' Ht';
                    elim Ht'; clear Ht'; intros t'_in_ts Ht').

  Ltac lt_inversion H :=
    match type of H with
      | lt ?s ?t =>
        let Hr := (fresh "case_roots") in
          let Hs := (fresh "case_status") in
            let Ht := (fresh "case_subterm") in
              let Hdum := (fresh "case_hdum") in
              (elim (lt_decomp s t H);
                [intro Hdum; elim Hdum; clear Hdum;
                  [intro Hr | intro Hs] | intro Ht];
                [(* Hr : *)
                  inversion_case_root Hr
                  | (* Hs : *)
                    inversion_case_status Hs
                  | (* Ht : *)
                    inversion_case_subterm Ht
                ])
      | _ => fail 10 "Hyp should be ~ lt s t"
    end.

End RPO_Model.

Module Status (PT : VPrecedenceType).

  Module Export P := VPrecedence PT.

  Import MultisetListOrder.
  Module Export LMO := MultisetListOrder Term_dec.

  Import ListLex.
  Module Export LO := LexOrder Term.

  Section Decidability.

    Variable R : relation Term.A.
    Variables ts ss : terms.

    Lemma lex_status_dec :
      (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) ->
      {lex R ts ss} + {~lex R ts ss}.

    Proof.
      intros. apply lex_dec.
      intros. destruct (term_eq_dec a b); intuition.
      hyp.
    Defined.

    Lemma mul_status_dec :
      (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) ->
      {mult (transp R) ts ss} + {~mult (transp R) ts ss}.

    Proof.
      intros.
      assert (eq_comp : Proper (eq ==> eq ==> impl) (transp R)).
      intros a b ab c d cd. subst. fo.
      destruct (@mOrd_dec_aux
        (transp R) eq_comp (list2multiset ss) (list2multiset ts)).
      assert (R_transp_dec : forall t s, In t ts -> In s ss ->
        {(transp R) s t} + {~(transp R) s t}).
      intros. destruct (X t s); intuition.
      intros. apply R_transp_dec.
      destruct (member_multiset_list ts H0). compute in H2. rewrite H2. hyp.
      destruct (member_multiset_list ss H). compute in H2. rewrite H2. hyp.
      intuition. intuition.
    Defined.

  End Decidability.

(*FIXME: unfinished proof

  Section Homomorphism.

    Variable R : relation Term.A.
    Variable F : Term.A -> Term.A.
    Variables ts ss : terms.

    Lemma mul_status_homomorphic :
      (forall s t, In s ss -> In t ts -> R s t -> R (F s) (F t)) ->
      mult (transp R) ss ts -> mult (transp R) (map F ss) (map F ts).

    Proof.
      intros. unfold mult, MultisetLT, transp.
      apply mord_list_sim with R ts ss; unfold eqA, Term.eqA; trivial.
      congruence.
      unfold order_compatible. intros. split.
      destruct (proj1 (in_map_iff F ts x') H2) as [x'' [x''x' x''ts]].
      destruct (proj1 (in_map_iff F ss y') H5) as [y'' [y''y' y''ss]].
      subst x'. subst y'. intro. apply H; try hyp.
    Abort.

  End Homomorphism.*)

End Status.

author: fblanqui

repo: color

save_path: github-repos/coq/fblanqui-color


Require Import compcert.lib.Coqlib.
Require Import compcert.common.AST.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.
Require Import compcert.common.Memory.
Require Export compcert.lib.Maps.
Require Import compcert.common.Events.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Smallstep.
Require Import ccc26x86.Locations.
Require Import ccc26x86.Stacklayout.
Require Import ccc26x86.Conventions.

(*LENB: again, in Compcomp we imported the modified Asm_comp*)
Require Import ccc26x86.Asm.
Require Import ccc26x86.Asm_coop.

Require Import sepcomp.mem_lemmas. (*for mem_forward*)
Require Import sepcomp.semantics.
Require Import sepcomp.effect_semantics.
Require Import ccc26x86.BuiltinEffects.
Require Import ccc26x86.load_frame.

Require Import msl.Extensionality.

Notation SP := ESP (only parsing).

Notation "a # b" := (a b) (at level 1, only parsing).
Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).

Section ASM_EFF.
(*Variable hf : I64Helpers.helper_functions.*)

(*A computational variant of eval_builtin_arg*)
Section CEVAL_BUILTIN_ARG_COMPUTE.

Variable A: Type.
Variable ge: Senv.t.
Variable e: A -> val.
Variable sp: val.
Variable m: mem.

Fixpoint ceval_builtin_arg (a:builtin_arg A): option val :=
  match a with
    BA x => Some (e x)
  | BA_int n => Some (Vint n)
  | BA_long n => Some (Vlong n)
  | BA_float n => Some (Vfloat n)
  | BA_single n => Some (Vsingle n)
  | BA_loadstack chunk ofs =>
      Mem.loadv chunk m (Val.add sp (Vint ofs))
  | BA_addrstack ofs => Some (Val.add sp (Vint ofs))
  | BA_loadglobal chunk id ofs =>
      Mem.loadv chunk m (Senv.symbol_address ge id ofs)
  | BA_addrglobal id ofs => Some (Senv.symbol_address ge id ofs)
  | BA_splitlong hi lo =>
     match ceval_builtin_arg hi, ceval_builtin_arg lo
     with Some vhi, Some vlo => Some (Val.longofwords vhi vlo)
          | _, _ => None
     end
  end.

Lemma ceval_builtin_arg_char1: forall a v,
  ceval_builtin_arg a = Some v -> eval_builtin_arg ge e sp m a v.
Proof.
  induction a; simpl; intros; inv H; try constructor; trivial.
  destruct (ceval_builtin_arg a1); inv H1.
  destruct (ceval_builtin_arg a2); inv H0.
  econstructor; eauto.
Qed.

Lemma ceval_builtin_arg_char2: forall a v,
  eval_builtin_arg ge e sp m a v -> ceval_builtin_arg a = Some v.
Proof.
  induction a; simpl; intros; inv H; trivial.
  rewrite (IHa1 _ H2). rewrite (IHa2 _ H4); trivial.
Qed.

Definition ceval_builtin_args (args:list (builtin_arg A)): option (list val) :=
fold_right (fun a vals => match ceval_builtin_arg a, vals with
                 Some v, Some vs => Some (v::vs)
               | _, _ => None end)
          (Some nil) args.

Lemma ceval_builtin_args_char: forall args vals,
  ceval_builtin_args args = Some vals <-> eval_builtin_args ge e sp m args vals.
Proof.
induction args; simpl; intros.
  split; intros; inv H. constructor. trivial.
split; intros.
+ remember (ceval_builtin_arg a) as p; symmetry in Heqp.
  destruct p; inv H.
  remember (ceval_builtin_args args) as q; symmetry in Heqq.
  destruct q; inv H1. constructor.
  eapply ceval_builtin_arg_char1. eassumption.
  apply IHargs. trivial.
+ inv H; simpl in *. apply ceval_builtin_arg_char2 in H2.
  apply IHargs in H4. rewrite H2, H4. trivial.
Qed.
End CEVAL_BUILTIN_ARG_COMPUTE.

Section EFFSEM.

Definition effect_instr (ge:genv) (c: code) (i: instruction) (rs: regset) (m: mem)
           : (block -> Z -> bool)  :=
  match i with
  | Pfstps_m a => (StoreEffect (eval_addrmode ge a rs) (encode_val Mfloat32 (rs ST0)))
  | Pfstpl_m a => (StoreEffect (eval_addrmode ge a rs) (encode_val Mfloat64 (rs ST0)))
  | Pmovss_mf a r1 => (StoreEffect (eval_addrmode ge a rs) (encode_val Mfloat32 (rs r1)))
  | Pmov_mr a r1 => (StoreEffect (eval_addrmode ge a rs) (encode_val Mint32 (rs r1)))
  | Pmov_mr_a a r1 => (StoreEffect (eval_addrmode ge a rs) (encode_val Many32 (rs r1)))
  | Pmovsd_mf a r1 => (StoreEffect (eval_addrmode ge a rs) (encode_val Mfloat64 (rs r1)))
  | Pmovsd_mf_a a r1 => (StoreEffect (eval_addrmode ge a rs) (encode_val Many64 (rs r1)))
  | Pmovb_mr a r1 => StoreEffect (eval_addrmode ge a rs) (encode_val Mint8unsigned (rs r1))
  | Pmovw_mr a r1 => StoreEffect (eval_addrmode ge a rs) (encode_val Mint16unsigned (rs r1))
  | Pfreeframe sz ofs_ra ofs_link =>
      match Mem.loadv Mint32 m (Val.add rs#ESP (Vint ofs_ra)) with
      | None => EmptyEffect
      | Some ra =>
          match Mem.loadv Mint32 m (Val.add rs#ESP (Vint ofs_link)) with
          | None => EmptyEffect
          | Some sp =>
              match rs#ESP with
              | Vptr stk ofs =>
                  match Mem.free m stk 0 sz with
                  | None => EmptyEffect
                  | Some m' => (FreeEffect m 0 sz stk)
                  end
              | _ => EmptyEffect
              end
          end
      end
  | Pbuiltin ef args res => EmptyEffect
(*     (BuiltinEffect ge ef (decode_longs (sig_args (ef_sig ef)) (map rs args)) m)*)
(*  | Pannot ef args =>
      EmptyEffect *)
  | _ => EmptyEffect
  end.
Variable ge: genv.

Inductive asm_effstep: (block -> Z -> bool) ->
                       state -> mem -> state -> mem -> Prop :=
  | asm_effexec_step_internal:
      forall b ofs f i rs m rs' m' lf,
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_instr (Int.unsigned ofs) (fn_code f) = Some i ->
      exec_instr ge f i rs m = Next rs' m' ->
      asm_effstep (effect_instr ge (fn_code f) i rs m) (State rs lf) m (State rs' lf) m'
  | asm_effexec_step_builtin:
      False -> (*We don't support builtins/helpers/vload/vstore etc yet*)
      forall b ofs f ef args res rs m vargs t E vres rs' m' lf
         (NASS: ~ isInlinedAssembly ef)  (*NEW; we don't support inlined assembly yet*),
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_instr (Int.unsigned ofs) (fn_code f) = Some (Pbuiltin ef args res) ->
      eval_builtin_args ge rs (rs ESP) m args vargs ->
      external_call ef ge vargs m t vres m' ->
      ~ observableEF (*hf*) ef ->
      rs' = nextinstr_nf
             (set_res res vres
               (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(*in compcomp:      E = BuiltinEffect ge ef (decode_longs (sig_args (ef_sig ef)) vargs) m ->*)
      E = BuiltinEffect ge ef vargs m ->
      asm_effstep E (State rs lf) m (State rs' lf) m'

  | asm_effexec_step_to_external:
      forall b ef args rs m lf,
      rs PC = Vptr b Int.zero ->
      Genv.find_funct_ptr ge b = Some (External ef) ->
      extcall_arguments rs m (ef_sig ef) args ->
      asm_effstep EmptyEffect (State rs lf) m (Asm_CallstateOut ef args rs lf) m
  | asm_effexec_step_external:
      False -> (*We don't support builtins/helpers/vload/vstore etc yet*)
      forall b callee args res rs m t rs' m' lf
      (OBS: EFisHelper (*hf*) callee),
      rs PC = Vptr b Int.zero ->
      Genv.find_funct_ptr ge b = Some (External callee) ->
      extcall_arguments rs m (ef_sig callee) args ->
      external_call callee ge args m t res m' ->
      rs' = (set_pair (loc_external_result (ef_sig callee)) res rs) #PC <- (rs RA) ->
      asm_effstep  (BuiltinEffect ge callee args m)
         (Asm_CallstateOut callee args rs lf) m (State rs' lf) m'
  (*NOTE [loader]*)
  | asm_exec_initialize_call:
      forall m args tys retty m1 stk m2 fb z,
      args_len_rec args tys = Some z ->
      Mem.alloc m 0 (4*z) = (m1, stk) ->
      store_args m1 stk args tys = Some m2 ->
      let rs0 := (Pregmap.init Vundef)
                  #PC <- (Vptr fb Int.zero)
                  #RA <- Vzero
                  # ESP <- (Vptr stk Int.zero) in
      asm_effstep EmptyEffect
               (Asm_CallstateIn fb args tys retty) m
               (State rs0 (mk_load_frame stk retty)) m2.

End EFFSEM.

Section ASM_EFFSEM.

Lemma exec_load_unchanged_on: forall g chunk m a rs rd rs' m' P,
   exec_load g chunk m a rs rd = Next rs' m' ->
   Mem.unchanged_on P m m'.
Proof. intros.
  unfold exec_load in H.
  remember (Mem.loadv chunk m (eval_addrmode g a rs)) as d.
  destruct d; inv H. apply Mem.unchanged_on_refl.
Qed.

Lemma exec_store_unchanged_on: forall g chunk m a rs rs1 pregs rs' m',
  exec_store g chunk m a rs rs1 pregs = Next rs' m' ->
  Mem.unchanged_on (fun b z => StoreEffect (eval_addrmode g a rs)
                     (encode_val chunk (rs rs1)) b z = false)
                   m m'.
Proof. intros. unfold exec_store in H.
  remember (Mem.storev chunk m (eval_addrmode g a rs) (rs rs1)) as d.
  destruct d; inv H. apply eq_sym in Heqd.
  eapply StoreEffect_Storev; eassumption.
Qed.

Lemma goto_label_unchanged_on: forall c0 l rs m rs' m' P,
      goto_label c0 l rs m = Next rs' m' ->
   Mem.unchanged_on P m m'.
Proof. intros.
  unfold goto_label in H.
   destruct (label_pos l 0 (fn_code c0)); inv H.
   destruct (rs PC); inv H1.
   apply Mem.unchanged_on_refl.
Qed.

Lemma exec_instr_unchanged_on g f i rs m rs' m': forall
      (EI: exec_instr g f i rs m = Next rs' m'),
     Mem.unchanged_on (fun b ofs => effect_instr g (fn_code f) i rs m b ofs = false) m m'.
Proof. intros.
 destruct i;
    try solve [inv EI;
                try solve [apply Mem.unchanged_on_refl];
                try solve [eapply exec_load_unchanged_on; eauto];
                try solve [eapply exec_store_unchanged_on; eauto];
                try solve [eapply goto_label_unchanged_on; eauto]].
+ (*Pdiv r1*) inv EI.
  destruct (Val.divu (rs EAX) (rs # EDX <- Vundef r1)); inv H0.
  destruct (Val.modu (rs EAX) (rs # EDX <- Vundef r1)); inv H1.
  apply Mem.unchanged_on_refl.
+ (*Pidiv r1*) inv EI.
  destruct (Val.divs (rs EAX) (rs # EDX <- Vundef r1)); inv H0.
  destruct (Val.mods (rs EAX) (rs # EDX <- Vundef r1)); inv H1.
  apply Mem.unchanged_on_refl.
+ (*Pcmov c rd r1*) inv EI.
      destruct (eval_testcond c rs); inv H0.
        destruct b; inv H1; apply Mem.unchanged_on_refl.
      apply Mem.unchanged_on_refl.
+ (*Pjcc c l*) inv EI.
      destruct (eval_testcond c rs); inv H0.
        destruct b; inv H1. eapply goto_label_unchanged_on; eauto.
      apply Mem.unchanged_on_refl.
+ (*Pjcc2 c1 c2 l*) inv EI.
      destruct (eval_testcond c1 rs); inv H0.
        destruct b; inv H1.
          destruct (eval_testcond c2 rs); inv H0.
            destruct b; inv H1. eapply goto_label_unchanged_on; eauto.
            apply Mem.unchanged_on_refl.
          destruct (eval_testcond c2 rs); inv H0.
            apply Mem.unchanged_on_refl.
+  (*Pjmptbl r tbl*) inv EI.
      destruct (rs r); inv H0.
        destruct (list_nth_z tbl (Int.unsigned i)); inv H1.
        eapply goto_label_unchanged_on; eauto.
+ (* Pallocframe sz ofs_ra ofs_link *) inv EI.
      remember (Mem.alloc m 0 sz) as d.
      destruct d; apply eq_sym in Heqd; inv H0.
      remember (Mem.store Mint32 m0 b (Int.unsigned (Int.add Int.zero ofs_link)) (rs ESP)) as q.
      apply eq_sym in Heqq; destruct q; inv H1.
      remember (Mem.store Mint32 m1 b (Int.unsigned (Int.add Int.zero ofs_ra)) (rs RA)) as w.
      destruct w; apply eq_sym in Heqw; inv H0.
      simpl.
      split; intros.
      - rewrite (Mem.nextblock_store _ _ _ _ _ _ Heqw).
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Heqq).
        rewrite (Mem.nextblock_alloc _ _ _ _ _ Heqd). xomega.
      - split; intros.
        * eapply Mem.perm_store_1; try eassumption.
          eapply Mem.perm_store_1; try eassumption.
          eapply Mem.perm_alloc_1; eassumption.
        * apply (Mem.perm_store_2 _ _ _ _ _ _ Heqw) in H1.
          apply (Mem.perm_store_2 _ _ _ _ _ _ Heqq) in H1.
          eapply Mem.perm_alloc_4; try eassumption.
          intros N; subst. apply Mem.fresh_block_alloc in Heqd. contradiction.
      - rewrite (Mem.store_mem_contents _ _ _ _ _ _ Heqw).
        rewrite (Mem.store_mem_contents _ _ _ _ _ _ Heqq).
        assert (BB: b0 <> b). intros N. subst. apply Mem.fresh_block_alloc in Heqd. apply Mem.perm_valid_block in H0. contradiction.
        rewrite PMap.gso; trivial.
        rewrite PMap.gso; trivial.
        eapply EmptyEffect_alloc; eassumption.
+ (* Pfreeframe sz ofs_ra ofs_link *) inv EI.
      remember (Mem.loadv Mint32 m (Val.add (rs ESP) (Vint ofs_ra))) as d.
      destruct d; inv H0.
      remember (Mem.loadv Mint32 m (Val.add (rs ESP) (Vint ofs_link))) as q.
      destruct q; inv H1.
      remember (rs ESP) as w.
      destruct w; inv H0.
      remember (Mem.free m b 0 sz) as t.
      destruct t; inv H1; apply eq_sym in Heqt.
      eapply unchanged_on_validblock.
      Focus 2. eapply FreeEffect_free; eassumption.
      intuition. unfold effect_instr in H0.
        rewrite <- Heqw, <- Heqd, <- Heqq, Heqt in H0. trivial.
Qed.
(*
Lemma decode_longs_nil: forall tys, decode_longs tys nil = nil.
induction tys. trivial.  simpl in *. destruct a; trivial. Qed.

Lemma BuiltinEffect_decode: forall F V (ge: Genv.t F V) ef vargs,
 BuiltinEffect ge ef (decode_longs (sig_args (ef_sig ef)) vargs)=
 BuiltinEffect ge ef vargs.
Proof. intros.
  destruct ef; trivial.
  + unfold free_Effect. simpl.
    destruct vargs; simpl. reflexivity. destruct v; try reflexivity.
   (* destruct vargs. reflexivity.
    extensionality m. Locate decode_longs. simpl.
    destruct (Mem.load Mint32 m b (Int.unsigned i - 4)); try reflexivity.
    destruct v0; try reflexivity.
    extensionality bb. extensionality z.
    destruct (eq_block bb b); simpl; trivial. subst.
    destruct (zlt 0 (Int.unsigned i0)); simpl; trivial.
    destruct (zle (Int.unsigned i - 4) z ); simpl; trivial.
    destruct (zlt z (Int.unsigned i + Int.unsigned i0)); simpl; trivial.*)
  + extensionality m. extensionality bb. extensionality z.
    remember (BuiltinEffect ge (EF_memcpy sz al) vargs m bb z) as r.
    remember (BuiltinEffect ge (EF_memcpy sz al) (decode_longs (sig_args (ef_sig (EF_memcpy sz al))) vargs) m bb z) as l.
    symmetry in Heql; symmetry in Heqr.
    destruct r.
    - specialize (BuiltinEffect_valid_block _ _ _ _ _ _ Heqr); intros.
      destruct Heql;  simpl in *; trivial.
      destruct vargs; simpl in *; try discriminate.
      destruct v; simpl in *; try discriminate.
      destruct vargs; simpl in *; try discriminate.
      destruct v; simpl in *; try discriminate.
      destruct vargs; simpl in *; try discriminate. trivial. trivial.
    - destruct l; trivial. specialize (BuiltinEffect_valid_block _ _ _ _ _ _ Heql); intros.
      simpl in *.
      destruct vargs; simpl in *; try discriminate.
      destruct v; simpl in *; try discriminate.
      destruct vargs; simpl in *; try discriminate.
      destruct v; simpl in *; try discriminate.
      destruct vargs; simpl in *; try discriminate.
      * rewrite Heqr in Heql. discriminate.
      * exfalso. rewrite Heql in Heqr. discriminate.
Qed.
*)
Lemma asmstep_effax1: forall (M : block -> Z -> bool) g c m c' m'
      (*(HF: helper_functions_declared g hf)*),
      asm_effstep g M c m c' m' ->
      (asm_step (*hf*) g c m c' m' /\
       Mem.unchanged_on (fun (b : block) (ofs : Z) => M b ofs = false) m m').
Proof.
intros.
destruct H; try contradiction.
+ split. eapply asm_exec_step_internal; try eassumption.
  (*clear -H2 hf.*) eapply exec_instr_unchanged_on; eassumption.
(*+ rewrite BuiltinEffect_decode in H6.
  split. eapply asm_exec_step_builtin; try eassumption.
  subst E. eapply BuiltinEffect_unchOn; eassumption.*)
+ split. econstructor; eauto.
       apply Mem.unchanged_on_refl.
(*+ split. econstructor; eauto.
  inv H1.
       exploit @BuiltinEffect_unchOn. eassumption.
         eapply EFhelpers; eassumption.
         eapply H3.
       rewrite BuiltinEffect_decode; trivial. *)
+ split. econstructor; eassumption.
  { assert (sp_fresh: ~Mem.valid_block m stk).
    { eapply Mem.fresh_block_alloc; eauto. }
    eapply mem_unchanged_on_sub_strong.
    eapply unchanged_on_trans with (m2 := m1).
    solve[eapply Mem.alloc_unchanged_on; eauto].
    solve[eapply store_args_unch_on; eauto].
    solve[apply alloc_forward in H0; auto].
    simpl. intros b ofs H2 _ H3. subst.
    solve[apply sp_fresh; auto]. }
Qed.

Lemma asmstep_effax2: forall  g c m c' m',
      asm_step (*hf*) g c m c' m' ->
      exists M, asm_effstep g M c m c' m'.
Proof.
intros. (*unfold corestep, Asm_coop_sem in H; simpl in H.*)
  inv H; try contradiction.
+ destruct i;
    try solve [eexists; econstructor; try eassumption].
(*+ eexists. eapply asm_effexec_step_builtin; try eassumption. trivial. reflexivity.*)
+ eexists. econstructor; eassumption.
(*+ eexists. econstructor; eauto.*)
+ eexists. econstructor; eauto.
Qed.

Lemma exec_store_curWR ge ch m1 a rs1 rs rs2 m2 b z l:
   exec_store ge ch m1 a rs1 rs l = Next rs2 m2 ->
    StoreEffect (eval_addrmode ge a rs1)
         (encode_val ch (rs1 rs)) b z = true ->
   Mem.perm m1 b z Cur Writable.
Proof.
intros. apply StoreEffectD in H0. destruct H0 as [i [? [? ?]]].
  unfold exec_store in H. rewrite H0 in *. simpl in H.
  remember (Mem.store ch m1 b (Int.unsigned i) (rs1 rs)) as q.
  destruct q; inv H. symmetry in Heqq.
  eapply (Mem.store_valid_access_3 _ _ _ _ _ _ Heqq).
  rewrite encode_val_length, <- size_chunk_conv in H2. omega.
Qed.

Lemma free_curWR bb lo hi b z: forall m m',
      Mem.free m bb lo hi = Some m' ->
      FreeEffect m lo hi bb b z = true ->
      Mem.perm m b z Cur Writable.
Proof. clear.
  intros.
  apply FreeEffectD in H0. destruct H0 as [? [? ?]]; subst bb.
  eapply Mem.perm_implies.
  eapply Mem.free_range_perm; eassumption. constructor.
Qed.

Lemma exec_instr_curWR ge f i rs1 m1 rs2 m2: forall
      (EI: exec_instr ge f i rs1 m1 = Next rs2 m2) b z
      (EFFI: effect_instr ge (fn_code f) i rs1 m1 b z = true),
      Mem.perm m1 b z Cur Writable.
Proof. intros.
  destruct i; simpl in *; try discriminate.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ eapply exec_store_curWR; eauto.
+ remember (Mem.loadv Mint32 m1 (Val.add (rs1 ESP) (Vint ofs_ra))) as q.
  destruct q; try discriminate.
  remember (Mem.loadv Mint32 m1 (Val.add (rs1 ESP) (Vint ofs_link))) as p.
  destruct p; try discriminate.
  remember (rs1 ESP) as u.
  destruct u; try discriminate.
  remember (Mem.free m1 b0 0 sz) as d.
  destruct d; try discriminate.
  symmetry in Heqd. eapply free_curWR; eassumption.
Qed.

Lemma asm_effstep_curWR: forall (M : block -> Z -> bool) g c m c' m',
      asm_effstep g M c m c' m' ->
      forall b z, M b z = true -> Mem.perm m b z Cur Writable.
Proof.
  intros.
  induction H; try (solve [inv H0]); try contradiction.
+ eapply exec_instr_curWR; eauto.
(*+ rewrite BuiltinEffect_decode in *; subst E.
  eapply nonobs_extcall_curWR; eassumption.*)
(*+ apply EFhelpers in OBS. inv H2.
  eapply nonobs_extcall_curWR. eassumption. eassumption.
  rewrite BuiltinEffect_decode; trivial.*)
Qed.

Lemma exec_store_valid: forall g chunk m a rs rs1 pregs rs' m' b z,
  exec_store g chunk m a rs rs1 pregs = Next rs' m' ->
  StoreEffect (eval_addrmode g a rs) (encode_val chunk (rs rs1)) b z =
              true ->
  Mem.valid_block m b.
Proof. intros. eapply Mem.perm_valid_block. eapply exec_store_curWR; eassumption. Qed.
(*
Lemma exec_instr_valid_block ge fn i rs1 m1 rs2 m2: forall
      (EI: exec_instr ge fn i rs1 m1 = Next rs2 m2) b z
      (EFFI: effect_instr ge fn i rs1 m1 b z = true),
      Mem.valid_block m1 b.
Proof. intros. eapply Mem.perm_valid_block. eapply exec_instr_curWR; eassumption. Qed.
*)
Lemma asm_effstep_valid: forall (M : block -> Z -> bool) g c m c' m',
      asm_effstep g M c m c' m' ->
       forall b z, M b z = true -> Mem.valid_block m b.
Proof. intros. eapply Mem.perm_valid_block. eapply asm_effstep_curWR; eassumption. Qed.

Program Definition Asm_eff_sem :
  @EffectSem genv state.
Proof.
eapply Build_EffectSem with (sem := Asm_mem_sem (*hf*)).
apply asmstep_effax1.
apply asmstep_effax2.
apply asm_effstep_curWR.
Defined.

Lemma Asm_eff_sem_det : semantics_lemmas.corestep_fun Asm_eff_sem.
Proof.
intros m m' m'' ge c c' c'' step1 step2.
simpl in step1, step2.
eapply asm_step_det in step1; eauto.
destruct step1; subst; auto.
Qed.

End ASM_EFFSEM.

End ASM_EFF.


text:
Require Export SystemFR.SatisfiesLemmas.
Require Export SystemFR.ErasedEquivalentIte.
Require Export SystemFR.ErasedEquivalentMatch.

Opaque reducible_values.

Lemma equivalent_split_bool:
  forall ρ Γ1 Γ2 b t t' x l,
    ~(x ∈ fv b) ->
    ~(x ∈ fv t) ->
    ~(x ∈ fv t') ->
    ~(x ∈ fv_context Γ1) ->
    ~(x ∈ fv_context Γ2) ->
    subset (fv b) (support Γ2) ->
    [ support ρ; Γ2 ⊨ b : T_bool ] ->
    valid_interpretation ρ ->
    (forall l,
       satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv b ttrue) :: Γ2) l ->
       [ substitute t l ≡ substitute t' l ]) ->
    (forall l,
       satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv b tfalse) :: Γ2) l ->
       [ substitute t l ≡ substitute t' l ]) ->
    satisfies (reducible_values ρ) (Γ1 ++ Γ2) l ->
    [ substitute t l ≡ substitute t' l ].
Proof.
  unfold open_reducible,reduces_to;
    repeat step || simp_red || satisfies_cut || t_instantiate_sat3 || t_sat_add;
    eauto 2 with b_equiv_subst;
    try solve [ eapply satisfies_insert2; eauto; t_closer ].
Qed.

Lemma equivalent_split_nat:
  forall ρ Γ1 Γ2 n t t' x y l,
    ~(x ∈ fv_context Γ1) ->
    ~(x ∈ fv_context Γ2) ->
    ~(x ∈ fv n) ->
    ~(x ∈ fv t) ->
    ~(x ∈ fv t') ->
    ~(y ∈ fv_context Γ1) ->
    ~(y ∈ fv_context Γ2) ->
    ~(y ∈ fv n) ->
    ~(y ∈ fv t) ->
    ~(y ∈ fv t') ->
    ~(x = y) ->
    subset (fv n) (support Γ2) ->
    [ support ρ; Γ2 ⊨ n : T_nat ] ->
    valid_interpretation ρ ->
    (forall l,
       satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv n zero) :: Γ2) l ->
       [ substitute t l ≡ substitute t' l ]) ->
    (forall l,
       satisfies (reducible_values ρ)
                 (Γ1 ++ (x, T_equiv n (succ (fvar y term_var))) :: (y, T_nat) :: Γ2)
                 l ->
       [ substitute t l ≡ substitute t' l ]) ->
    satisfies (reducible_values ρ) (Γ1 ++ Γ2) l ->
    [ substitute t l ≡ substitute t' l ].
Proof.
  unfold open_reducible,reduces_to;
    repeat step || t_instantiate_sat3 || simp_red || satisfies_cut.

  force_invert is_nat_value; repeat step || t_sat_add;
    eauto 2 with b_equiv_subst;
    try solve [ eapply satisfies_insert2; eauto; t_closer ];
    try solve [ eapply satisfies_insert_nat_succ; eauto; t_closer ].
Qed.

Lemma reducible_equivalent_ite:
  forall ρ Γ t1 t2 t3 t x l,
    ~(x ∈ fv_context Γ) ->
    ~(x ∈ fv t1) ->
    ~(x ∈ fv t2) ->
    ~(x ∈ fv t3) ->
    ~(x ∈ fv t) ->
    is_erased_term t2 ->
    is_erased_term t3 ->
    wf t2 0 ->
    wf t3 0 ->
    subset (fv t2) (support Γ) ->
    subset (fv t3) (support Γ) ->
    valid_interpretation ρ ->
    [ support ρ; Γ ⊨ t1 : T_bool ] ->
    satisfies (reducible_values ρ) Γ l ->
    (forall l,
       satisfies (reducible_values ρ) ((x, T_equiv t1 ttrue) :: Γ) l ->
       [ substitute t2 l ≡ substitute t l ]) ->
    (forall l,
       satisfies (reducible_values ρ) ((x, T_equiv t1 tfalse) :: Γ) l ->
       [ substitute t3 l ≡ substitute t l ]) ->
    [ ite (substitute t1 l) (substitute t2 l) (substitute t3 l) ≡ substitute t l ].
 Proof.
   unfold open_reducible;
     repeat step || apply equivalent_ite || t_instantiate_sat3 || simp_red ||
            t_deterministic_star || unfold reduces_to in * || t_sat_add;
     eauto 2 with b_equiv_subst;
     t_closer;
     try solve [ eapply satisfies_insert3; eauto; t_closer ].
Qed.

Lemma reducible_equivalent_match:
  forall ρ Γ tn t0 ts t n p l,
    ~(p ∈ fv_context Γ) ->
    ~(p ∈ fv tn) ->
    ~(p ∈ fv ts) ->
    ~(p ∈ fv t0) ->
    ~(p ∈ fv t) ->
    ~(n ∈ fv_context Γ) ->
    ~(n ∈ fv ts) ->
    ~(n ∈ fv tn) ->
    ~(n ∈ fv t) ->
    ~(n = p) ->
    [ support ρ; Γ ⊨ tn : T_nat ] ->
    valid_interpretation ρ ->
    is_erased_term t0 ->
    is_erased_term ts ->
    wf t0 0 ->
    wf ts 1 ->
    subset (fv t0) (support Γ) ->
    subset (fv ts) (support Γ) ->
    (forall l,
       satisfies (reducible_values ρ) ((p, T_equiv tn zero) :: Γ) l ->
       [ substitute t0 l ≡ substitute t l ]) ->
    (forall l,
       satisfies (reducible_values ρ)
                 ((p, T_equiv tn (succ (fvar n term_var))) :: (n, T_nat) :: Γ)
                 l ->
       [ substitute (open 0 ts (fvar n term_var)) l ≡ substitute t l ]) ->
    satisfies (reducible_values ρ) Γ l ->
    [ tmatch (substitute tn l) (substitute t0 l) (substitute ts l) ≡ substitute t l ].
Proof.
  unfold open_reducible,reduces_to; repeat step || t_instantiate_sat3 || simp_red.
  eapply equivalent_match; eauto;
    repeat step || t_sat_add || step_inversion is_nat_value;
      eauto 2 with b_equiv_subst;
      t_closer;
      try solve [ eapply satisfies_insert3; eauto; t_closer ];
      try solve [ eapply satisfies_cons_nat_succ; eauto; t_closer ].
Qed.

author: epfl-lara

repo: SystemFR

save_path: github-repos/coq/epfl-lara-SystemFR