text:
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Maps.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.
Require Import compcert.common.Memory.
Require Import compcert.common.Events.
Require Import compcert.common.AST.
Require Import compcert.common.Globalenvs.

Require Import VST.msl.Extensionality.
Require Import VST.sepcomp.mem_lemmas.
Require Import VST.sepcomp.semantics.
Require Import VST.sepcomp.semantics_lemmas.

(** * Effect Semantics *)

(** Effect semantics augment memory semantics with effects, in the form
    of a set of locations [block -> Z -> bool] associated with each internal
    step of the semantics. *)

Record EffectSem {C} :=
  { (** [sem] is a memory semantics. *)
    sem :> @MemSem C

    (** The step relation of the new semantics. *)
  ; effstep: (block -> Z -> bool) -> C -> mem -> C -> mem -> Prop

    (** The next three fields axiomatize [effstep] and its relation to the
        underlying step relation of [sem]. *)
  ; effax1: forall M c m c' m',
       effstep M c m c' m' ->
            corestep sem c m c' m'
         /\ Mem.unchanged_on (fun b ofs => M b ofs = false) m m'
  ; effax2: forall c m c' m',
       corestep sem c m c' m' ->
       exists M, effstep M c m c' m'
  ; effstep_perm: forall M c m c' m',
       effstep M c m c' m' ->
       forall b z, M b z = true -> Mem.perm m b z Cur Writable
  }.
(*
Arguments EffectSem [].
*)
(** * Lemmas and auxiliary definitions *)

Section effsemlemmas.
  Context {C:Type} (Sem: @EffectSem C).

  Lemma effstep_valid: forall M c m c' m',
       effstep Sem 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 effstep_perm; eassumption. Qed.

  Lemma effstep_corestep: forall M c m c' m',
      effstep Sem M c m c' m' -> corestep Sem c m c' m'.
  Proof. intros. apply effax1 in H. apply H. Qed.

  Lemma effstep_unchanged: forall M c m c' m',
        effstep Sem M c m c' m' ->
        Mem.unchanged_on (fun b ofs => M b ofs = false) m m'.
  Proof. intros. apply effax1 in H. apply H. Qed.

  Lemma effstep_mem U c m c' m' (EF: effstep Sem U c m c' m'): mem_step m m'.
  Proof. intros. apply effax1 in EF. destruct EF as [EF _].
         eapply corestep_mem. apply EF.
  Qed.

  Lemma effstep_fwd U c m c' m' (EF: effstep Sem U c m c' m'): mem_forward m m'.
  Proof. apply preserve_mem. apply mem_forward_preserve.
         eapply effstep_mem. apply EF.
  Qed.

  Fixpoint effstepN (n:nat) : (block -> Z -> bool) -> C -> mem -> C -> mem -> Prop :=
    match n with
      | O => fun U c m c' m' => (c,m) = (c',m') /\ U = (fun b z => false)
      | S k => fun U c1 m1 c3 m3 => exists c2, exists m2, exists U1, exists U2,
        effstep Sem U1 c1 m1 c2 m2 /\
        effstepN k U2 c2 m2 c3 m3 /\
        U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b))
    end.

  Lemma effstepN_perm: forall n U c1 m1 c2 m2, effstepN n U c1 m1 c2 m2 ->
       forall b z, U b z = true -> Mem.perm m1 b z Cur Writable.
  Proof. intros n.
    induction n; simpl; intros. destruct H; subst. discriminate.
    destruct H as [c [m [U1 [U2 [Step [StepN UU]]]]]]; subst; simpl.
    specialize (IHn _ _ _ _ _ StepN).
    specialize (effstep_perm _ _ _ _ _ _ Step b z). intros.
    remember (U1 b z) as d.
    destruct d; simpl in *.
    + apply H; trivial.
    + (* destruct (Mem.perm_dec m1 b z Cur Writable). trivial. simpl in *.*)
      clear H Heqd StepN.
      rewrite andb_true_iff in H0. destruct H0.
      specialize (IHn _ _ H). destruct (valid_block_dec m1 b); inv H0.
      apply effstep_corestep in Step. apply corestep_mem in Step.
      apply perm_preserve in Step. apply Step; trivial.
      eapply Mem.perm_implies. eapply Mem.perm_max. eassumption. constructor.
  Qed.
  Lemma effstepN_valid n U c1 m1 c2 m2  (Step:effstepN n U c1 m1 c2 m2)
        b z (EFF:U b z = true): Mem.valid_block m1 b.
  Proof. eapply Mem.perm_valid_block. eapply effstepN_perm; eassumption. Qed.

  Lemma effstepN_mem: forall n U c m c' m' (EF: effstepN n U c m c' m'), mem_step m m'.
  Proof.
    induction n; simpl; intros.
    + destruct EF as [EF _]; inv EF. apply mem_step_refl.
    + destruct EF as [c1 [m2 [U1 [U2 [EF1 [EF2 _]]]]]].
      apply IHn in EF2. clear IHn.
      apply effstep_mem in EF1.
      eapply mem_step_trans; eassumption.
  Qed.

  Lemma effstepN_fwd n U c m c' m' (EF:effstepN n U c m c' m'): mem_forward m m'.
  Proof. apply preserve_mem. apply mem_forward_preserve.
         eapply effstepN_mem. apply EF.
  Qed.

  Lemma effstepN_corestepN: forall n E c m c' m',
      effstepN n E c m c' m' -> corestepN Sem n c m c' m'.
  Proof. intros n.
    induction n; intros; simpl in *.
        apply H.
      destruct H as [c1 [m1 [U1 [U2 [Estep [EN HE]]]]]].
        apply effstep_corestep in Estep.
        apply IHn in EN. exists c1, m1.
        split; eassumption.
  Qed.

  Lemma effstepN_unchanged: forall n U c1 m1 c2 m2,
        effstepN n U c1 m1 c2 m2 ->
        Mem.unchanged_on (fun b z => U b z = false) m1 m2.
  Proof. intros n.
    induction n; simpl; intros.
      destruct H. inv H. apply Mem.unchanged_on_refl.
    rename c2 into c3. rename m2 into m3.
    destruct H as [c2 [m2 [E1 [E2 [Step1 [Step2 HE]]]]]].
    apply IHn in Step2; clear IHn. subst.
    assert (FWD:= effstep_fwd _ _ _ _ _ Step1).
    apply effstep_unchanged in Step1.
    split; intros.
     eapply Ple_trans; [apply Step1 | apply Step2].
     apply orb_false_iff in H. destruct H.
     remember (valid_block_dec m1 b) as v.
     destruct v; simpl in *; try contradiction.
     clear H0 Heqv.
     rewrite andb_true_r in H1.
     split; intros. apply Step2; trivial.
        apply (FWD _ v).
     apply Step1; try assumption.

     apply Step1; try assumption.
       apply Step2; try assumption.
        apply (FWD _ v).

   apply orb_false_iff in H. destruct H.
     remember (valid_block_dec m1 b) as v.
     destruct v; simpl in *; try contradiction.
     clear Heqv.
     rewrite andb_true_r in H1.
     destruct Step2. rewrite unchanged_on_contents; trivial.
       eapply Step1; try eassumption.
       eapply Step1; try eassumption.
     elim n0. eapply Mem.perm_valid_block; eassumption.
  Qed.

Lemma effstepN_trans: forall n1 n2 U1 st1 m1 st2 m2 U2 st3 m3,
      effstepN n1 U1 st1 m1 st2 m2 ->
      effstepN n2 U2 st2 m2 st3 m3 ->
   effstepN (n1+n2)
        (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) st1 m1 st3 m3.
Proof. intros n1.
induction n1; simpl.
  intros. destruct H; subst. inv H. simpl.
  assert (U2 = (fun b z => U2 b z && valid_block_dec m2 b)).
    extensionality b; extensionality z.
    remember (U2 b z) as d. destruct d; trivial.
    apply eq_sym in Heqd.
    apply (effstepN_valid _ _ _ _ _ _ H0) in Heqd.
    remember (valid_block_dec m2 b) as q.
    destruct q; trivial. contradiction.
  rewrite H in H0. apply H0.
intros. rename st3 into st4. rename m3 into m4.
   rename st2 into st3. rename m2 into m3.
   rename U1 into U. rename U2 into U3.
   destruct H as [st2 [m2 [U1 [U2 [Step1 [Step2 HU]]]]]].
   subst; simpl in *.
   exists st2, m2, U1; simpl.
   specialize (IHn1 _ _ _ _ _ _ _ _ _ Step2 H0).
   clear Step2 H0.
   eexists; split. assumption.
   split. eassumption.
   extensionality b; extensionality z; simpl.
   remember (U1 b z) as d. destruct d; simpl; trivial; apply eq_sym in Heqd.
   remember (U2 b z) as q. destruct q; simpl; trivial; apply eq_sym in Heqq.
     remember (valid_block_dec m1 b) as u.
     destruct u; trivial; simpl. apply andb_false_r.
   remember (U3 b z) as p. destruct p; simpl; trivial; apply eq_sym in Heqp.
     remember (valid_block_dec m1 b) as u.
     destruct u; trivial; simpl. clear Hequ. rewrite andb_true_r.
       apply effstep_fwd in Step1. apply Step1 in v.
       destruct (valid_block_dec m2 b); trivial. destruct v; contradiction.
     rewrite andb_false_r. trivial.
Qed.

Lemma effstepN_trans': forall n1 n2 U U1 st1 m1 st2 m2 U2 st3 m3,
      effstepN n1 U1 st1 m1 st2 m2 ->
      effstepN n2 U2 st2 m2 st3 m3 ->
      U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) ->
   effstepN (n1+n2) U st1 m1 st3 m3.
Proof. intros; subst. eapply effstepN_trans; eassumption. Qed.

  Definition effstep_plus U c m c' m' :=
    exists n, effstepN (S n) U c m c' m'.

  Definition effstep_star U c m c' m' :=
    exists n, effstepN n U c m c' m'.

  Lemma effstep_plus_corestep_plus U c m c' m' (EFF: effstep_plus U c m c' m'):
        corestep_plus Sem c m c' m'.
  Proof. destruct EFF. apply effstepN_corestepN in H. exists x; trivial. Qed.

  Lemma effstep_star_corestep_star U c m c' m' (EFF: effstep_star U c m c' m'):
        corestep_star Sem c m c' m'.
  Proof. destruct EFF. apply effstepN_corestepN in H. exists x; trivial. Qed.

  Lemma effstep_plus_star : forall U c1 c2 m1 m2,
    effstep_plus U c1 m1 c2 m2 -> effstep_star U c1 m1 c2 m2.
  Proof. intros. destruct H as [n1 H1]. eexists. apply H1. Qed.

  Lemma effstep_plus_trans : forall U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_plus U1 c1 m1 c2 m2 -> effstep_plus U2 c2 m2 c3 m3 ->
    effstep_plus (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) c1 m1 c3 m3.
  Proof. intros. destruct H as [n1 H1]. destruct H0 as [n2 H2].
    exists ((n1 + (S n2))%nat). simpl.
    apply (effstepN_trans (S n1) (S n2) U1 c1 m1 c2 m2 U2 c3 m3 H1 H2).
  Qed.
  Lemma effstep_plus_trans' : forall U U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_plus U1 c1 m1 c2 m2 -> effstep_plus U2 c2 m2 c3 m3 ->
    U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) ->
    effstep_plus U c1 m1 c3 m3.
  Proof. intros; subst. eapply effstep_plus_trans; eassumption. Qed.

  Lemma effstep_star_plus_trans : forall U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_star U1 c1 m1 c2 m2 -> effstep_plus U2 c2 m2 c3 m3 ->
    effstep_plus (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) c1 m1 c3 m3.
  Proof. intros. destruct H as [n1 H1]. destruct H0 as [n2 H2].
    exists ((n1 + n2)%nat).
    specialize (effstepN_trans n1 (S n2) U1 c1 m1 c2 m2 U2 c3 m3 H1 H2); intros H.
    rewrite <- plus_n_Sm in H. assumption.
  Qed.
  Lemma effstep_star_plus_trans' : forall U U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_star U1 c1 m1 c2 m2 -> effstep_plus U2 c2 m2 c3 m3 ->
    U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) ->
    effstep_plus U c1 m1 c3 m3.
  Proof. intros; subst. eapply effstep_star_plus_trans; eassumption. Qed.

  Lemma effstep_plus_star_trans: forall U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_plus U1 c1 m1 c2 m2 -> effstep_star U2 c2 m2 c3 m3 ->
    effstep_plus (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) c1 m1 c3 m3.
  Proof. intros. destruct H as [n1 H1]. destruct H0 as [n2 H2].
    exists ((n1 + n2)%nat).
    apply (effstepN_trans _ _  U1 c1 m1 c2 m2 U2 c3 m3 H1 H2).
  Qed.
  Lemma effstep_plus_star_trans': forall U U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_plus U1 c1 m1 c2 m2 -> effstep_star U2 c2 m2 c3 m3 ->
    U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) ->
    effstep_plus U c1 m1 c3 m3.
  Proof. intros; subst. eapply effstep_plus_star_trans; eassumption. Qed.

  Lemma effstep_star_trans: forall U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_star U1 c1 m1 c2 m2 -> effstep_star U2 c2 m2 c3 m3 ->
    effstep_star (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) c1 m1 c3 m3.
  Proof. intros. destruct H as [n1 H1]. destruct H0 as [n2 H2].
    eexists.
    eapply (effstepN_trans _ _ U1 c1 m1 c2 m2 U2 c3 m3 H1 H2).
  Qed.
  Lemma effstep_star_trans': forall U U1 c1 c2 c3 U2 m1 m2 m3,
    effstep_star U1 c1 m1 c2 m2 -> effstep_star U2 c2 m2 c3 m3 ->
    U = (fun b z => U1 b z || (U2 b z && valid_block_dec m1 b)) ->
    effstep_star U c1 m1 c3 m3.
  Proof. intros; subst. eapply effstep_star_trans; eassumption. Qed.

  Lemma effstep_plus_one: forall U c m c' m',
    effstep Sem U c m c' m' -> effstep_plus U c m c' m'.
  Proof. intros. exists O. simpl. exists c', m', U, (fun b z =>false).
    intuition.
    extensionality b; extensionality z; simpl.
    rewrite orb_false_r. trivial.
  Qed.

  Lemma effstep_plus_two: forall U1 c m c' m' U2 c'' m'',
    effstep  Sem U1 c m c' m' -> effstep Sem U2 c' m' c'' m'' ->
    effstep_plus (fun b z => U1 b z || (U2 b z && valid_block_dec m b)) c m c'' m''.
  Proof. intros.
    exists (S O). exists c', m', U1, U2. split; trivial.
    split; trivial. simpl.
    exists c'', m'', U2, (fun b z =>false).
    intuition.
    extensionality b; extensionality z; simpl.
    rewrite orb_false_r. trivial.
  Qed.

  Lemma effstep_star_zero: forall c m, effstep_star (fun b z =>false) c m c m.
  Proof. intros. exists O. simpl. split; reflexivity. Qed.

  Lemma effstep_star_one: forall U c m c' m',
    effstep  Sem U c m c' m' -> effstep_star U c m c' m'.
  Proof. intros.
    exists (S O). exists c', m', U, (fun b z =>false).
    simpl; split; trivial. split. split; reflexivity.
    extensionality b; extensionality z; simpl.
    rewrite orb_false_r. trivial.
  Qed.

  Lemma effstep_plus_split: forall U c m c' m',
    effstep_plus U c m c' m' ->
    exists c'', exists m'', exists U1, exists U2,
      effstep Sem U1 c m c'' m'' /\
      effstep_star U2 c'' m'' c' m' /\
      U = (fun b z => U1 b z || (U2 b z && valid_block_dec m b)).
  Proof. intros.
    destruct H as [n [c2 [m2 [U1 [U2 [Hstep [Hstar HU]]]]]]].
    exists c2, m2, U1, U2. split. assumption. split; try assumption.
    exists n. assumption.
  Qed.

  Lemma effstep_plus_perm U c1 m1 c2 m2 (Step: effstep_plus U c1 m1 c2 m2):
       forall b z, U b z = true -> Mem.perm m1 b z Cur Writable.
  Proof. destruct Step. eapply effstepN_perm; eassumption. Qed.

  Lemma effstep_star_perm U c1 m1 c2 m2 (Step: effstep_star U c1 m1 c2 m2):
       forall b z, U b z = true -> Mem.perm m1 b z Cur Writable.
  Proof. destruct Step. eapply effstepN_perm; eassumption. Qed.

  Lemma effstep_plus_valid U c1 m1 c2 m2 (Step: effstep_plus U c1 m1 c2 m2):
       forall b z, U b z = true -> Mem.valid_block m1 b.
  Proof. destruct Step. eapply effstepN_valid; eassumption. Qed.

  Lemma effstep_star_valid U c1 m1 c2 m2 (Step: effstep_star U c1 m1 c2 m2):
       forall b z, U b z = true -> Mem.valid_block m1 b.
  Proof. destruct Step. eapply effstepN_valid; eassumption. Qed.

  Lemma effstep_star_mem U c m c' m' (EF: effstep_star U c m c' m'): mem_step m m'.
  Proof. destruct EF as [n H].
      eapply effstepN_mem; eassumption.
  Qed.

  Lemma effstep_plus_mem U c m c' m' (EF: effstep_plus U c m c' m'): mem_step m m'.
  Proof. destruct EF as [n H].
      eapply effstepN_mem; eassumption.
  Qed.

  Lemma effstep_plus_fwd U c m c' m' (EF: effstep_plus U c m c' m'): mem_forward m m'.
  Proof. apply preserve_mem. apply mem_forward_preserve.
         eapply effstep_plus_mem. apply EF.
  Qed.
  Lemma effstep_star_fwd U c m c' m' (EF: effstep_star U c m c' m'): mem_forward m m'.
  Proof. apply preserve_mem. apply mem_forward_preserve.
         eapply effstep_star_mem. apply EF.
  Qed.

End effsemlemmas.

Definition EmptyEffect: Values.block -> Z -> bool := fun b z => false.

Lemma EmptyEffect_alloc: forall m lo hi m' b (ALLOC: Mem.alloc m lo hi = (m', b)),
      Mem.unchanged_on (fun b ofs => EmptyEffect b ofs = false) m m'.
Proof. intros.
       eapply Mem.alloc_unchanged_on; eassumption.
Qed.

Definition FreeEffect m lo hi (sp b:Values.block) (ofs:Z): bool :=
   if valid_block_dec m b
   then eq_block b sp && zle lo ofs && zlt ofs hi
   else false.

Lemma FreeEffectD: forall m lo hi sp b z
   (FREE:FreeEffect m lo hi sp b z = true),
   b = sp /\ Mem.valid_block m b /\ lo <= z /\ z < hi.
Proof. intros.
  unfold FreeEffect in FREE.
  destruct (valid_block_dec m b); simpl in *; try discriminate.
  destruct (eq_block b sp); subst; simpl in *; try discriminate.
  destruct (zle lo z); simpl in *; try discriminate.
  destruct (zlt z hi); simpl in *; try discriminate.
  auto.
Qed.

Lemma FreeEffect_free: forall m sp lo hi m'
             (FREE: Mem.free m sp lo hi = Some m'),
     Mem.unchanged_on  (fun b ofs => FreeEffect m lo hi sp b ofs = false) m m'.
Proof. intros.
       eapply Mem.free_unchanged_on; try eassumption.
               intros. unfold FreeEffect; simpl. intros N.
               destruct (valid_block_dec m sp).
               apply andb_false_iff in N. destruct H.
               destruct (eq_block sp sp); simpl in *.
                 destruct N. destruct (zle lo i). inv H1. lia.
               destruct (zlt i hi). inv H1. lia.
               apply n; trivial.
               apply Mem.free_range_perm in FREE.
                 apply n; clear n.
                 eapply Mem.perm_valid_block.
                 eapply (FREE lo). lia.
Qed.

Definition FreelistEffect
  m (L: list (Values.block * Z * Z)) (b:Values.block) (ofs:Z): bool :=
  List.fold_right (fun X E b z => match X with (bb,lo,hi) =>
                                   E b z || FreeEffect m lo hi bb b z
                                 end)
                  EmptyEffect L b ofs.

Lemma FreelistEffect_Dfalse: forall m bb lo hi L b ofs
      (F:FreelistEffect m ((bb, lo, hi) :: L) b ofs = false),
      FreelistEffect m L b ofs = false /\
      FreeEffect m lo hi bb b ofs = false.
Proof. intros.
  unfold FreelistEffect in F. simpl in F.
  apply orb_false_iff in F. apply F.
Qed.

Lemma FreelistEffect_Dtrue: forall m bb lo hi L b ofs
      (F:FreelistEffect m ((bb, lo, hi) :: L) b ofs = true),
      FreelistEffect m L b ofs = true \/
      FreeEffect m lo hi bb b ofs = true.
Proof. intros.
  unfold FreelistEffect in F. simpl in F.
  apply orb_true_iff in F. apply F.
Qed.

Lemma FreelistEffect_same: forall m bb lo hi mm L
          (F:Mem.free m bb lo hi = Some mm)
          b (VB: Mem.valid_block mm b) ofs,
      FreelistEffect mm L b ofs = false <-> FreelistEffect m L b ofs = false.
Proof. intros  m bb lo hi mm L.
  induction L; simpl; intros. intuition.
  intuition.
    apply orb_false_iff in H0. destruct H0.
    specialize (H _ VB ofs).
    apply H in H0. rewrite H0. simpl. clear H H0.
    unfold FreeEffect in *; simpl in *.
    apply Mem.nextblock_free in F.
    destruct (valid_block_dec m b).
      destruct (valid_block_dec mm b); trivial.
      red in v. rewrite <- F in v. elim n. apply v.
    trivial.
  apply orb_false_iff in H0. destruct H0.
    specialize (H _ VB ofs).
    apply H in H0. rewrite H0. simpl. clear H H0.
    unfold FreeEffect in *; simpl in *.
    apply Mem.nextblock_free in F.
    destruct (valid_block_dec mm b).
      destruct (valid_block_dec m b); trivial.
      red in v. rewrite F in v. elim n. apply v.
    trivial.
Qed.

Lemma FreelistEffect_freelist: forall L m m' (FL: Mem.free_list m L = Some m'),
      Mem.unchanged_on (fun b ofs => FreelistEffect m L b ofs = false) m m'.
Proof. intros L.
  induction L; simpl; intros.
    inv FL. apply Mem.unchanged_on_refl.
  destruct a as [[bb lo] hi].
    remember (Mem.free m bb lo hi) as d.
    destruct d; try inv FL. apply eq_sym in Heqd.
    specialize (IHL _ _ H0).
    assert (FF:= FreeEffect_free _ _ _ _ _ Heqd).
    eapply (unchanged_on_trans _ m0 _).
      eapply mem_unchanged_on_sub; try eassumption.
        intuition. apply orb_false_iff in H. apply H.
      clear FF.
      specialize (unchanged_on_validblock_invariant m0 m'
           (fun (b : block) (ofs : Z) => FreelistEffect m0 L b ofs = false)
           (fun (b : block) (ofs : Z) => FreelistEffect m L b ofs = false)).
      intros. apply H in IHL. clear H.
        eapply mem_unchanged_on_sub; try eassumption.
        intuition. apply orb_false_iff in H. apply H.
      clear IHL H. intros.
       eapply FreelistEffect_same; eassumption.
   eapply free_forward; eassumption.
Qed.

Lemma FreeEffect_validblock: forall m lo hi sp b ofs
        (EFF: FreeEffect m lo hi sp b ofs = true),
      Mem.valid_block m b.
Proof. intros.
  unfold FreeEffect in EFF.
  destruct (valid_block_dec m b); trivial; inv EFF.
Qed.

Lemma FreelistEffect_validblock: forall l m b ofs
        (EFF: FreelistEffect m l b ofs = true),
      Mem.valid_block m b.
Proof. intros l.
  induction l; unfold FreelistEffect; simpl; intros.
     unfold EmptyEffect in EFF. inv EFF.
  destruct a as [[bb lo] hi].
  apply orb_true_iff in EFF.
  destruct EFF.
  apply IHl in H. assumption.
  eapply FreeEffect_validblock; eassumption.
Qed.

Definition StoreEffect (tv:val)(vl : list memval) (b:Values.block) (z:Z):bool :=
  match tv with Vptr bb ofs => eq_block bb b &&
             zle (Ptrofs.unsigned ofs) z && zlt z (Ptrofs.unsigned ofs + Z.of_nat (length vl))
         | _ => false
  end.

Lemma StoreEffect_Storev: forall m chunk tv tv' m'
         (STORE : Mem.storev chunk m tv tv' = Some m'),
      Mem.unchanged_on
        (fun b ofs => StoreEffect tv (encode_val chunk tv') b ofs = false)
        m m'.
Proof. intros.
  destruct tv; inv STORE.
  unfold StoreEffect.
  split; intros.
      rewrite (Mem.nextblock_store _ _ _ _ _ _ H0); apply Pos.le_refl.
      split; intros. eapply Mem.perm_store_1; eassumption.
      eapply Mem.perm_store_2; eassumption.
  rewrite (Mem.store_mem_contents _ _ _ _ _ _ H0). clear H0.
  destruct (eq_block b b0); subst; simpl in *.
    rewrite PMap.gss. apply andb_false_iff in H.
    apply Mem.setN_outside.
    destruct H. destruct (zle (Ptrofs.unsigned i) ofs ); simpl in *. inv H.
                left. lia.
    right. remember (Z.of_nat (length (encode_val chunk tv'))).
       destruct (zlt ofs (Ptrofs.unsigned i + z)); simpl in *. inv H. apply g.
  rewrite PMap.gso. trivial. intros N; subst. elim n; trivial.
Qed.

Lemma StoreEffectD: forall vaddr v b ofs
      (STE: StoreEffect vaddr v b ofs = true),
      exists i, vaddr = Vptr b i /\
        (Ptrofs.unsigned i) <= ofs < (Ptrofs.unsigned i + Z.of_nat (length v)).
Proof. intros.
  unfold StoreEffect in STE. destruct vaddr; inv STE.
  destruct (eq_block b0 b); inv H0.
  exists i.
  destruct (zle (Ptrofs.unsigned i) ofs); inv H1.
  destruct (zlt ofs (Ptrofs.unsigned i + Z.of_nat (length v))); inv H0.
  intuition.
Qed.

Lemma free_curWR m sp lo hi m' (FR: Mem.free m sp lo hi = Some m')
      b z (EFF: FreeEffect m lo hi sp b z = true):
      Mem.perm m b z Cur Writable.
Proof.
  apply FreeEffectD in EFF. destruct EFF as [? [? ?]]; subst.
  eapply Mem.perm_implies.
  eapply Mem.free_range_perm; eauto. constructor.
Qed.

Lemma storev_curWR ch m vaddr v m' (ST:Mem.storev ch m vaddr v = Some m')
      b z (EFF : StoreEffect vaddr (encode_val ch v) b z = true):
      Mem.perm m b z Cur Writable.
Proof.
  apply StoreEffectD in EFF. destruct EFF as [? [? [? ?]]]; subst.
  apply Mem.store_valid_access_3 in ST. apply ST.
  rewrite encode_val_length, <- size_chunk_conv in H1. lia.
Qed.

Lemma freelist_curWR l: forall m m' (FR: Mem.free_list m l = Some m')
      b z (EFF : FreelistEffect m l b z = true),
      Mem.perm m b z Cur Writable.
Proof. clear.
induction l; intros.
+ inv EFF.
+ destruct a as [[? ?] ?].
  simpl in FR.
  remember (Mem.free m b0 z0 z1) as f.
  destruct f; inv FR. symmetry in Heqf. simpl in EFF.
  remember (FreelistEffect m l b z) as q.
  destruct q; symmetry in Heqq; simpl in *.
  - clear EFF. specialize (IHl _ _ H0).
    remember (FreelistEffect m0 l b z) as w.
    destruct w; symmetry in Heqw.
    * eapply Mem.perm_free_3; eauto.
    * apply (FreelistEffect_same _ _ _ _ _ _ Heqf) in Heqw.
      rewrite Heqw in Heqq; discriminate.
      apply FreelistEffect_validblock in Heqq.
      eapply Mem.valid_block_free_1; eassumption.
  - eapply free_curWR; eassumption.
Qed.

repo: VST


text:
Require Import prelude chapter2.

Local Open Scope path_scope.

(*
Exercise 2.1. Show that the three obvious proofs of Lemma 2.1.2 [concatenation of paths] are pairwise equal.
*)
Section ex_2_1.
  Local Definition concat1 {A} {x y z : A} : x = y → y = z → x = z := λ p q, (match p with refl => id end) q.
  Local Definition concat2 {A} {x y z : A} : x = y → y = z → x = z := λ p q, (match q with refl => id end) p.
  Local Definition concat3 {A} {x y z : A} (p:x = y) (q:y = z) : x = z := match p, q with refl, refl => refl end.

  Context {A} {x y z : A} .
  Local Definition concat1_eq_concat2 : Π (p:x = y) (q:y = z), concat1 p q = concat2 p q.
  Proof. refine (path_ind (λ x y p, Π (q:y = z), concat1 p q = concat2 p q) _ x y). clear x y.
         refine (λ x, path_ind (λ x z q, concat1 1 q = concat2 1 q) _ x z).
         exact (λ _, refl).
  Defined.
  Local Definition concat2_eq_concat3 (p:x = y) (q:y = z) : concat2 p q = concat3 p q.
  Proof. destruct p, q. exact refl. Defined.
  Local Definition concat1_eq_concat3 (p:x = y) (q:y = z) : concat1 p q = concat3 p q.
  Proof. destruct p, q. exact refl. Defined.
End ex_2_1.

(*
Exercise 2.2. Show that the three equalities of proofs constructed in the previous exercise form a
commutative triangle. In other words, if the three definitions of concatenation are denoted by
 (p ·₁ q), (p ·₂ q), and (p ·₃ q),
then the concatenated equality
 (p ·₁ q) = (p ·₂ q) = (p ·₃ q)
is equal to the equality
 (p ·₁ q) = (p ·₃ q).
*)
Section ex_2_2.
  Context {A} {x y z : A} (p : x = y) (q : y = z).
  Goal (concat1_eq_concat2 p q) · (concat2_eq_concat3 p q) = concat1_eq_concat3 p q.
  Proof. destruct p, q. exact refl. Defined.
End ex_2_2.

(*
Exercise 2.3. Give a fourth, different, proof of Lemma 2.1.2, and prove that it is equal to the others.
*)

(*
Exercise 2.4. Define, by induction on n, a general notion of n-dimensional path in a type A,
simultaneously with the type of boundaries for such paths.
*)
Section ex_2_4.
  Local Open Scope nat_scope.
  Local Fixpoint npath (n:ℕ) : 𝓤 → 𝓤 := match n with
  | 0 => id
  | succ m => λ A, Σ (x y : A), npath m (x = y)
  end.
End ex_2_4.

(*
Exercise 2.5. Prove that the functions (2.3.6) and (2.3.7) are inverse equivalences.
*)
Section ex_2_5.
  Context {A B} `(p:x = y :> A) (f:A → B).

  (* This is just path_precomp_isequiv from chatper2. *)
  Goal (f x = f y) ≃ ((p # f x) = f y).
  Proof ((transport_const p (f x) ·); _).
End ex_2_5.

(*
Exercise 2.6. Prove that if p : x = y, then the function (p · –) : (y = z) → (x = z) is an
equivalence.
*)
(* See path_precomp_isequiv from chatper2. *)

(*
Exercise 2.7. State and prove a generalization of Theorem 2.6.5 from cartesian products to Σtypes.
*)
(* See ap_sig_eq from chapter2. *)

(*
Exercise 2.8. State and prove an analogue of Theorem 2.6.5 for coproducts.
*)
(* See inl_ap, inr_ap in chapter2. *)

(*
Exercise 2.9. Prove that coproducts have the expected universal property,
(A + B → X) ≃ (A → X) × (B → X).
Can you generalize this to an equivalence involving dependent functions?
*)
Section ex_2_9.
  Context `{!Funext}.
  Context {A B X : 𝓤}.

  Let F : (A + B → X) → (A → X) × (B → X)
  := λ f, (f ∘ inl, f ∘ inr).

  Let G : qinv F.
  Proof. exists ( λ p x, match x with
                         | inl a => π₁ p a
                         | inr b => π₂ p b
                         end ).
    split.
    + intros [f g]. exact refl.
    + intros f. apply funext. intros [a|b]; exact refl.
  Defined.

  Definition coproduct_universal : (A + B → X) ≃ (A → X) × (B → X) := (F; _).
End ex_2_9.

Section ex_2_9_ii.
  Context `{!Funext}.
  Context {A B : 𝓤} {C : A + B → 𝓤}.

  Let F : (Π x, C x) → (Π a, C (inl a)) × (Π b, C (inr b))
  := λ f, (λ a, f (inl a), λ b, f (inr b)).

  Let G : (Π a, C (inl a)) × (Π b, C (inr b)) → Π x, C x.
  Proof. intros [f g] [a|b]; [apply f | apply g]. Defined.

  Definition coproduct_universal_dep : (Π x, C x) ≃ (Π a, C (inl a)) × (Π b, C (inr b)).
  Proof. apply (Equiv_from_qinv_alt F G).
  + intros [f g]. exact refl.
  + intros f. apply funext. intros [a|b]; exact refl.
  Defined.
End ex_2_9_ii.

(*
Exercise 2.10. Prove that Σ-types are “associative”, in that for any A : U and families B : A → U
and C : (∑(x:A) B(x)) → U, we have
∑_(x:A) ∑_(y:B(x)) C((x, y)) ≃ ∑_(p:∑(x:A) B(x)) C(p) .
*)
Section ex_2_10.
  Context `{B:A → 𝓤} (C: (Σ x, B x) → 𝓤).

  Let F : (Σ x (y: B x), C (x; y)) → Σ p, C p
  := λ z, ((z.1; z.2.1); z.2.2).

  Let G : (Σ p, C p) → Σ x (y: B x), C (x; y).
  Proof. intros [[a b] c]. exists a. exists b. exact c. Defined.

  Definition sigma_assoc : (Σ x (y: B x), C (x; y)) ≃ Σ p, C p.
  Proof. apply (Equiv_from_qinv_alt F G).
  + intros [[a b] c]. exact refl.
  + intros [a [b c]]. exact refl.
  Defined.
End ex_2_10.

(*
Exercise 2.11. A (homotopy) commutative square

      h
   P ---> A
   |      |
 k |      | f
   v      v
   B ---> C
      g

consists of functions f, g, h, and k as shown, together with a path f ◦ h = g ◦ k. Note that
this is exactly an element of the pullback (P → A) ×P→C (P → B) as defined in (2.15.11). A
commutative square is called a (homotopy) pullback square if for any X, the induced map
(X → P) → (X → A) ×(X→C) (X → B)
is an equivalence. Prove that the pullback P :≡ A ×C B defined in (2.15.11) is the corner of a
pullback square.
*)
Definition pullback {A B C} (f:A → C) (g:B → C) := Σ a b, f a = g b.
Section ex_2_11.
  Context `{!Funext}.
  Context {A B C} (f:A → C) (g:B → C).
  Notation P := (pullback f g).

  Let h:P → A := pr₁.
  Let k:P → B := λ p, p.2.1.
  Let comm p : f (h p) = g (k p) := p.2.2.

  Context (X : 𝓤).
  Let square := pullback (compose (A:=X) f) (compose g).

  Let comm_hom (u:X → P) : f ∘ h ∘ u ~ g ∘ k ∘ u := λ x, comm (u x).
  Let F : (X → P) → square := λ u, (h ∘ u; (k ∘ u; funext (comm_hom u))).

  Let G : square → (X → P).
  Proof. intros [x₁[x₂ p]] x. exact (x₁ x; (x₂ x; happly p x)). Defined.

  Definition pullback_universal : (X → P) ≃ square.
  Proof. apply (Equiv_from_qinv_alt F G).
  + intros [x₁[x₂ p]].
    do 2 (apply sig⁼; exists refl). simpl.
    exact (ap funext 1 · (funext_unique p)⁻¹).
  + intros u. unfold compose, id, F, G. apply funext. intros x.
    do 2 (apply sig⁼; exists refl). simpl.
    exact (happly (funext_compute (comm_hom u)) x).
  Defined.
End ex_2_11.

(*
Exercise 2.12. Suppose given two commutative squares
A /

C /

E

B /D /F
and suppose that the right-hand square is a pullback square. Prove that the left-hand square is a
pullback square if and only if the outer rectangle is a pullback square.
*)

(*
Exercise 2.13. Show that (2 ≃ 2) ≃ 2.
*)
Require Import chapter3.
Section ex_2_13.
  Local Open Scope bool_scope.

  Instance: isequiv not₂.
  Proof. apply qinv_to_isequiv. exists not₂.
    split; intros [|]; exact refl.
  Defined.

  Let F : (𝟐 ≃ 𝟐) → 𝟐 := λ f, f 0.
  Let G : 𝟐 → (𝟐 ≃ 𝟐) := λ b, match b with 0 => 1%equiv | 1 => eqv not₂ end.

  Let aux1 (f:𝟐 → 𝟐) `{!isequiv f} : f 0 = f 1 ≃ 𝟎 := ((eqv (ap f))⁻¹ · bool_0_ne_1)%equiv.
  Let aux2 (f:𝟐 → 𝟐) `{!isequiv f} : ((0 = f 0) × (1 = f 1)) + ((1 = f 0) × (0 = f 1)).
  Proof. pose proof aux1 f as P.
    destruct (f 0) as [|], (f 1) as [|]; try destruct (P refl); [ right | left ]; exact (refl, refl).
  Defined.

  Let linv `{!Funext} (f:𝟐 ≃ 𝟐) : G (F f) = f :> (𝟐 → 𝟐) .
  Proof. destruct f as [f ?]. apply funext.
    enough ( (G (f 0) 0 = f 0) × (G (f 0) 1 = f 1) ) as P by (intros [|]; apply P).
    destruct (aux2 f) as [[[][]]|[[][]]]; exact (refl, refl).
  Defined.

  Definition bool_auto_equiv_bool `{!Funext} `{Hequiv:Π A B (f:A → B), isProp (isequiv f)} : (𝟐 ≃ 𝟐) ≃ 𝟐.
  Proof. apply (Equiv_from_qinv_alt F G).
  + intros [|]; exact refl.
  + intros f. eapply @subtype_eq.
    * intro p. apply Hequiv.
    * exact (linv f).
  Defined.
End ex_2_13.

(*
Exercise 2.14. Suppose we add to type theory the equality reflection rule which says that if there is
an element p : x = y, then in fact x ≡ y. Prove that for any p : x = x we have p ≡ reflx. (This
implies that every type is a set in the sense to be introduced in §3.1; see §7.2.)

Exercise 2.15. Show that Lemma 2.10.5 can be strengthened to
transportB
(p, –) =B(x)→B(y)
idtoeqv(apB
(p))
without using function extensionality. (In this and other similar cases, the apparently weaker
formulation has been chosen for readability and consistency.)
Exercise 2.16. Suppose that rather than function extensionality (Axiom 2.9.3), we suppose only
the existence of an element
funext : ∏
(A:U)
∏
(B:A→U)
∏
(f ,g:∏(x:A) B(x))
(f ∼ g) → (f = g)
(with no relationship to happly assumed). Prove that in fact, this is sufficient to imply the whole
function extensionality axiom (that happly is an equivalence). This is due to Voevodsky; its proof
is tricky and may require concepts from later chapters.
Exercise 2.17.
(i) Show that if A ' A
0 and B ' B
0
, then (A × B) ' (A
0 × B
0
).
(ii) Give two proofs of this fact, one using univalence and one not using it, and show that the
two proofs are equal.
(iii) Formulate and prove analogous results for the other type formers: Σ, →, Π, and +.
Exercise 2.18. State and prove a version of Lemma 2.4.3 for dependent functions
*)

author: jlottes

repo: hottbook

save_path: github-repos/coq/jlottes-hottbook


text:
Require Import Syntax.
Require Import Bindings.
Require Import BindingsFacts.
Require Import Sig.
Set Implicit Arguments.

Implicit Types EP EV LV V L : Set.

Fixpoint EV_map_it_sig
EP EV EV' LV L (f : EV → EV')
κ (N : it EP EV LV L κ)
Σ P Σ' P'
(H : it_sig N = exist _ Σ P)
(H' : it_sig (EV_map_it f N) = exist _ Σ' P')
{struct N} :
EV_map_is f Σ = Σ'.
Proof.
destruct N as [ F | κ N E ].
+ inversion H ; inversion H'.
  rewrite <- EP_EV_map_is.
  erewrite EV_map_map_is ; crush.
+ simpl EV_map_it in H'.
  destruct (it_sig N) as [ Σ₀ P₀ ] eqn:H₀.
  destruct (it_sig (EV_map_it f N)) as [ Σ₀' P₀' ] eqn:H₀'.
  assert (EV_map_is f Σ₀ = Σ₀') as HΣ₀Σ₀'.
  { eapply EV_map_it_sig with (N := N) ; eassumption. }

  destruct Σ₀ as [ | Σ₀ ] ; simpl in P₀ ; inversion P₀.
  assert (HΣ : Σ = EP_subst_is E Σ₀).
  {
    clear - H H₀.
    simpl in H ; rewrite H₀ in H.
    injection H ; auto.
  }
  destruct Σ₀' as [ | Σ₀'] ; simpl in P₀' ; inversion P₀'.
  assert (HΣ' : Σ' = EP_subst_is (EV_map_eff f E) Σ₀').
  {
    clear - H' H₀'.
    simpl in H' ; rewrite H₀' in H'.
    injection H' ; auto.
  }

  clear - HΣ HΣ' HΣ₀Σ₀'.
  simpl in HΣ₀Σ₀'.
  inversion HΣ₀Σ₀' ; subst Σ₀'.
  rewrite HΣ, HΣ' ; simpl.
  erewrite EP_bind_EV_map_is ; crush.
Qed.

Lemma EV_map_it_msig
EP EV EV' LV L (f : EV → EV')
(N : it EP EV LV L 𝕄) :
EV_map_ms f (it_msig N) = it_msig (EV_map_it f N).
Proof.
destruct (it_sig N) as [ Σ P ] eqn:H.
destruct (it_sig (EV_map_it f N)) as [ Σ' P' ] eqn:H'.
assert (Q : EV_map_is f Σ = Σ').
{ eapply EV_map_it_sig ; eassumption. }
simpl in Q.

destruct Σ as [ σ | ] ; [ | discriminate ].
destruct Σ' as [ σ' | ] ; [ | discriminate ].

unfold it_msig.
rewrite H, H'.
injection Q ; auto.
Qed.

Fixpoint LV_map_it_sig
EP EV LV LV' L (f : LV → LV')
κ (N : it EP EV LV L κ)
Σ P Σ' P'
(H : it_sig N = exist _ Σ P)
(H' : it_sig (LV_map_it f N) = exist _ Σ' P')
{struct N} :
LV_map_is f Σ = Σ'.
Proof.
destruct N as [ F | κ N E ].
+ inversion H ; inversion H'.
  rewrite <- EP_LV_map_is.
  rewrite <- EV_LV_map_is.
  erewrite LV_map_map_is ; crush.
+ simpl LV_map_it in H'.
  destruct (it_sig N) as [ Σ₀ P₀ ] eqn:H₀.
  destruct (it_sig (LV_map_it f N)) as [ Σ₀' P₀' ] eqn:H₀'.
  assert (LV_map_is f Σ₀ = Σ₀') as HΣ₀Σ₀'.
  {
    eapply LV_map_it_sig with (N := N).
    + apply H₀.
    + apply H₀'.
  }

  destruct Σ₀ as [ | Σ₀ ] ; simpl in P₀ ; inversion P₀.
  assert (HΣ : Σ = EP_subst_is E Σ₀).
  {
    clear - H H₀.
    simpl in H ; rewrite H₀ in H.
    injection H ; auto.
  }
  destruct Σ₀' as [ | Σ₀'] ; simpl in P₀' ; inversion P₀'.
  assert (HΣ' : Σ' = EP_subst_is (LV_map_eff f E) Σ₀').
  {
    clear - H' H₀'.
    simpl in H' ; rewrite H₀' in H'.
    injection H' ; auto.
  }

  clear - HΣ HΣ' HΣ₀Σ₀'.
  simpl in HΣ₀Σ₀'.
  inversion HΣ₀Σ₀' ; subst Σ₀'.
  rewrite HΣ, HΣ' ; simpl.
  erewrite EP_bind_LV_map_is ; crush.
Qed.

Lemma LV_map_it_msig
EP EV LV LV' L (f : LV → LV')
(N : it EP EV LV L 𝕄) :
LV_map_ms f (it_msig N) = it_msig (LV_map_it f N).
Proof.
destruct (it_sig N) as [ Σ P ] eqn:H.
destruct (it_sig (LV_map_it f N)) as [ Σ' P' ] eqn:H'.
assert (Q : LV_map_is f Σ = Σ').
{ eapply LV_map_it_sig ; eassumption. }
simpl in Q.

destruct Σ as [ σ | ] ; [ | discriminate ].
destruct Σ' as [ σ' | ] ; [ | discriminate ].

unfold it_msig.
rewrite H, H'.
injection Q ; auto.
Qed.

Fixpoint EV_bind_it_sig
EP EV EV' LV L (f : EV → eff EP EV' LV L)
κ (N : it EP EV LV L κ)
Σ P Σ' P'
(H : it_sig N = exist _ Σ P)
(H' : it_sig (EV_bind_it f N) = exist _ Σ' P')
{struct N} :
EV_bind_is f Σ = Σ'.
Proof.
destruct N as [ F | κ N E ].
+ inversion H ; inversion H'.
  generalize (LV_open_is (L_open_is (Signature F)) : is ∅ ∅ LV L).
  intro Σ₀.
  repeat rewrite EP_EV_map_is.
  erewrite EV_bind_map_is, EV_bind_is_id ; crush.
+ simpl EV_bind_it in H'.
  destruct (it_sig N) as [ Σ₀ P₀ ] eqn:H₀.
  destruct (it_sig (EV_bind_it f N)) as [ Σ₀' P₀' ] eqn:H₀'.
  assert (EV_bind_is f Σ₀ = Σ₀') as HΣ₀Σ₀'.
  { eapply EV_bind_it_sig with (N := N) ; eassumption. }

  destruct Σ₀ as [ | Σ₀ ] ; simpl in P₀ ; inversion P₀.
  assert (HΣ : Σ = EP_subst_is E Σ₀).
  {
    clear - H H₀.
    simpl in H ; rewrite H₀ in H.
    injection H ; auto.
  }
  destruct Σ₀' as [ | Σ₀'] ; simpl in P₀' ; inversion P₀'.
  assert (HΣ' : Σ' = EP_subst_is (EV_bind_eff f E) Σ₀').
  {
    clear - H' H₀'.
    simpl in H' ; rewrite H₀' in H'.
    injection H' ; auto.
  }

  clear - HΣ HΣ' HΣ₀Σ₀'.
  simpl in HΣ₀Σ₀'.
  inversion HΣ₀Σ₀' ; subst Σ₀'.
  rewrite HΣ, HΣ' ; simpl.
  erewrite EP_EV_bind_is ; try reflexivity.
  - intro ; unfold compose.
    erewrite EP_bind_map_eff, EP_map_eff_id, EP_bind_eff_id ; reflexivity.
  - destruct x ; simpl ; reflexivity.
Qed.

Lemma EV_bind_it_msig
EP EV EV' LV L (f : EV → eff EP EV' LV L)
(N : it EP EV LV L 𝕄) :
EV_bind_ms f (it_msig N) = it_msig (EV_bind_it f N).
Proof.
destruct (it_sig N) as [ Σ P ] eqn:H.
destruct (it_sig (EV_bind_it f N)) as [ Σ' P' ] eqn:H'.
assert (Q : EV_bind_is f Σ = Σ').
{ eapply EV_bind_it_sig ; eassumption. }
simpl in Q.

destruct Σ as [ σ | ] ; [ | discriminate ].
destruct Σ' as [ σ' | ] ; [ | discriminate ].

unfold it_msig.
rewrite H, H'.
injection Q ; auto.
Qed.

Fixpoint LV_bind_it_sig
EP EV LV LV' L (f : LV → lbl LV' L)
κ (N : it EP EV LV L κ)
Σ P Σ' P'
(H : it_sig N = exist _ Σ P)
(H' : it_sig (LV_bind_it f N) = exist _ Σ' P')
{struct N} :
LV_bind_is f Σ = Σ'.
Proof.
destruct N as [ F | κ N E ].
+ inversion H ; inversion H'.
  repeat rewrite EV_LV_map_is.
  repeat rewrite EP_LV_map_is.
  erewrite LV_bind_map_is, LV_bind_is_id ; crush.
+ simpl LV_bind_it in H'.
  destruct (it_sig N) as [ Σ₀ P₀ ] eqn:H₀.
  destruct (it_sig (LV_bind_it f N)) as [ Σ₀' P₀' ] eqn:H₀'.
  assert (LV_bind_is f Σ₀ = Σ₀') as HΣ₀Σ₀'.
  { eapply LV_bind_it_sig with (N := N) ; eassumption. }

  destruct Σ₀ as [ | Σ₀ ] ; simpl in P₀ ; inversion P₀.
  assert (HΣ : Σ = EP_subst_is E Σ₀).
  {
    clear - H H₀.
    simpl in H ; rewrite H₀ in H.
    injection H ; auto.
  }
  destruct Σ₀' as [ | Σ₀'] ; simpl in P₀' ; inversion P₀'.
  assert (HΣ' : Σ' = EP_subst_is (LV_bind_eff f E) Σ₀').
  {
    clear - H' H₀'.
    simpl in H' ; rewrite H₀' in H'.
    injection H' ; auto.
  }

  clear - HΣ HΣ' HΣ₀Σ₀'.
  simpl in HΣ₀Σ₀'.
  inversion HΣ₀Σ₀' ; subst Σ₀'.
  rewrite HΣ, HΣ' ; simpl.
  erewrite EP_LV_bind_is ; try reflexivity.
  destruct x ; simpl ; reflexivity.
Qed.

Lemma LV_bind_it_msig
EP EV LV LV' L (f : LV → lbl LV' L)
(N : it EP EV LV L 𝕄) :
LV_bind_ms f (it_msig N) = it_msig (LV_bind_it f N).
Proof.
destruct (it_sig N) as [ Σ P ] eqn:H.
destruct (it_sig (LV_bind_it f N)) as [ Σ' P' ] eqn:H'.
assert (Q : LV_bind_is f Σ = Σ').
{ eapply LV_bind_it_sig ; eassumption. }
simpl in Q.

destruct Σ as [ σ | ] ; [ | discriminate ].
destruct Σ' as [ σ' | ] ; [ | discriminate ].

unfold it_msig.
rewrite H, H'.
injection Q ; auto.
Qed.

Fixpoint L_bind_it_sig
EP EV LV L L' (f : L → lid L')
κ (N : it EP EV LV L κ)
Σ P Σ' P'
(H : it_sig N = exist _ Σ P)
(H' : it_sig (L_bind_it f N) = exist _ Σ' P')
{struct N} :
L_bind_is f Σ = Σ'.
Proof.
destruct N as [ F | κ N E ].
+ inversion H ; inversion H'.
  repeat rewrite LV_L_map_is.
  repeat rewrite EV_L_map_is.
  repeat rewrite EP_L_map_is.
  erewrite L_bind_map_is, L_bind_is_id ; crush.
+ simpl L_bind_it in H'.
  destruct (it_sig N) as [ Σ₀ P₀ ] eqn:H₀.
  destruct (it_sig (L_bind_it f N)) as [ Σ₀' P₀' ] eqn:H₀'.
  assert (L_bind_is f Σ₀ = Σ₀') as HΣ₀Σ₀'.
  { eapply L_bind_it_sig with (N := N) ; eassumption. }

  destruct Σ₀ as [ | Σ₀ ] ; simpl in P₀ ; inversion P₀.
  assert (HΣ : Σ = EP_subst_is E Σ₀).
  {
    clear - H H₀.
    simpl in H ; rewrite H₀ in H.
    injection H ; auto.
  }
  destruct Σ₀' as [ | Σ₀'] ; simpl in P₀' ; inversion P₀'.
  assert (HΣ' : Σ' = EP_subst_is (L_bind_eff f E) Σ₀').
  {
    clear - H' H₀'.
    simpl in H' ; rewrite H₀' in H'.
    injection H' ; auto.
  }

  clear - HΣ HΣ' HΣ₀Σ₀'.
  simpl in HΣ₀Σ₀'.
  inversion HΣ₀Σ₀' ; subst Σ₀'.
  rewrite HΣ, HΣ' ; simpl.
  erewrite EP_L_bind_is ; try reflexivity.
  destruct x ; simpl ; reflexivity.
Qed.

Lemma L_bind_it_msig
EP EV LV L L' (f : L → lid L')
(N : it EP EV LV L 𝕄) :
L_bind_ms f (it_msig N) = it_msig (L_bind_it f N).
Proof.
destruct (it_sig N) as [ Σ P ] eqn:H.
destruct (it_sig (L_bind_it f N)) as [ Σ' P' ] eqn:H'.
assert (Q : L_bind_is f Σ = Σ').
{ eapply L_bind_it_sig ; eassumption. }
simpl in Q.

destruct Σ as [ σ | ] ; [ | discriminate ].
destruct Σ' as [ σ' | ] ; [ | discriminate ].

unfold it_msig.
rewrite H, H'.
injection Q ; auto.
Qed.

author: yizhouzhang

repo: olaf-coq

save_path: github-repos/coq/yizhouzhang-olaf-coq


text:
From Coq Require Import String List ZArith.
From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.
Local Open Scope Z_scope.

Definition ___builtin_annot : ident := 11%positive.
Definition ___builtin_annot_intval : ident := 12%positive.
Definition ___builtin_bswap : ident := 5%positive.
Definition ___builtin_bswap16 : ident := 7%positive.
Definition ___builtin_bswap32 : ident := 6%positive.
Definition ___builtin_bswap64 : ident := 37%positive.
Definition ___builtin_clz : ident := 38%positive.
Definition ___builtin_clzl : ident := 39%positive.
Definition ___builtin_clzll : ident := 40%positive.
Definition ___builtin_ctz : ident := 41%positive.
Definition ___builtin_ctzl : ident := 42%positive.
Definition ___builtin_ctzll : ident := 43%positive.
Definition ___builtin_debug : ident := 55%positive.
Definition ___builtin_fabs : ident := 8%positive.
Definition ___builtin_fmadd : ident := 46%positive.
Definition ___builtin_fmax : ident := 44%positive.
Definition ___builtin_fmin : ident := 45%positive.
Definition ___builtin_fmsub : ident := 47%positive.
Definition ___builtin_fnmadd : ident := 48%positive.
Definition ___builtin_fnmsub : ident := 49%positive.
Definition ___builtin_fsqrt : ident := 9%positive.
Definition ___builtin_membar : ident := 13%positive.
Definition ___builtin_memcpy_aligned : ident := 10%positive.
Definition ___builtin_nop : ident := 54%positive.
Definition ___builtin_read16_reversed : ident := 50%positive.
Definition ___builtin_read32_reversed : ident := 51%positive.
Definition ___builtin_va_arg : ident := 15%positive.
Definition ___builtin_va_copy : ident := 16%positive.
Definition ___builtin_va_end : ident := 17%positive.
Definition ___builtin_va_start : ident := 14%positive.
Definition ___builtin_write16_reversed : ident := 52%positive.
Definition ___builtin_write32_reversed : ident := 53%positive.
Definition ___compcert_i64_dtos : ident := 22%positive.
Definition ___compcert_i64_dtou : ident := 23%positive.
Definition ___compcert_i64_sar : ident := 34%positive.
Definition ___compcert_i64_sdiv : ident := 28%positive.
Definition ___compcert_i64_shl : ident := 32%positive.
Definition ___compcert_i64_shr : ident := 33%positive.
Definition ___compcert_i64_smod : ident := 30%positive.
Definition ___compcert_i64_smulh : ident := 35%positive.
Definition ___compcert_i64_stod : ident := 24%positive.
Definition ___compcert_i64_stof : ident := 26%positive.
Definition ___compcert_i64_udiv : ident := 29%positive.
Definition ___compcert_i64_umod : ident := 31%positive.
Definition ___compcert_i64_umulh : ident := 36%positive.
Definition ___compcert_i64_utod : ident := 25%positive.
Definition ___compcert_i64_utof : ident := 27%positive.
Definition ___compcert_va_composite : ident := 21%positive.
Definition ___compcert_va_float64 : ident := 20%positive.
Definition ___compcert_va_int32 : ident := 18%positive.
Definition ___compcert_va_int64 : ident := 19%positive.
Definition _foo : ident := 4%positive.
Definition _main : ident := 60%positive.
Definition _s : ident := 56%positive.
Definition _x : ident := 1%positive.
Definition _x1 : ident := 58%positive.
Definition _y : ident := 2%positive.
Definition _y1 : ident := 57%positive.
Definition _y2 : ident := 59%positive.
Definition _z : ident := 3%positive.
Definition _t'1 : ident := 61%positive.
Definition _t'2 : ident := 62%positive.

Definition v_s := {|
  gvar_info := (Tstruct _foo noattr);
  gvar_init := (Init_int32 (Int.repr 5) ::
                Init_float32 (Float32.of_bits (Int.repr 1079655793)) ::
                Init_float64 (Float.of_bits (Int64.repr 0)) :: nil);
  gvar_readonly := false;
  gvar_volatile := false
|}.

Definition f_main := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_y1, tdouble) :: (_x1, tint) :: (_y2, tint) ::
               (_t'2, tfloat) :: (_t'1, tfloat) :: nil);
  fn_body :=
(Ssequence
  (Ssequence
    (Ssequence
      (Sset _t'2 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat))
      (Sset _y1 (Ecast (Etempvar _t'2 tfloat) tdouble)))
    (Ssequence
      (Sset _x1 (Efield (Evar _s (Tstruct _foo noattr)) _x tint))
      (Ssequence
        (Ssequence
          (Sset _t'1 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat))
          (Sset _y2 (Ecast (Etempvar _t'1 tfloat) tint)))
        (Ssequence
          (Sset _y1 (Efield (Evar _s (Tstruct _foo noattr)) _z tdouble))
          (Sreturn (Some (Econst_int (Int.repr 0) tint)))))))
  (Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.

Definition composites : list composite_definition :=
(Composite _foo Struct
   ((_x, tint) :: (_y, tfloat) :: (_z, tdouble) :: nil)
   noattr :: nil).

Definition global_definitions : list (ident * globdef fundef type) :=
((___builtin_bswap,
   Gfun(External (EF_builtin "__builtin_bswap"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tuint cc_default)) ::
 (___builtin_bswap32,
   Gfun(External (EF_builtin "__builtin_bswap32"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tuint cc_default)) ::
 (___builtin_bswap16,
   Gfun(External (EF_builtin "__builtin_bswap16"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tushort Tnil) tushort cc_default)) ::
 (___builtin_fabs,
   Gfun(External (EF_builtin "__builtin_fabs"
                   (mksignature (AST.Tfloat :: nil) (Some AST.Tfloat)
                     cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) ::
 (___builtin_fsqrt,
   Gfun(External (EF_builtin "__builtin_fsqrt"
                   (mksignature (AST.Tfloat :: nil) (Some AST.Tfloat)
                     cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) ::
 (___builtin_memcpy_aligned,
   Gfun(External (EF_builtin "__builtin_memcpy_aligned"
                   (mksignature
                     (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil)
                     None cc_default))
     (Tcons (tptr tvoid)
       (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid
     cc_default)) ::
 (___builtin_annot,
   Gfun(External (EF_builtin "__builtin_annot"
                   (mksignature (AST.Tint :: nil) None
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons (tptr tschar) Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (___builtin_annot_intval,
   Gfun(External (EF_builtin "__builtin_annot_intval"
                   (mksignature (AST.Tint :: AST.Tint :: nil) (Some AST.Tint)
                     cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
     tint cc_default)) ::
 (___builtin_membar,
   Gfun(External (EF_builtin "__builtin_membar"
                   (mksignature nil None cc_default)) Tnil tvoid cc_default)) ::
 (___builtin_va_start,
   Gfun(External (EF_builtin "__builtin_va_start"
                   (mksignature (AST.Tint :: nil) None cc_default))
     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
 (___builtin_va_arg,
   Gfun(External (EF_builtin "__builtin_va_arg"
                   (mksignature (AST.Tint :: AST.Tint :: nil) None
                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
     tvoid cc_default)) ::
 (___builtin_va_copy,
   Gfun(External (EF_builtin "__builtin_va_copy"
                   (mksignature (AST.Tint :: AST.Tint :: nil) None
                     cc_default))
     (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
 (___builtin_va_end,
   Gfun(External (EF_builtin "__builtin_va_end"
                   (mksignature (AST.Tint :: nil) None cc_default))
     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
 (___compcert_va_int32,
   Gfun(External (EF_external "__compcert_va_int32"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
 (___compcert_va_int64,
   Gfun(External (EF_external "__compcert_va_int64"
                   (mksignature (AST.Tint :: nil) (Some AST.Tlong)
                     cc_default)) (Tcons (tptr tvoid) Tnil) tulong
     cc_default)) ::
 (___compcert_va_float64,
   Gfun(External (EF_external "__compcert_va_float64"
                   (mksignature (AST.Tint :: nil) (Some AST.Tfloat)
                     cc_default)) (Tcons (tptr tvoid) Tnil) tdouble
     cc_default)) ::
 (___compcert_va_composite,
   Gfun(External (EF_external "__compcert_va_composite"
                   (mksignature (AST.Tint :: AST.Tint :: nil) (Some AST.Tint)
                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
     (tptr tvoid) cc_default)) ::
 (___compcert_i64_dtos,
   Gfun(External (EF_runtime "__compcert_i64_dtos"
                   (mksignature (AST.Tfloat :: nil) (Some AST.Tlong)
                     cc_default)) (Tcons tdouble Tnil) tlong cc_default)) ::
 (___compcert_i64_dtou,
   Gfun(External (EF_runtime "__compcert_i64_dtou"
                   (mksignature (AST.Tfloat :: nil) (Some AST.Tlong)
                     cc_default)) (Tcons tdouble Tnil) tulong cc_default)) ::
 (___compcert_i64_stod,
   Gfun(External (EF_runtime "__compcert_i64_stod"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tfloat)
                     cc_default)) (Tcons tlong Tnil) tdouble cc_default)) ::
 (___compcert_i64_utod,
   Gfun(External (EF_runtime "__compcert_i64_utod"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tfloat)
                     cc_default)) (Tcons tulong Tnil) tdouble cc_default)) ::
 (___compcert_i64_stof,
   Gfun(External (EF_runtime "__compcert_i64_stof"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tsingle)
                     cc_default)) (Tcons tlong Tnil) tfloat cc_default)) ::
 (___compcert_i64_utof,
   Gfun(External (EF_runtime "__compcert_i64_utof"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tsingle)
                     cc_default)) (Tcons tulong Tnil) tfloat cc_default)) ::
 (___compcert_i64_sdiv,
   Gfun(External (EF_runtime "__compcert_i64_sdiv"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) ::
 (___compcert_i64_udiv,
   Gfun(External (EF_runtime "__compcert_i64_udiv"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) ::
 (___compcert_i64_smod,
   Gfun(External (EF_runtime "__compcert_i64_smod"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) ::
 (___compcert_i64_umod,
   Gfun(External (EF_runtime "__compcert_i64_umod"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) ::
 (___compcert_i64_shl,
   Gfun(External (EF_runtime "__compcert_i64_shl"
                   (mksignature (AST.Tlong :: AST.Tint :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) ::
 (___compcert_i64_shr,
   Gfun(External (EF_runtime "__compcert_i64_shr"
                   (mksignature (AST.Tlong :: AST.Tint :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tulong (Tcons tint Tnil)) tulong cc_default)) ::
 (___compcert_i64_sar,
   Gfun(External (EF_runtime "__compcert_i64_sar"
                   (mksignature (AST.Tlong :: AST.Tint :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) ::
 (___compcert_i64_smulh,
   Gfun(External (EF_runtime "__compcert_i64_smulh"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) ::
 (___compcert_i64_umulh,
   Gfun(External (EF_runtime "__compcert_i64_umulh"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil)
                     (Some AST.Tlong) cc_default))
     (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) ::
 (___builtin_bswap64,
   Gfun(External (EF_builtin "__builtin_bswap64"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tlong)
                     cc_default)) (Tcons tulong Tnil) tulong cc_default)) ::
 (___builtin_clz,
   Gfun(External (EF_builtin "__builtin_clz"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_clzl,
   Gfun(External (EF_builtin "__builtin_clzl"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_clzll,
   Gfun(External (EF_builtin "__builtin_clzll"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tint)
                     cc_default)) (Tcons tulong Tnil) tint cc_default)) ::
 (___builtin_ctz,
   Gfun(External (EF_builtin "__builtin_ctz"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_ctzl,
   Gfun(External (EF_builtin "__builtin_ctzl"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_ctzll,
   Gfun(External (EF_builtin "__builtin_ctzll"
                   (mksignature (AST.Tlong :: nil) (Some AST.Tint)
                     cc_default)) (Tcons tulong Tnil) tint cc_default)) ::
 (___builtin_fmax,
   Gfun(External (EF_builtin "__builtin_fmax"
                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) ::
 (___builtin_fmin,
   Gfun(External (EF_builtin "__builtin_fmin"
                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) ::
 (___builtin_fmadd,
   Gfun(External (EF_builtin "__builtin_fmadd"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fmsub,
   Gfun(External (EF_builtin "__builtin_fmsub"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fnmadd,
   Gfun(External (EF_builtin "__builtin_fnmadd"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fnmsub,
   Gfun(External (EF_builtin "__builtin_fnmsub"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     (Some AST.Tfloat) cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_read16_reversed,
   Gfun(External (EF_builtin "__builtin_read16_reversed"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons (tptr tushort) Tnil) tushort cc_default)) ::
 (___builtin_read32_reversed,
   Gfun(External (EF_builtin "__builtin_read32_reversed"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
     (Tcons (tptr tuint) Tnil) tuint cc_default)) ::
 (___builtin_write16_reversed,
   Gfun(External (EF_builtin "__builtin_write16_reversed"
                   (mksignature (AST.Tint :: AST.Tint :: nil) None
                     cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
     tvoid cc_default)) ::
 (___builtin_write32_reversed,
   Gfun(External (EF_builtin "__builtin_write32_reversed"
                   (mksignature (AST.Tint :: AST.Tint :: nil) None
                     cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
     tvoid cc_default)) ::
 (___builtin_nop,
   Gfun(External (EF_builtin "__builtin_nop"
                   (mksignature nil None cc_default)) Tnil tvoid cc_default)) ::
 (___builtin_debug,
   Gfun(External (EF_external "__builtin_debug"
                   (mksignature (AST.Tint :: nil) None
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons tint Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (_s, Gvar v_s) :: (_main, Gfun(Internal f_main)) :: nil).

Definition public_idents : list ident :=
(_main :: _s :: ___builtin_debug :: ___builtin_nop ::
 ___builtin_write32_reversed :: ___builtin_write16_reversed ::
 ___builtin_read32_reversed :: ___builtin_read16_reversed ::
 ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub ::
 ___builtin_fmadd :: ___builtin_fmin :: ___builtin_fmax ::
 ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll ::
 ___builtin_clzl :: ___builtin_clz :: ___builtin_bswap64 ::
 ___compcert_i64_umulh :: ___compcert_i64_smulh :: ___compcert_i64_sar ::
 ___compcert_i64_shr :: ___compcert_i64_shl :: ___compcert_i64_umod ::
 ___compcert_i64_smod :: ___compcert_i64_udiv :: ___compcert_i64_sdiv ::
 ___compcert_i64_utof :: ___compcert_i64_stof :: ___compcert_i64_utod ::
 ___compcert_i64_stod :: ___compcert_i64_dtou :: ___compcert_i64_dtos ::
 ___compcert_va_composite :: ___compcert_va_float64 ::
 ___compcert_va_int64 :: ___compcert_va_int32 :: ___builtin_va_end ::
 ___builtin_va_copy :: ___builtin_va_arg :: ___builtin_va_start ::
 ___builtin_membar :: ___builtin_annot_intval :: ___builtin_annot ::
 ___builtin_memcpy_aligned :: ___builtin_fsqrt :: ___builtin_fabs ::
 ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: nil).

Definition prog : Clight.program :=
  mkprogram composites global_definitions public_idents _main Logic.I.

author: ildyria

repo: coq-verif-tweetnacl


text:
(* (c) P. Casteran *)

Set Implicit Arguments.
Require Export List.

(* potentialy infinite trees with internal nodes labeled with type A *)

CoInductive LTree (A:Set) : Set :=
  LLeaf : LTree A
| LBin : A -> LTree A -> LTree A -> LTree A.

Implicit Arguments LLeaf [A].

Definition is_LLeaf (A:Set) (t:LTree A) : Prop :=
  match t with
  | LLeaf => True
  | _ => False
  end.

Definition L_root (A:Set) (t:LTree A) : option A :=
  match t with
  | LLeaf => None
  | LBin r _ _ => Some r
  end.

Definition L_left_son (A:Set) (t:LTree A) : option (LTree A) :=
  match t with
  | LLeaf => None
  | LBin _ t1 _ => Some t1
  end.

Definition L_right_son (A:Set) (t:LTree A) : option (LTree A) :=
  match t with
  | LLeaf => None
  | LBin _ _ t2 => Some t2
  end.

Inductive direction : Set :=
  | d0 : direction (* left *)
  | d1 : direction (* right *).

Definition path := list direction.

(* The subtree at path p *)

Fixpoint L_subtree (A:Set) (p:path) (t:LTree A) {struct p} :
 option (LTree A) :=
  match p with
  | nil => Some t
  | d0 :: p' =>
      match t with
      | LLeaf => None
      | LBin a t1 t2 => L_subtree p' t1
      end
  | d1 :: p' =>
      match t with
      | LLeaf => None
      | LBin a t1 t2 => L_subtree p' t2
      end
  end.

(* the label at path p *)
Inductive label (A:Set) : Set :=
  | node_label : A -> label A
  | leaf_label : label A.

Definition LTree_label (A:Set) (t:LTree A) (p:path) :
  option (label A) :=
  match L_subtree p t with
  | None => None
  | Some t' =>
      match t' with
      | LLeaf => Some (leaf_label A)
      | LBin x _ _ => Some (node_label x)
      end
  end.

Lemma LTree_label_rw_leaf :
 forall (A:Set) (d:direction) (p:path),
   LTree_label (LLeaf (A:=A)) (d :: p) = None.
Proof.
  unfold LTree_label in |- *; intros A d p; case d; simpl in |- *; auto.
Qed.

Lemma LTree_label_rw_root_bin :
 forall (A:Set) (a:A) (t1 t2:LTree A),
   LTree_label (LBin a t1 t2) nil = Some (node_label a).
Proof.
  unfold LTree_label in |- *; simpl in |- *; auto.
Qed.

Lemma LTree_label_rw_root_leaf :
 forall A:Set, LTree_label (LLeaf (A:=A)) nil = Some (leaf_label A).
Proof.
  unfold LTree_label in |- *; simpl in |- *; auto.
Qed.

Lemma LTree_label_rw0 :
 forall (A:Set) (a:A) (t1 t2:LTree A) (p:path),
   LTree_label (LBin a t1 t2) (d0 :: p) = LTree_label t1 p.
Proof.
  unfold LTree_label in |- *; simpl in |- *; auto.
Qed.

Lemma LTree_label_rw1 :
 forall (A:Set) (a:A) (t1 t2:LTree A) (p:path),
   LTree_label (LBin a t1 t2) (d1 :: p) = LTree_label t2 p.
Proof.
  unfold LTree_label in |- *; simpl in |- *; auto.
Qed.

author: kalfazed

repo: Coq---Programming-Language


text:
(** * kat_untyping: untyping theorem for KAT *)

(** We prove a strong untyping theorem for KAT:
   - types can be erased (as in the untyping theorem in [untyping])
   - predicate variables of distinct types can be merged

   The proofs are quite simple since we can perform them at the level
   of guarded string languages: unlike for KA, we proved typed
   completeness of KAT w.r.t. these models. *)

Require Import kat gregex ugregex ordinal positives glang.
Set Implicit Arguments.

Section s.
Variable Pred: nat.
Notation Atom := (ord (pow2 Pred)).
Notation Sigma := positive.
Variables src tgt: Sigma -> positive.
Notation pred := (ord Pred).
Notation gregex := (gregex_kat_ops Pred src tgt).
Notation ugregex := (ugregex_monoid_ops Pred ugregex_tt ugregex_tt).
Notation glang := (@gregex.lang Pred src tgt).
Notation uglang := (@ugregex.lang Pred).
Notation typed := (@typed' Atom src tgt).

(** type-erasing function on extended regular expressions *)

Fixpoint gerase n m (e: gregex n m): ugregex :=
  match e with
    | g_zer _ _ _ => 0
    | g_prd _ _ p => u_prd p
    | g_pls e f => gerase e + gerase f
    | g_dot e f => gerase e ⋅ gerase f
    | g_itr e => (gerase e)^+
    | g_var i => u_var _ i
  end.

(** charaterisation of the guarded string language of erased epressions *)

Lemma uglang_gerase n m (e: gregex n m):
  uglang (gerase e) ≡ eval (fun _ => traces_tt) (fun _ => @lsyntax.e_var _) tsingle e.
Proof.
  induction e; simpl gerase.
   apply lang_0.
   simpl. rewrite lsyntax.eval_var. reflexivity.
   reflexivity.
   now apply cup_weq.
   now apply dot_weq.
   now apply itr_weq.
Qed.

Corollary gerase_weq n m: Proper (weq ==> weq) (@gerase n m).
Proof. intros ? ? H. simpl. unfold u_weq. rewrite 2uglang_gerase. apply (H _ _ _). Qed.

(** the a priori untyped guarded string language of a typed gregex is necessarily typed *)

Lemma typed_uglang_gerase n m (e: gregex n m): typed n m (uglang (gerase e)).
Proof.
  induction e.
   intros [|] H. discriminate. destruct H.
   apply typed'_inj.
   apply typed'_single.
   revert IHe1 IHe2. apply typed'_cup.
   revert IHe1 IHe2. apply typed'_dot.
   revert IHe. apply typed'_itr.
Qed.

(** we can thus recover the typed language out of the untyped one *)

Notation restrict := (restrict src tgt).

Theorem untype_glang n m (e: gregex n m): glang e ≡ restrict n m (uglang (gerase e)).
Proof.
  symmetry. induction e.
   setoid_rewrite lang_0. apply restrict_0.
   setoid_rewrite restrict_inj. simpl. unfold ttraces_weq. simpl. now rewrite lsyntax.eval_var.
   apply restrict_single.
   etransitivity. 2: apply cup_weq; eassumption. apply restrict_pls.
   etransitivity. 2: apply dot_weq; eassumption. apply restrict_dot; apply typed_uglang_gerase.
   etransitivity. 2: apply itr_weq; eassumption. apply restrict_itr; apply typed_uglang_gerase.
Qed.

End s.

author: damien-pous

repo: relation-algebra


text:
Require Import Category.
Require Import Eq_Category.
Require Import Category2.
Require Import CategoryAsCategory2.
Require Import Category2AsCategory.

Theorem ToCatToCat2 : forall (A:Type) (c:Category A),
    toCategory (toCategory2 c) = c.
Proof.
    intros A c. apply eq_Category.
    - intros f. reflexivity.
    - intros f. reflexivity.
    - intros f g. reflexivity.
Qed.

(* When creating a Category from a Category2, we are effectively discarding
   the type of objects Obj, which is not needed since it can be replaced
   by the type of identity arrows. If we attempt to go back to an object
   of type Category2, we are constructing a new type of objects based on
   the identity arrows. There is no hope to recover the initial 'Obj' from
   this construction, and therefore, the equality of the following theorem
   is not even properly typed, let alone true or false...

   We know that toCategory . toCategory2 is the identity on Category A,
   but we are not able to write anything like toCategory2 . toCategory
   being the identity on Category2 Obj Mor
*)

(*
Theorem ToCat2ToCat : forall (Obj Mor:Type) (c:Category2 Obj Mor),
    toCategory2 (toCategory c) = c.
*)

author: possientis

repo: Prog

save_path: github-repos/coq/possientis-Prog


text:
From mathcomp
  Require Import ssreflect.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Powerset.

Lemma Formula_1_4 (T : Type) (A B C : Ensemble T) : Included T A B /\ Included T B C -> Included T A C.
Proof.
  case.
  move=> HAinclB HBinclC x HxinA.
  apply (HBinclC x).
  apply (HAinclB x).
  by [].
Qed.

Lemma Formula_1_5 (T : Type) (A : Ensemble T) : Included T (Empty_set T) A.
Proof.
  move=> x HxinEmptySet.
  by [].
Qed.

Lemma Formula_2_2_1 (T : Type) (A B : Ensemble T) : Included T A (Union T A B).
Proof.
  move=> x HxinA.
  left.
  by [].
Qed.

Lemma Formula_2_2_2 (T : Type) (A B : Ensemble T) : Included T B (Union T A B).
Proof.
  move=> x HxinB.
  right.
  by [].
Qed.

Lemma Formula_2_3 (T : Type) (A B C : Ensemble T) : Included T A C /\ Included T B C -> Included T (Union T A B) C.
Proof.
  case.
  move=> HAinclC HBinclC x [y | z].
  + apply HAinclC.
  + apply HBinclC.
Qed.

Lemma Formula_2_4 (T : Type) (A : Ensemble T) : (Union T A A) = A.
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinAcupA.
    destruct HxinAcupA as [x HxinA | x HxinA].
    + by [].
    + by [].
  + apply (Formula_2_2_1 T A A).
Qed.

Lemma Formula_2_5 (T : Type) (A B : Ensemble T) : (Union T A B) = (Union T B A).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinAcupB.
    destruct HxinAcupB as [x HxinA | x HxinB].
    + right.
      by [].
    + left.
      by [].
  + move=>x HxinBcupA.
    destruct HxinBcupA as [x HxinB | x HxinA].
    + right.
      by [].
    + left.
      by [].
Qed.

Lemma Formula_2_6 (T : Type) (A B C : Ensemble T) : (Union T (Union T A B) C) = (Union T A (Union T B C)).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x [ab | c].
    + move=> [a | b].
      + left.
        by [].
      + right.
        left.
        by [].
    + move=> HcinC.
      right.
      right.
      by [].
  + move=> x [a | bc].
    + move=> HainA.
      left.
      left.
      by [].
    + move=> [b | c].
      + left.
        right.
        by [].
      + right.
        by [].
Qed.

Lemma Formula_2_7 (T : Type) (A B : Ensemble T) : Included T A B <-> (Union T A B) = B.
Proof.
  apply conj.
  + move=> HAinclB.
    apply Extensionality_Ensembles.
    apply conj.
    + move=> x HxinAcupB.
      destruct HxinAcupB as [x HxinA| x HxinB].
      + apply HAinclB.
        by [].
      + by [].
    + move=> x HxinB.
      right.
      by [].
  + move=> Heq.
    rewrite -Heq.
    apply Formula_2_2_1.
Qed.

Lemma Formula_2_8 (T : Type) (A B C : Ensemble T) : Included T A B -> Included T (Union T A C) (Union T B C).
Proof.
  move=> HAinclB x HxinAcupC.
  destruct HxinAcupC as [x HxinA | x HxinC].
  + left.
    apply HAinclB.
    by [].
  + right.
    by [].
Qed.

Lemma Formula_2_9 (T : Type) (A : Ensemble T) : (Union T (Empty_set T) A) = A.
Proof.
  apply Formula_2_7.
  apply Formula_1_5.
Qed.

Lemma Formula_2_2'_1 (T : Type) (A B : Ensemble T) : Included T (Intersection T A B) A.
Proof.
  move=> x [y HyinA HyinB].
  by [].
Qed.

Lemma Formula_2_2'_2 (T : Type) (A B : Ensemble T) : Included T (Intersection T A B) B.
Proof.
  move=> x [y HyinA HyinB].
  by [].
Qed.

Lemma Formula_2_3' (T : Type) (A B C : Ensemble T) : Included T C A /\ Included T C B -> Included T C (Intersection T A B).
Proof.
  move=> [HCinclA HCinclB] x HxinC.
  apply Intersection_intro.
  + apply HCinclA.
    by [].
  + apply HCinclB.
    by [].
Qed.

Lemma Formula_2_4' (T : Type) (A : Ensemble T) : (Intersection T A A) = A.
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + apply (Formula_2_2'_1 T A A).
  + move=> x HxinA.
    apply Intersection_intro.
    + by [].
    + by [].
Qed.

Lemma Formula_2_5' (T : Type) (A B : Ensemble T) : (Intersection T A B) = (Intersection T B A).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinAcapB.
    destruct HxinAcapB as [x HinA HinB].
    apply Intersection_intro.
    + by [].
    + by [].
  + move=> x HxinBcapA.
    destruct HxinBcapA as [x HinB HinA].
    apply Intersection_intro.
    + by [].
    + by [].
Qed.

Lemma Formula_2_6' (T : Type) (A B C : Ensemble T) : (Intersection T (Intersection T A B) C) = (Intersection T A (Intersection T B C)).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinAcapBcapC.
    destruct HxinAcapBcapC as [x HxinAcapB HxinC].
    destruct HxinAcapB as [x HxinA HxinB].
    apply Intersection_intro.
    + by [].
    + apply Intersection_intro.
      + by [].
      + by [].
  + move=> x HxinAcapBcapC.
    destruct HxinAcapBcapC as [x HxinA HxinBcapC].
    destruct HxinBcapC as [x HxinB HxinC].
    apply Intersection_intro.
    + apply Intersection_intro.
      + by [].
      + by [].
    + by [].
Qed.

Lemma Formula_2_7' (T : Type) (A B : Ensemble T) : Included T A B <-> (Intersection T A B) = A.
Proof.
  apply conj.
  + move=> HAinclB.
    apply Extensionality_Ensembles.
    apply conj.
    + move=> x HxinAcapB.
      destruct HxinAcapB as [x HxinA HxinB].
      by [].
    + move=> x HxinAcapB.
      apply Intersection_intro.
      + by [].
      + apply HAinclB.
        by [].
  + move=> Heq.
    rewrite -Heq.
    apply (Formula_2_2'_2 T A B).
Qed.

Lemma Formula_2_8' (T : Type) (A B C : Ensemble T) : Included T A B -> Included T (Intersection T A C) (Intersection T B C).
Proof.
  move=> HAinclB x HxinAcapB.
  destruct HxinAcapB as [x HxinA HxinC].
  apply Intersection_intro.
  + apply HAinclB.
    by [].
  + by [].
Qed.

Lemma Formula_2_9' (T : Type) (A : Ensemble T) : Intersection T (Empty_set T) A = (Empty_set T).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x Hxin.
    destruct Hxin as [x HxinEmp HxinA].
    by [].
  + move=> x Hxin.
    by [].
Qed.

Lemma Formula_2_10 (T : Type) (A B C : Ensemble T) : Intersection T (Union T A B) C = Union T (Intersection T A C) (Intersection T B C).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinCap.
    destruct HxinCap as [x HxinCup HxinC].
    destruct HxinCup as [x HxinA | HxinB].
    + left.
      by apply Intersection_intro.
    + right.
      by apply Intersection_intro.
  + move=> x HxinCup.
    destruct HxinCup as [x HxinAcapC | x HxinBcapC].
    + destruct HxinAcapC as [x HxinA HxinC].
      apply Intersection_intro.
      + by left.
      + by [].
    + destruct HxinBcapC as [x HxinB HxinC].
      apply Intersection_intro.
      + by right.
      + by [].
Qed.

Lemma Formula_2_10' (T : Type) (A B C : Ensemble T) : Union T (Intersection T A B) C = Intersection T (Union T A C) (Union T B C).
Proof.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> x HxinCup.
    destruct HxinCup as [x HxinCap | x HxinC].
    + destruct HxinCap as [x HxinA HxinB].
      by apply Intersection_intro; left.
    + by split; right.
  + move=> x HxinCap.
    destruct HxinCap as [x HxinAcupC HxinBcupC].
    destruct HxinAcupC as [x HxinA | x HxinC].
    + destruct HxinBcupC as [x HxinB | x HxinC].
      + by left; split.
      + by right.
    + destruct HxinBcupC as [x HxinB | x HxinC'].
      + by right.
      + by right.
Qed.

Lemma Formula_2_11 (T : Type) (A B : Ensemble T) : Intersection T (Union T A B) A = A.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinAcupB.
    destruct HxinAcupB as [x HxinAcupB HxinA].
    by [].
  + move=> x HxinA.
    split.
    + by left.
    + by [].
Qed.

Lemma Formula_2_11' (T : Type) (A B : Ensemble T) : Union T (Intersection T A B) A = A.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinCup.
    destruct HxinCup as [x HxinAcapB | x HxinA].
    + by destruct HxinAcapB as [x HxinA HxinB].
    + by [].
  + move=> x HxinA.
    by right.
Qed.

Lemma Formula_2_12_1 (T : Type) (A : Ensemble T) : Union T A (Complement T A) = Full_set T.
Proof.
  apply Extensionality_Ensembles.
  split.
  + by [].
  + move=> x _.
    by case: (classic (In T A x)); [left | right].
Qed.

Lemma Formula_2_12_2 (T : Type) (A : Ensemble T) : Intersection T A (Complement T A) = Empty_set T.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinAcapAc.
    destruct HxinAcapAc as [x HxinA HxinAc].
    by [].
  + by [].
Qed.

Lemma Formula_2_13 (T : Type) (A : Ensemble T) : Complement T (Complement T A) = A.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinAcc.
    apply NNPP.
    by [].
  + move=> x HxinA HxinAc.
    apply (HxinAc HxinA).
Qed.

Lemma Formula_2_14_1 (T : Type) : Complement T (Empty_set T) = Full_set T.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x Hx.
    by [].
  + move=> x H1 H2.
    by [].
Qed.

Lemma Formula_2_14_2 (T : Type) : Complement T (Full_set T) = Empty_set T.
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x H.
    by case H.
  + move=> x H.
    by [].
Qed.

Lemma Formula_2_15 (T : Type) (A B : Ensemble T) : Included T A B <-> Included T (Complement T B) (Complement T A).
Proof.
  split.
  + move=> HAinclB x HxinBc HxinA.
    apply HxinBc.
    apply HAinclB.
    by [].
  + move=> HBcinclAc x HxinA.
    apply NNPP.
    move=> HxnotinB.
    apply (HBcinclAc x HxnotinB).
    by [].
Qed.

Lemma Formula_2_16 (T : Type) (A B : Ensemble T) : Complement T (Union T A B) = Intersection T (Complement T A) (Complement T B).
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinAcupBc.
    split.
    + move=> HxinA.
      apply HxinAcupBc.
      left.
      by [].
    + move=> HxinB.
      apply HxinAcupBc.
      right.
      by [].
  + move=> x HxinAccapBc HxinAcupB.
    destruct HxinAccapBc as [x HxinAc HxinBc].
    destruct HxinAcupB as [x HxinA | x HxinB].
    + apply HxinAc.
      by [].
    + apply HxinBc.
      by [].
Qed.

Lemma Formula_2_16' (T : Type) (A B : Ensemble T) : Complement T (Intersection T A B) = Union T (Complement T A) (Complement T B).
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> x HxinAcapBc.
    case (classic (In T A x)).
    + move=> HxinA.
      right.
      move=> HxinB.
      apply HxinAcapBc.
      by split.
    + move=> HxnotinA.
      by left.
  + move=> x HxinAccupBc HxinAcapB.
    destruct HxinAcapB as [x HxinA HxinB].
    by destruct HxinAccupBc as [x HxinAc | x HxinBc].
Qed.

Lemma Formula_p18_l10 (T : Type) : (Full_set T) = (Empty_set T) -> (Power_set T (Full_set T)) = (Singleton (Ensemble T) (Empty_set T)).
Proof.
  move=> HFullEqEmpty.
  apply Extensionality_Ensembles.
  apply conj.
  + move=> X HXinPFull.
    have: (X = Empty_set T).
    + apply Extensionality_Ensembles.
      split.
      + rewrite -HFullEqEmpty.
        by [].
      + by [].
    + move=> HXeqEmpty.
      rewrite HXeqEmpty.
      by [].
  + move=> X HX.
    apply Definition_of_Power_set.
    move=> x HxinX.
    apply Full_intro.
Qed.

Lemma Formula_p18_l10' (T : Type) : (Power_set T (Empty_set T)) = (Singleton (Ensemble T) (Empty_set T)).
Proof.
  apply Extensionality_Ensembles.
  split.
  + move=> X HXinPEmpty.
    destruct HXinPEmpty as [X HXinclEmpty].
    have: (X = Empty_set T).
    + apply Extensionality_Ensembles.
      split.
      + by [].
      + apply Empty_set_minimal.
    + move=> HXEqEmpty.
      rewrite HXEqEmpty.
      apply In_singleton.
  + move=> X.
    apply Singleton_ind.
    apply Definition_of_Power_set.
    move=> x.
    by [].
Qed.

repo: theorem-proving-in-coq