text:
Require Import Coqlib.
Require Import STS.
Require Import Behavior.
Require Import ModSem.
Require Import Skeleton.
Require Import PCM.
Require Import Any.
Require Export HoareDef STB.
Require Import Hoareproof0 Hoareproof1 Hoareproof2.
Require Import SimModSem ProofMode.

Set Implicit Arguments.

Lemma fold_right_map
      XS XI YS YI
      (xs: XS) (xi: list XI)
      (xadd: XI -> XS -> XS)

      (* (ys: YS) (yi: list YI) *)
      (yadd: YI -> YS -> YS)

      (fs: XS -> YS)
      (fi: XI -> YI)
      (HOM: forall xi xs, fs (xadd xi xs) = yadd (fi xi) (fs xs))
  :
    <<EQ: fs (fold_right xadd xs xi) = fold_right yadd (fs xs) (List.map fi xi)>>
.
Proof.
  r. ginduction xi; ii; ss.
  rewrite HOM. f_equal. eapply IHxi; et.
Qed.

(*** TODO: move to Coqlib ***)
Lemma find_app
      X (xs0 xs1: list X) (f: X -> bool) x
      (FIND: find f xs0 = Some x)
  :
    <<FIND: find f (xs0 ++ xs1) = Some x>>
.
Proof.
  revert_until xs0. induction xs0; ii; ss. des_ifs. erewrite IHxs0; et.
Qed.

Section CANCELSTB.

  Context `{Σ: GRA.t}.

  Variable mds: list SMod.t.

  Let sk: Sk.t := SMod.get_sk mds.

  Let _mss: Sk.t -> list SModSem.t := fun sk => (List.map ((flip SMod.get_modsem) sk) mds).
  Let _sbtb: Sk.t -> list (gname * fspecbody) := fun sk => (List.flat_map (SModSem.fnsems) (_mss sk)).
  Let _stb: Sk.t -> list (gname * fspec) := fun sk => List.map (fun '(fn, fs) => (fn, fs.(fsb_fspec))) (_sbtb sk).

  Let mss: list SModSem.t := _mss sk.
  Let sbtb: list (gname * fspecbody) := _sbtb sk.

  Variable stb: Sk.t -> gname -> option fspec.
  Hypothesis STBCOMPLETE:
    forall fn fsp (FIND: alist_find fn (_stb sk) = Some fsp), stb sk fn = Some fsp.
  Hypothesis STBSOUND:
    forall fn (FIND: alist_find fn (_stb sk) = None),
      (<<NONE: stb sk fn = None>>) \/ (exists fsp, <<FIND: stb sk fn = Some fsp>> /\ <<TRIVIAL: forall x, fsp.(measure) x = ord_top>>).

  Let mds_src: list Mod.t := List.map (SMod.to_src) mds.
  Let mds_tgt: list Mod.t := List.map (SMod.to_tgt stb) mds.

  Let W: Type := p_state.
  (* Let wf: Ord.t -> W -> W -> Prop := top3. *)

  Opaque EventsL.interp_Es.

  Let ms_src: ModSemL.t := ModL.enclose (Mod.add_list mds_src).
  Let ms_tgt: ModSemL.t := ModL.enclose (Mod.add_list mds_tgt).

  Section STRONGER.
  Context {CONFS CONFT: EMSConfig}.
  Hypothesis (FINSAME: (@finalize CONFS) = (@finalize CONFT)).

  Theorem adequacy_type_arg_stb
          (MAINM:
             forall (main_fsp: fspec) (MAIN: stb sk "main" = Some main_fsp),
             exists (x: main_fsp.(meta)) entry_r,
               (<<PRE: main_fsp.(precond) None x (@initial_arg CONFS) (@initial_arg CONFT) entry_r>>) /\
               (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
               (<<WFR: URA.wf (entry_r ⋅ fold_left (⋅) (List.map SModSem.initial_mr mss) ε)>>) /\
               (<<RET: forall ret_src ret_tgt,
                   ((main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ ⌜ret_src = ret_tgt⌝)>>))
    :
      Beh.of_program (@ModL.compile _ CONFT (Mod.add_list mds_tgt)) <1=
      Beh.of_program (@ModL.compile _ CONFS (Mod.add_list mds_src)).
  Proof.
    ii. eapply adequacy_type_m2s; et.
    eapply adequacy_type_m2m; et.
    eapply adequacy_type_t2m; et.
    i. exploit MAINM; et. i. des. esplits; et.
    i. specialize (RET ret_src ret_tgt). uipropall.
    hexploit RET; et. i. rr in H. uipropall.
    all:ss.
  Qed.
  End STRONGER.

  Context {CONF: EMSConfig}.
  Variable entry_r: Σ.

  Hypothesis WFR: URA.wf (entry_r ⋅ SMod.get_initial_mrs mds sk).

  Hypothesis MAINM: forall (main_fsp: fspec) (MAIN: stb sk "main" = Some main_fsp),
      exists (x: main_fsp.(meta)),
        (<<PRE: Own (entry_r) -∗ main_fsp.(precond) None x initial_arg initial_arg>>) /\
        (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
        (<<RET: forall ret_src ret_tgt,
            (main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ (⌜ret_src = ret_tgt⌝)>>).

  Theorem adequacy_type_stb: refines_closed (Mod.add_list mds_tgt) (Mod.add_list mds_src).
  Proof.
    ii. eapply adequacy_type_arg_stb; et.
    i. hexploit MAINM; et. i. des. esplits; et.
    { eapply to_semantic.
      { eapply PRE.  }
      { eapply URA.wf_mon; et. }
    }
    { r_wf WFR. unfold SMod.get_initial_mrs. ss. unfold mss, _mss.
      rewrite List.map_map. ss. }
  Qed.

End CANCELSTB.

Section CANCEL.

  Context `{Σ: GRA.t}.

  Variable mds: list SMod.t.

  Let sk: Sk.t := SMod.get_sk mds.
  Let stb0: Sk.t -> gname -> option fspec := fun sk => to_stb (SMod.get_stb mds sk).
  Let stb1: Sk.t -> gname -> option fspec := fun sk => to_closed_stb (SMod.get_stb mds sk).

  Let mds_src: list Mod.t := List.map (SMod.to_src) mds.
  Let mds_tgt0: list Mod.t := List.map (SMod.to_tgt stb0) mds.
  Let mds_tgt1: list Mod.t := List.map (SMod.to_tgt stb1) mds.

  Section STRONGER.
  Context {CONFS CONFT: EMSConfig}.
  Hypothesis (FINSAME: (@finalize CONFS) = (@finalize CONFT)).

  Theorem adequacy_type_arg
          (MAINM:
             forall (main_fsp: fspec) (MAIN: stb0 sk "main" = Some main_fsp),
             exists (x: main_fsp.(meta)) entry_r,
               (<<PRE: main_fsp.(precond) None x (@initial_arg CONFS) (@initial_arg CONFT) entry_r>>) /\
               (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
               (<<WFR: URA.wf (entry_r ⋅ SMod.get_initial_mrs mds sk)>>) /\
               (<<RET: forall ret_src ret_tgt,
                   ((main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ ⌜ret_src = ret_tgt⌝)>>))
    :
      Beh.of_program (@ModL.compile _ CONFT (Mod.add_list mds_tgt0)) <1=
      Beh.of_program (@ModL.compile _ CONFS (Mod.add_list mds_src)).
  Proof.
    eapply adequacy_type_arg_stb; et.
    { unfold stb0, sk, SMod.get_stb, SMod.get_sk. unfold to_stb.
      rewrite flat_map_map. ss. }
    { i. left. rewrite <- FIND.
      unfold stb0, to_stb, SMod.get_stb.
      rewrite flat_map_map. ss. }
    { i. hexploit MAINM; et. i. des. esplits; et.
      r_wf WFR. rewrite map_map. ss. }
  Qed.

  Theorem adequacy_type_arg_closed
          (MAINM:
             forall (main_fsp: fspec) (MAIN: stb1 sk "main" = Some main_fsp),
             exists (x: main_fsp.(meta)) entry_r,
               (<<PRE: main_fsp.(precond) None x (@initial_arg CONFS) (@initial_arg CONFT) entry_r>>) /\
               (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
               (<<WFR: URA.wf (entry_r ⋅ SMod.get_initial_mrs mds sk)>>) /\
               (<<RET: forall ret_src ret_tgt,
                   ((main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ ⌜ret_src = ret_tgt⌝)>>))
    :
      Beh.of_program (@ModL.compile _ CONFT (Mod.add_list mds_tgt1)) <1=
      Beh.of_program (@ModL.compile _ CONFS (Mod.add_list mds_src)).
  Proof.
    eapply adequacy_type_arg_stb; et.
    { unfold stb1, sk, SMod.get_stb, SMod.get_sk. unfold to_closed_stb.
      rewrite flat_map_map. i. ss. unfold map_snd. rewrite FIND. auto. }
    { unfold stb1, sk, SMod.get_stb, SMod.get_sk. unfold to_closed_stb.
      rewrite flat_map_map. ss. i. right. unfold map_snd.
      rewrite FIND. esplits; et. }
    { i. exploit MAINM; et. i. des. esplits; et.
      r_wf WFR. rewrite map_map. ss. }
  Qed.
  End STRONGER.

  Context {CONF: EMSConfig}.
  Variable entry_r: Σ.

  Hypothesis WFR: URA.wf (entry_r ⋅ SMod.get_initial_mrs mds sk).

  Section TYPE0.
  Hypothesis MAINM: forall (main_fsp: fspec) (MAIN: stb0 sk "main" = Some main_fsp),
      exists (x: main_fsp.(meta)),
        (<<PRE: Own (entry_r) -∗ main_fsp.(precond) None x initial_arg initial_arg>>) /\
        (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
        (<<RET: forall ret_src ret_tgt,
            (main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ (⌜ret_src = ret_tgt⌝)>>).

  Theorem adequacy_type: refines_closed (Mod.add_list mds_tgt0) (Mod.add_list mds_src).
  Proof.
    ii. eapply adequacy_type_arg; et.
    i. hexploit MAINM; et. i. des. esplits; et.
    { eapply to_semantic.
      { uipropall. }
      { eapply URA.wf_mon; et. }
    }
  Qed.
  End TYPE0.

  Section TYPE1.
  Hypothesis MAINM: forall (main_fsp: fspec) (MAIN: stb1 sk "main" = Some main_fsp),
      exists (x: main_fsp.(meta)),
        (<<PRE: Own (entry_r) -∗ main_fsp.(precond) None x initial_arg initial_arg>>) /\
        (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
        (<<RET: forall ret_src ret_tgt,
            (main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ (⌜ret_src = ret_tgt⌝)>>).

  Theorem adequacy_type_closed: refines_closed (Mod.add_list mds_tgt1) (Mod.add_list mds_src).
  Proof.
    ii. eapply adequacy_type_arg_closed; et.
    i. hexploit MAINM; et. i. des. esplits; et.
    { eapply to_semantic.
      { uipropall. }
      { eapply URA.wf_mon; et. }
    }
  Qed.
  End TYPE1.

End CANCEL.

Require Import Weakening.
Require Import ClassicalChoice.

Section CANCEL.

  Context `{Σ: GRA.t}.

  Variable mds: list SMod.t.

  Let sk: Sk.t := SMod.get_sk mds.
  (* Let sk: Sk.t := Sk.sort (fold_right Sk.add Sk.unit (List.map SMod.sk mds)). *)
  (* Let skenv: SkEnv.t := Sk.load_skenv sk. *)

  Let _mss: Sk.t -> list SModSem.t := fun sk => (List.map ((flip SMod.get_modsem) sk) mds).
  Let _sbtb: Sk.t -> list (gname * fspecbody) := fun sk => (List.flat_map (SModSem.fnsems) (_mss sk)).
  Let _stb: Sk.t -> list (gname * fspec) := fun sk => List.map (fun '(fn, fs) => (fn, fs.(fsb_fspec))) (_sbtb sk).

  Let mss: list SModSem.t := _mss sk.
  Let sbtb: list (gname * fspecbody) := _sbtb sk.

  Let stb: gname -> option fspec :=
    fun fn => match alist_find fn (_stb sk) with
              | Some fsp => Some fsp
              | None => Some fspec_trivial
              end.

  Let mds_src: list Mod.t := List.map (SMod.to_src) mds.
  Variable mds_tgt: list Mod.t.

  Hypothesis WEAKEN: Forall2 (fun md md_tgt => exists stb0, (<<WEAK: forall sk, stb_weaker (stb0 sk) stb>>)
                                                            /\ (<<MD: md_tgt = SMod.to_tgt stb0 md>>)) mds mds_tgt.

  Opaque EventsL.interp_Es.

  Let ms_src: ModSemL.t := ModL.enclose (Mod.add_list mds_src).
  Let ms_tgt: ModSemL.t := ModL.enclose (Mod.add_list mds_tgt).

  Let initial_mrs_eq_aux
      sk0
    :
      List.map
        (fun x =>
           (SModSem.mn (SMod.get_modsem x sk0),
            (Any.pair (SModSem.initial_st (SMod.get_modsem x sk0)) (SModSem.initial_mr (SMod.get_modsem x sk0))↑))) mds =
      ModSemL.initial_mrs (ModL.get_modsem (Mod.add_list mds_tgt) sk0)
  .
  Proof.
    clear - WEAKEN.
    eapply Forall2_impl in WEAKEN; cycle 1.
    { instantiate (1:=(fun md md_tgt => exists stb0, (<<MD: md_tgt = SMod.to_tgt stb0 md>>))).
      ii. ss. des. subst. eauto. }
    induction WEAKEN; ss.
    des; subst. ss.
    f_equal; ss.
    eapply IHf.
    inv WEAKEN; ss.
  Qed.

  Lemma sk_eq: fold_right Sk.add Sk.unit (List.map SMod.sk mds) = ModL.sk (Mod.add_list mds_tgt).
  Proof.
    clear - WEAKEN.
    eapply Forall2_impl in WEAKEN; cycle 1.
    { instantiate (1:=(fun md md_tgt => exists stb0, (<<MD: md_tgt = SMod.to_tgt stb0 md>>))).
      ii. ss. des. subst. eauto. }
    induction WEAKEN; ss. des; subst. ss.
    f_equal. erewrite IHf; ss.
  Qed.

  Lemma sk_eq2: fold_right Sk.add Sk.unit (List.map SMod.sk mds) = (ModL.sk (Mod.add_list (List.map (SMod.to_tgt (fun _ => stb)) mds))).
  Proof.
    rewrite sk_eq. clear - WEAKEN.
    eapply Forall2_impl in WEAKEN; cycle 1.
    { instantiate (1:=(fun md md_tgt => exists stb0, (<<MD: md_tgt = SMod.to_tgt stb0 md>>))).
      ii. ss. des. subst. eauto. } des.
    unfold Mod.add_list.
    erewrite fold_right_map with (fi:=ModL.sk) (fs:=ModL.sk) (yadd:=Sk.add); try refl; cycle 1.
    erewrite fold_right_map with (fi:=ModL.sk) (fs:=ModL.sk) (yadd:=Sk.add); try refl; cycle 1.
    f_equal.
    rewrite ! List.map_map.
    eapply Forall2_apply_Forall2 with (Q:=eq) (f:=ModL.sk ∘ (SMod.to_tgt (fun _ => stb))) (g:=(ModL.sk ∘ Mod.lift)) in WEAKEN.
    { eapply Forall2_eq in WEAKEN. des; ss. }
    ii. des. subst. ss.
  Qed.

  Lemma initial_mrs_eq
    :
      List.map
        (fun x =>
           (SModSem.mn (SMod.get_modsem x sk),
            (Any.pair (SModSem.initial_st (SMod.get_modsem x sk))) (SModSem.initial_mr (SMod.get_modsem x sk))↑)) mds =
      ModSemL.initial_mrs (ModL.enclose (Mod.add_list mds_tgt))
  .
  Proof.
    unfold ModL.enclose.
    erewrite initial_mrs_eq_aux. repeat f_equal. unfold sk, SMod.get_sk.
    f_equal. rewrite sk_eq. ss.
  Qed.

  Lemma initial_mrs_eq2
    :
      List.map fst (ModSemL.initial_mrs ms_tgt) =
      List.map fst (ModSemL.initial_mrs (ModL.enclose (Mod.add_list (List.map (SMod.to_tgt (fun _ => stb)) mds))))
  .
  Proof.
    unfold ms_tgt. rewrite <- initial_mrs_eq.
    unfold ModL.enclose. rewrite <- sk_eq2. folder.
    unfold Mod.add_list.
    match goal with
    | [ |- context[ModL.get_modsem ?x ?sk] ] =>
      replace (ModL.get_modsem x sk) with (((flip ModL.get_modsem) sk) x) by refl
    end.
    erewrite fold_right_map with (yadd:=ModSemL.add) (fi:=(flip ModL.get_modsem) sk); cycle 1.
    { refl. }
    erewrite fold_right_map with (yadd:=@List.app _) (fi:=ModSemL.initial_mrs); cycle 1.
    { refl. }
    rewrite ! List.map_map. cbn.
    clear - mds. clearbody sk.
    induction mds; ii; ss. f_equal; ss.
  Qed.

  Context {CONF: EMSConfig}.
  Lemma adequacy_type2 entry_r
        (WFR: URA.wf (entry_r ⋅ SMod.get_initial_mrs mds sk))
        (MAINM:
           forall (main_fsp: fspec) (MAIN: stb "main" = Some main_fsp),
           exists (x: main_fsp.(meta)),
             (<<PRE: Own entry_r -∗ main_fsp.(precond) None x initial_arg initial_arg>>) /\
             (<<MEASURE: main_fsp.(measure) x = ord_top>>) /\
             (<<RET: forall ret_src ret_tgt,
                 (main_fsp.(postcond) None x ret_src ret_tgt: iProp) -∗ (⌜ret_src = ret_tgt⌝)>>))
    :
      refines_closed (Mod.add_list mds_tgt) (Mod.add_list mds_src).
  Proof.
    ii. eapply adequacy_type_arg_stb; ss.
    { instantiate (1:=fun _ => stb). unfold stb. i.
      unfold _stb, _sbtb, _mss, sk. rewrite FIND. auto. }
    { i. unfold stb, _stb, _sbtb, _mss, sk. rewrite FIND.
      right. esplits; et. }
    { i. ss. hexploit MAINM; et. i. des. esplits; et.
      { eapply to_semantic; et.
        eapply URA.wf_mon; et. }
      { r_wf WFR. unfold SMod.get_initial_mrs. rewrite map_map. ss. }
    }
    { revert x0 PR. eapply refines_close. eapply refines2_pairwise.
      rewrite <- (map_id mds_tgt). rewrite <- Forall2_flip.
      eapply Forall2_apply_Forall2; et.
      i. ss. des. subst. eapply adequacy_weaken; et.
    }
  Qed.

End CANCEL.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR


text:
From Coq Require Import
  Lists.List.

From Theories Require Import
  Tactics.

Import ListNotations.
Open Scope list_scope.

Notation List := list.
Notation Opt := option.
Notation some := Some.
Notation none := None.

(** * Specification *)

Inductive Typ := t_void | t_arr (t1 t2 : Typ).
Inductive Exp := e_var (x : nat) | e_app (e1 e2 : Exp) | e_abs (e : Exp).
Inductive Val := v_abs (ve : List Val) (e : Exp).

Definition ValEnv := List Val.
Definition TypEnv := List Typ.

Fixpoint index {X : Type} (n : nat) (xs : List X) : Opt X :=
  match xs with
  | []      => none
  | x :: xs' => if beq_nat n (length xs') then some x else index n xs'
  end.

Inductive ExpTyp : TypEnv -> Exp -> Typ -> Prop :=
  | et_var :
      forall x te t1,
      index x te = some t1 ->
      ExpTyp te (e_var x) t1
  | et_app :
      forall te e1 e2 t1 t2,
      ExpTyp te e1 (t_arr t1 t2) ->
      ExpTyp te e2 t1 ->
      ExpTyp te (e_app e1 e2) t2
  | et_abs :
      forall te e t1 t2,
      ExpTyp (t1 :: te) e t2 ->
      ExpTyp te (e_abs e) (t_arr t1 t2)
  .

Inductive WfEnv : ValEnv -> TypEnv -> Prop :=
  | wfe_nil :
      WfEnv [] []
  | wfe_cons :
      forall v t ve te,
      ValTyp v t ->
      WfEnv ve te ->
      WfEnv (v :: ve) (t :: te)
with ValTyp : Val -> Typ -> Prop :=
  | vt_abs :
      forall ve te e t1 t2,
      WfEnv ve te ->
      ExpTyp (t1 :: te) e t2 ->
      ValTyp (v_abs ve e) (t_arr t1 t2)
  .

(* Note that this notation allows [MonadFail] style patterns for [p]. *)
Notation "' p <- e1 ; e2" :=
  (match e1 with
   | some (some p) => e2
   | some _ => some none
   | none => none
   end)
  (right associativity, at level 60, p pattern).

Fixpoint eval (n : nat) (ve : ValEnv) (e : Exp) : Opt (Opt Val) :=
  match n with
  | 0 => none
  | S n =>
      match e with
      | e_var x => some (index x ve)
      | e_abs e => some (some (v_abs ve e))
      | e_app e1 e2 =>
          ' v_abs ve1' e1' <- eval n ve e1;
          ' v2 <- eval n ve e2;
          eval n (v2 :: ve1') e1'
      end
  end.

(** * Theorems *)

Hint Constructors Typ Exp Val ExpTyp ValTyp WfEnv Opt List.
Hint Unfold index length ValEnv TypEnv.
Hint Resolve ex_intro.

Lemma wve_length :
  forall ve te,
  WfEnv ve te ->
  length ve = length te.
Proof.
  intros ? ? H. induction H.
  Case "wfe_nil". reflexivity.
  Case "wfe_cons". simpl. rewrite IHWfEnv. reflexivity.
Qed.

Hint Immediate wve_length.

Lemma index_max :
  forall X (xs : List X) (n : nat) (x : X),
  index n xs = some x ->
  n < length xs.
Proof.
  intros ? xs. induction xs.
  Case "nil".
    intros ? ? H. simpl in H. inversion H.
  Case "cons".
    intros ? ? H. simpl. case_eq (n =? length xs); intros E.
    Case2 "hit".
      eapply beq_nat_true in E. rewrite <- E. constructor.
    Case2 "miss".
      simpl in H. rewrite E in H. transitivity (length xs).
      - eapply IHxs. apply H.
      - constructor.
Qed.

Lemma index_extend :
  forall X xs n x' (x : X),
  index n xs = some x ->
  index n (x' :: xs) = some x.
Proof.
  intros ? ? ? ? ? H. simpl. rewrite H.
  assert (n < length xs) as H0. { eapply index_max. exact H. }
  assert (n <> length xs) as H1. { omega. }
  assert ((n =? length xs) = false) as H2. { eapply beq_nat_false_iff. exact H1. }
  rewrite H2. reflexivity.
Qed.

Lemma wve_index :
  forall ve te t n,
  WfEnv ve te ->
  index n te = some t ->
  exists v, index n ve = some v /\ ValTyp v t.
Proof.
  intros ? ? ? ? HWf Hindex. induction HWf.
  Case "wfe_nil".
    simpl in Hindex. inversion Hindex.
  Case "wfe_cons".
    simpl in Hindex. case_eq (n =? length te).
    Case2 "index hits head".
      intros Hhit. rewrite Hhit in Hindex. inversion Hindex; subst t0; clear Hindex.
      assert ((n =? length ve) = true) as Hhit'. { eauto using wve_length. }
      assert (index n (v :: ve) = some v). { simpl. rewrite Hhit'. reflexivity. }
      eauto.
    Case2 "index hits tail".
      intros Hmiss. rewrite Hmiss in Hindex.
      assert ((n =? length ve) = false) as Hmiss'. { eauto using wve_length. }
      specialize (IHHWf Hindex). inversion IHHWf as [v0 [H0 H1]].
      exists v0. constructor. { apply index_extend. exact H0. } { exact H1. }
Qed.

Theorem full_safety :
  forall n e te ve res t,
  eval n ve e = some res ->
  ExpTyp te e t ->
  WfEnv ve te ->
  exists v, res = some v /\ ValTyp v t.
Proof.
  intros n. induction n.
  Case "n = 0". intros until 0. intros Heval. inversion Heval.
  Case "n = S n". intros until 0. intros Heval Htype Hwf. destruct e.
    Case2 "var".
      inversion Heval as [Heval']; clear Heval Heval'.
      inversion Htype; subst te0 x t1; rename H1 into Htype'.
      destruct (wve_index _ _ _ _ Hwf Htype') as [v [I V]].
      rewrite I. eexists. split. reflexivity. exact V.
    Case2 "app".
      inversion Htype; subst t2 e0 e3 te0;
        rename H2 into Htype1; rename H4 into Htype2; rename t into t2.
      simpl in Heval.
      remember (eval n ve e1) as mmv1.
      destruct mmv1 as [mv1|].
      Case3 "mmv1 = some mv1".
        (** Apply [IHn] to [e1] *)
        assert (exists v1, mv1 = some v1 /\ ValTyp v1 (t_arr t1 t2)) as [v1 [E1 HVtype1]].
          { eapply IHn; eauto. }
        subst mv1.
        (** Invert [v1] to closure [v_abs ve0 e] with [ExpTyp] evidence. *)
        inversion HVtype1; subst t0 t3. subst v1.
        remember (eval n ve e2) as mmv2.
        destruct mmv2 as [mv2|].
        Case4 "mmv2 = some mv2".
          (** Apply [IHn] to [e2] *)
          assert (exists v2, mv2 = some v2 /\ ValTyp v2 t1) as [v2 [E2 HVtype2]].
            { eapply IHn; eauto. }
          subst mv2.
          (** Apply [IHn] to closure body [e] *)
          eapply IHn; eauto.
        Case4 "mmv2 = none  [contradiction]".
          inversion Heval.
      Case3 "mmv1 = none  [contradiction]".
        inversion Heval.
    Case2 "abs".
      inversion Htype; subst te0 e0. subst t.
      inversion Heval as [Heval']; clear Heval Heval'.
      eexists. split. eauto. eapply vt_abs; eauto.
Qed.

repo: definitional


text:
Require Import ZArith.
From Bremen.theories.harmony Require Import Letter.

Inductive pitchClass : Type :=
  pitch_class : letter -> Z -> pitchClass.

Notation "L # M" := (pitch_class L M) (at level 80, right associativity).

Definition letter (x : pitchClass) : letter :=
  match x with
  | l # m => l
  end.

Definition modifier (x : pitchClass) : Z :=
  match x with
  | l # m => m
  end.

Definition upward_distance (x y : pitchClass) : nat :=
  match x, y with
  | l # m, l' # m' => Z.to_nat (Zmod (Z.of_nat (upward_distance l l') - m + m') 12)
  end.

Definition eqb (x y : pitchClass) : bool :=
  match x, y with
  | (l1 # m1), (l2 # m2) => andb (Letter.eqb l1 l2) (Z.eqb m1 m2)
  end.

Definition enharmonic_eq (x y : pitchClass) : Prop :=
  upward_distance (A # 0) x = upward_distance (A # 0) y.

Notation "X e= Y" := (enharmonic_eq X Y) (at level 80, right associativity).

Definition sharpen (x : pitchClass) : pitchClass :=
  match x with
  | l # m => l # m + 1
  end.

Definition flatten (x : pitchClass) : pitchClass :=
  match x with
  | l # m => l # m - 1
  end.

Definition halfstep_up (x : pitchClass) : pitchClass :=
    match x with | l # m =>
    next l # (m - Z.of_nat(upward_distance (l # 0) (next l # 0)) + 1)
end.

Lemma same_letter_same_pitch_class : forall (l1 l2 : Letter.letter) (m : Z), l1 = l2 -> (l1 # m) = (l2 # m).
Proof. intros l1 l2 m. intro H. rewrite -> H. reflexivity.
Qed.

Lemma different_pitch_classes : forall (l1 l2 : Letter.letter) (m1 m2 : Z),
  eqb (l1 # m1) (l2 # m2) = false <->
  orb (Bool.eqb (Letter.eqb l1 l2) false) (Bool.eqb (Z.eqb m1 m2) false) = true.
Proof.
intros. split.
  * unfold eqb. unfold Bool.eqb. unfold andb. unfold orb. destruct (Letter.eqb l1 l2) eqn:eqL1L2.
  ** destruct (Z.eqb m1 m2). auto. auto.
  ** auto.
  * destruct (Letter.eqb l1 l2) eqn:eqL1L2.
  ** destruct (Z.eqb m1 m2) eqn:eqM1M2.
  *** simpl. rewrite -> eqL1L2. rewrite -> eqM1M2. auto.
  *** simpl. rewrite -> eqL1L2. rewrite -> eqM1M2. auto.
  ** destruct (Z.eqb m1 m2) eqn:eqM1M2.
  *** simpl. rewrite -> eqM1M2. rewrite -> eqL1L2. auto.
  *** simpl. rewrite -> eqM1M2. rewrite -> eqL1L2. auto.
Qed.

Lemma pitchclass16 : forall (l1 l2 : Letter.letter) (m1 m2 : Z),
  upward_distance (l1 # m1) (l2 # m1) = upward_distance (l1 # m2) (l2 # m2).
Proof. Admitted.

Lemma upward_distance_12 : forall (x y : pitchClass),
  eqb x y = false <->
  Nat.eqb (upward_distance x y) (12 - (upward_distance y x)) = true.
Proof. Admitted.

Lemma upward_distance_modifier : forall (l1 l2 : Letter.letter) (m1 m2 : Z),
  upward_distance (l1 # m1) (l2 # m1) = upward_distance (l1 # m2) (l2 # m2).
Proof. Admitted.

(* A flatten és a sharpen kapcsolatára vonatkozó állítások *)
Lemma flatten_sharpen_1 : forall (x : pitchClass), flatten (sharpen x) = x.
Proof. Admitted.

Lemma flatten_sharpen_2 : forall (x y : pitchClass), sharpen x = y -> flatten y = x.
Proof. Admitted.

Lemma upward_distance_sharpen : forall (x y : pitchClass), upward_distance x y + 1 = upward_distance x (sharpen y).
Proof. Admitted.

author: fajtaiandris

repo: bremen

save_path: github-repos/coq/fajtaiandris-bremen


text:
Require Import VST.floyd.proofauto.
Require Import VST.progs.float.

Instance CompSpecs : compspecs.
Proof. make_compspecs prog. Defined.

Local Open Scope logic.

Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog nil gv
  POST [ tint ] main_post prog nil gv.

Definition t_struct_foo := Tstruct _foo noattr.

Definition Vprog : varspecs := (_s, t_struct_foo)::nil.

Definition Gprog : funspecs :=   ltac:(with_library prog [main_spec]).

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
name x1 _x1.
name y1 _y1.
name y2 _y2.
name s _s.
start_function.
pose (f :=  PROP () LOCAL (gvars gv)
  SEP (data_at Ews t_struct_foo (Vint (Int.repr 5),
          (Vsingle (Float32.of_bits (Int.repr 1079655793)),
           Vfloat (Float.of_bits (Int64.repr 0)))) (gv _s))).
apply semax_pre with f; subst f. (* factored out "f" to work around a bug
   in Coq 8.4pl6 (and earlier versions back at least to 8.4pl3).
  To exhibit the bug, put the r.h.s. of the "pose" as in place of f
  in the "apply...with".  *)
 {
unfold data_at.
 unfold_field_at (field_at _ t_struct_foo _ _ _).
entailer!.
simpl.
unfold field_at, data_at_rec, at_offset. simpl.
  repeat (rewrite prop_true_andp by (auto with field_compatible)).
fold noattr; fold tint; fold tfloat; fold tdouble.
repeat match goal with |- context [field_offset ?A ?B ?C] =>
  set (aa :=field_offset A B C); compute in aa; subst aa
end.
normalize. cancel.
}
forward.
forward.
forward.
forward.
forward.
forward.
forward.
Qed.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
From iris.algebra Require Import auth frac agree gmap list excl.
From Perennial.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From Perennial.program_logic Require Export language.
From Perennial.program_logic Require Import lifting.
From Perennial.program_logic Require Export crash_lang ncinv staged_invariant.

Set Default Proof Using "Type".

(*

   Encoding of an abstract source program as a ghost resource, in order to use
   Iris to prove refinements. This encoding is based on that of the one used in
   iris-examples/theories/logrel/rules_binary.v for the logical relations proofs
   by Timany et al.

*)

Section ghost.
Context {Λ: language}.
Context {CS: crash_semantics Λ}.

(** The CMRA for the heap of the specification. *)
Definition tpoolUR : ucmra := gmapUR nat (exclR (exprO Λ)).
Definition stateUR := optionUR (exclR (prodO (stateO Λ) (global_stateO Λ))).
Definition cfgUR := prodUR tpoolUR stateUR.

Class cfgPreG (Σ : gFunctors) :=
  { cfg_preG_inG :> inG Σ (authR cfgUR) ;
    cfg_preG_stagedG :> stagedG Σ}.
Class cfgG Σ := { cfg_inG :> cfgPreG Σ;
                  cfg_name : gname }.

Definition cfgΣ : gFunctors :=
  #[GFunctor (authR cfgUR); stagedΣ].

Instance subG_cfgG {Σ} : subG cfgΣ Σ → cfgPreG Σ.
Proof. solve_inG. Qed.

Fixpoint tpool_to_map_aux (tp: list (language.expr Λ)) (id: nat) : gmap nat (language.expr Λ) :=
  match tp with
  | [] => ∅
  | e :: tp' => <[id := e]>(tpool_to_map_aux tp' (S id))
  end.

Definition tpool_to_map tp := tpool_to_map_aux tp O.
Definition tpool_to_res tp := (Excl <$> (tpool_to_map tp) : tpoolUR).

Definition sN := nroot .@ "source".
Definition sN_inv := sN.@ "base".

Section ghost_spec.
  Context `{cfgG Σ, crashGS Σ, invGS Σ}.

  Definition tpool_mapsto (j: nat) (e: language.expr Λ) : iProp Σ :=
    own cfg_name (◯ ({[ j := Excl e]}, ε)).

  (* ownership of this does not mean there aren't other threads not in (fst ρ) *)
  Definition source_cfg (ρ: (list (language.expr Λ)) * (language.state Λ * language.global_state Λ)) : iProp Σ :=
    own cfg_name (◯ (tpool_to_res (fst ρ), Some (Excl (snd ρ)))).

  Definition source_state (σ: language.state Λ) (g: language.global_state Λ) : iProp Σ :=
    own cfg_name (◯ (∅ : tpoolUR, Some (Excl (σ, g)))).

  Definition source_pool_map (tp: gmap nat (language.expr Λ)) : iProp Σ :=
    own cfg_name (◯ (Excl <$> tp : tpoolUR, ε)).

  Definition source_inv r tp σ g : iProp Σ :=
    (∃ s tp' σ' g', own cfg_name (● (tpool_to_res tp', Some (Excl (σ', g')))) ∗
                   ⌜ erased_rsteps (CS := CS) r (tp, (σ, g)) (tp', (σ', g')) s
                     ∧ crash_safe (CS := CS) r (tp, (σ, g)) ⌝)%I.

  Definition source_ctx' r (ρ : cfg Λ) : iProp Σ :=
    ncinv sN_inv (source_inv r (fst ρ) (ρ.2.1) (ρ.2.2)).

  Definition source_ctx : iProp Σ :=
    (∃ r ρ, source_ctx' r ρ)%I.

  Definition source_crash_ctx' r (ρ : cfg Λ) P : iProp Σ :=
    □ (|C={↑sN_inv}=> inv sN_inv (P ∨ source_inv r (fst ρ) (ρ.2.1) (ρ.2.2))).

  Definition source_crash_ctx P : iProp Σ :=
    (∃ r ρ, source_crash_ctx' r ρ P)%I.

  Global Instance tpool_mapsto_timeless j e : Timeless (tpool_mapsto j e).
  Proof. apply _. Qed.
  Global Instance source_state_timeless σ g : Timeless (source_state σ g).
  Proof. apply _. Qed.
  Global Instance source_ctx'_persistent r ρ : Persistent (source_ctx' r ρ).
  Proof. apply _. Qed.
  Global Instance source_ctx_persistent : Persistent (source_ctx).
  Proof. apply _. Qed.
  Global Instance source_crash_ctx'_persistent r ρ P : Persistent (source_crash_ctx' r ρ P).
  Proof. apply _. Qed.
  Global Instance source_crash_ctx_persistent P : Persistent (source_crash_ctx P).
  Proof. apply _. Qed.

End ghost_spec.

Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : bi_scope.

Section ghost_step.
  Context `{invGS Σ, crashGS Σ, stagedG Σ}.
  Implicit Types (σ : state Λ) (g : global_state Λ).

  Lemma tpool_to_map_lookup_aux tp id j e:
    tpool_to_map_aux tp id !! (id + j) = Some e ↔ tp !! j = Some e.
  Proof.
    revert id j; induction tp => id j //=.
    destruct j.
    * rewrite //= Nat.add_0_r lookup_insert //=.
    * rewrite //= lookup_insert_ne //=; last by lia.
      replace (id + S j) with (S id + j) by lia; eauto.
  Qed.

  Lemma tpool_to_map_lookup_aux_none tp id j:
    tpool_to_map_aux tp id !! (id + j) = None ↔ tp !! j = None.
  Proof.
    revert id j; induction tp => id j //=.
    destruct j.
    * rewrite //= Nat.add_0_r lookup_insert //=.
    * rewrite //= lookup_insert_ne //=; last by lia.
      replace (id + S j) with (S id + j) by lia; eauto.
  Qed.

  Lemma tpool_to_map_lookup tp j e:
    tpool_to_map tp !! j = Some e ↔ tp !! j = Some e.
  Proof.
    rewrite /tpool_to_map. pose (tpool_to_map_lookup_aux tp 0 j e) => //=.
  Qed.

  Lemma tpool_to_map_lookup_none tp j:
    tpool_to_map tp !! j = None ↔ tp !! j = None.
  Proof.
    rewrite /tpool_to_map. pose (tpool_to_map_lookup_aux_none tp 0 j) => //=.
  Qed.

  Lemma tpool_to_res_lookup tp j e:
    tpool_to_res tp !! j = Some (Excl e) ↔ tp !! j = Some e.
  Proof.
    rewrite /tpool_to_res lookup_fmap. generalize (tpool_to_map_lookup tp j e) => Hconv.
    split.
    - destruct (tpool_to_map tp !! j); inversion 1; subst; eapply Hconv; eauto.
    - intros. rewrite (proj2 Hconv); eauto.
  Qed.

  Lemma tpool_to_res_lookup_none tp j:
    tpool_to_res tp !! j = None ↔ tp !! j = None.
  Proof.
    rewrite /tpool_to_res lookup_fmap. generalize (tpool_to_map_lookup_none tp j) => Hconv.
    split.
    -destruct (tpool_to_map tp !! j); inversion 1; subst; eapply Hconv; eauto.
    - intros. rewrite (proj2 Hconv); eauto.
  Qed.

  Lemma tpool_to_res_lookup_excl tp j x:
    tpool_to_res tp !! j = Some x → ∃ e, x = Excl e.
  Proof.
    rewrite /tpool_to_res/tpool_to_map. generalize 0. induction tp => n //=.
    destruct (decide (j = n)); subst.
    * rewrite lookup_fmap //= lookup_insert. inversion 1; setoid_subst; by eexists.
    * rewrite lookup_fmap //= lookup_insert_ne //= -lookup_fmap; eauto.
  Qed.

  Lemma tpool_to_res_insert_update tp j e :
    j < length tp →
    tpool_to_res (<[j := e]> tp) = <[j := Excl e]> (tpool_to_res tp).
  Proof.
    intros Hlt. apply: map_eq; intros i.
    destruct (decide (i = j)); subst.
    - rewrite lookup_insert tpool_to_res_lookup list_lookup_insert //=.
    - rewrite lookup_insert_ne //=.
      destruct (decide (i < length tp)) as [Hl|Hnl].
      * efeed pose proof (lookup_lt_is_Some_2 tp) as His; first eassumption.
        destruct His as (e'&His).
        rewrite (proj2 (tpool_to_res_lookup tp i e')) //=.
        apply tpool_to_res_lookup. rewrite list_lookup_insert_ne //=.
      * efeed pose proof (lookup_ge_None_2 tp i) as Hnone; first lia.
        rewrite (proj2 (tpool_to_res_lookup_none tp i)) //=.
        apply tpool_to_res_lookup_none. rewrite list_lookup_insert_ne //=.
  Qed.

  Lemma tpool_to_res_insert_snoc tp e :
    tpool_to_res (tp ++ [e]) = <[length tp := Excl e]> (tpool_to_res tp).
  Proof.
    apply: map_eq; intros i.
    destruct (decide (i = length tp)); subst.
    - rewrite lookup_insert tpool_to_res_lookup.
      rewrite lookup_app_r //= Nat.sub_diag //=.
    - rewrite lookup_insert_ne //=.
      destruct (decide (i < length tp)) as [Hl|Hnl].
      * efeed pose proof (lookup_lt_is_Some_2 tp) as His; first eassumption.
        destruct His as (e'&His).
        rewrite (proj2 (tpool_to_res_lookup tp i e')) //=.
        apply tpool_to_res_lookup. rewrite lookup_app_l //=.
      * efeed pose proof (lookup_ge_None_2 tp i) as Hnone; first lia.
        rewrite (proj2 (tpool_to_res_lookup_none tp i)) //=.
        apply tpool_to_res_lookup_none. rewrite lookup_ge_None_2 //= app_length //=; lia.
  Qed.

  Lemma tpool_to_res_length tp j e :
    tpool_to_res tp !! j = Some e → j < length tp.
  Proof.
    intros Hlookup. destruct (decide (j < length tp)) as [Hl|Hnl]; auto.
    rewrite (proj2 (tpool_to_res_lookup_none tp j)) in Hlookup; first by congruence.
    apply lookup_ge_None_2; lia.
  Qed.

  Lemma tpool_singleton_included1 tp j e :
    {[j := Excl e]} ≼ tpool_to_res tp → tpool_to_res tp !! j = Some (Excl e).
  Proof.
    intros (x&Hlookup&Hexcl)%singleton_included_l.
    destruct (tpool_to_res_lookup_excl tp j x) as (e'&Heq); setoid_subst; eauto.
    apply Excl_included in Hexcl; setoid_subst; auto.
  Qed.

  Lemma tpool_singleton_included2 tp j e :
    {[j := Excl e]} ≼ tpool_to_res tp → tp !! j = Some e.
  Proof.
    intros Hlookup%tpool_singleton_included1.
    apply tpool_to_res_lookup; rewrite Hlookup; eauto.
  Qed.

  Lemma tpool_map_included1 tp1 tp2 :
    Excl <$> tp1 ≼ tpool_to_res tp2 → (∀ j e, tp1 !! j = Some e → tp2 !! j = Some e).
  Proof.
    rewrite lookup_included => Hincl j e Hin.
    specialize (Hincl j). apply tpool_to_res_lookup.
    rewrite (lookup_fmap _ tp1 j) Hin //= in Hincl.
    destruct (tpool_to_res tp2 !! j) as [x|] eqn: Heq; rewrite Heq in Hincl.
    {
      destruct (tpool_to_res_lookup_excl tp2 j x) as (e'&Heq'); setoid_subst; eauto.
      apply Excl_included in Hincl; setoid_subst; eauto.
    }
    apply option_included in Hincl as [Hfalse|(?&?&?&?&?)]; congruence.
  Qed.

  Lemma tpool_to_res_lookup_case tp j:
    (tpool_to_res tp !! j = None) ∨ (∃ e, tpool_to_res tp !! j = Excl' e).
  Proof.
    rewrite /tpool_to_res.
    destruct (tpool_to_map tp !! j) as [p|] eqn:Heq; rewrite lookup_fmap Heq //=.
    * by (right; exists p).
    * by left.
  Qed.

  Lemma source_cfg_init_names1 `{cfgPreG Σ} r tp0 σ0 g0 tp σ g P s:
    erased_rsteps (CS := CS) r (tp0, (σ0, g0)) (tp, (σ, g)) s →
    crash_safe (CS := CS) r (tp0, (σ0, g0)) →
    ⊢ |={⊤}=> ∃ γ, let _ : cfgG Σ := {| cfg_name := γ |} in
                            source_ctx' r (tp0, (σ0, g0)) ∗
                            source_pool_map (tpool_to_map tp) ∗
                            source_state σ g ∗
                            source_crash_ctx' r (tp0, (σ0, g0)) P.
  Proof using H1.
    intros Herased Hno_err.
    iMod (own_alloc (● (tpool_to_res tp, Some (Excl (σ,g)))
                       ⋅ ◯ (tpool_to_res tp, Some (Excl (σ,g))))) as (γ) "(Hauth&Hfrag)".
    { apply @auth_both_valid_discrete; first by apply _. split; [| split].
      { reflexivity. }
      - rewrite //=. intros i.
        destruct (tpool_to_res_lookup_case tp i) as [Heq_none|(e&Heq_some)].
        * rewrite Heq_none; econstructor.
        * rewrite Heq_some; econstructor.
      - rewrite //=.
    }
    set (IN := {| cfg_name := γ |}).
    iExists γ.
    iMod (ncinv_cinv_alloc sN_inv ⊤ (↑sN_inv) (source_inv r tp0 σ0 g0) (P ∨ source_inv r tp0 σ0 g0)%I True%I
            with "[] [Hauth]") as "(#Hinv&_&#Hcfupd)".
    { set_solver. }
    { iModIntro. iIntros ">H _". iModIntro; eauto. }
    { rewrite /source_inv. iNext. iExists s, tp, σ, g. iFrame "Hauth".
      iPureIntro; split; eauto. }
    iModIntro. iFrame.
    rewrite pair_split.
    iDestruct "Hfrag" as "($&$)". iFrame "Hinv".
    iModIntro.
    iMod (cfupd_weaken_mask with "[Hcfupd]") as "H"; eauto.
  Qed.

  Lemma source_cfg_init_names2 `{cfgPreG Σ} r tp σ g P :
    crash_safe (CS := CS) r (tp, (σ, g)) →
    ⊢ |={⊤}=> ∃ γ, let _ : cfgG Σ := {| cfg_name := γ |} in
                            source_ctx' r (tp, (σ, g)) ∗
                            source_pool_map (tpool_to_map tp) ∗
                            source_state σ g ∗
                            source_crash_ctx' r (tp, (σ, g)) P.
  Proof using H1.
    intros Hno_err.
    iApply source_cfg_init_names1; eauto.
    { econstructor. econstructor. }
  Qed.

  Lemma source_cfg_init1 `{cfgPreG Σ} r tp0 σ0 g0 tp σ g P s:
    erased_rsteps (CS := CS) r (tp0, (σ0, g0)) (tp, (σ, g)) s →
    crash_safe (CS := CS) r (tp0, (σ0, g0)) →
    ⊢ |={⊤}=> ∃ _ : cfgG Σ, source_ctx' r (tp0, (σ0, g0)) ∗
                            source_pool_map (tpool_to_map tp) ∗
                            source_state σ g ∗
                            source_crash_ctx' r (tp0, (σ0, g0)) P.
  Proof using H1.
    iIntros. iMod (source_cfg_init_names1) as (?) "H"; eauto.
  Qed.

  Lemma source_cfg_init2 `{cfgPreG Σ} r tp σ g P :
    crash_safe (CS := CS) r (tp, (σ, g)) →
    ⊢ |={⊤}=> ∃ _ : cfgG Σ, source_ctx' r (tp, (σ, g)) ∗
                            source_pool_map (tpool_to_map tp) ∗
                            source_state σ g ∗
                            source_crash_ctx' r (tp, (σ, g)) P.
  Proof using H1.
    intros Hno_err.
    iApply source_cfg_init1; eauto.
    { econstructor. econstructor. }
  Qed.

  Context `{cfgG Σ}.
  Context `{Hstate_inhabited: Inhabited (state Λ)}.
  Context `{Hgstate_inhabited: Inhabited (global_state Λ)}.

  Set Default Proof Using "Hstate_inhabited Hgstate_inhabited".

  Lemma source_pool_singleton e:
    source_pool_map (tpool_to_map [e]) -∗ 0 ⤇ e.
  Proof.
    rewrite /source_pool_map/tpool_to_map/tpool_to_map_aux/tpool_mapsto.
    by rewrite fmap_insert fmap_empty insert_empty.
  Qed.

  Lemma source_thread_update e' tp j e σ g :
    j ⤇ e -∗ own cfg_name (● (tpool_to_res tp, Excl' (σ, g)))
      ==∗ j ⤇ e' ∗ own cfg_name (● (tpool_to_res (<[j := e']>tp), Excl' (σ, g))).
  Proof.
    iIntros "Hj Hauth".
    iDestruct (own_valid_2 with "Hauth Hj") as %Hval_pool.
    apply auth_both_valid_discrete in Hval_pool as ((Hpool&_)%prod_included&Hval').
    apply tpool_singleton_included1 in Hpool.
    iMod (own_update_2 with "Hauth Hj") as "[Hauth Hj]".
    {
      eapply auth_update, prod_local_update_1.
      eapply singleton_local_update,
      (exclusive_local_update _ (Excl e')); eauto.
      { econstructor. }
    }
    iFrame.
    rewrite tpool_to_res_insert_update //; last first.
    { eapply tpool_to_res_length; eauto. }
  Qed.

  Lemma source_threads_fork efs tp σ g :
    own cfg_name (● (tpool_to_res tp, Excl' (σ, g)))
      ==∗ ([∗ list] ef ∈ efs, ∃ j', j' ⤇ ef)
        ∗ own cfg_name (● (tpool_to_res (tp ++ efs), Excl' (σ, g))).
  Proof.
    iInduction efs as [| ef efs] "IH" forall (tp).
    - rewrite /= app_nil_r /=; auto.
    - iIntros "Hown".
      iMod (own_update with "Hown") as "[Hown Hj']".
      eapply auth_update_alloc, prod_local_update_1.
      eapply (alloc_local_update (tpool_to_res tp) _ (length tp) (Excl ef)).
      { apply tpool_to_res_lookup_none, lookup_ge_None_2. reflexivity. }
      { econstructor. }
      iEval (rewrite insert_empty) in "Hj'".
      rewrite //= -assoc.
      iSplitL "Hj'".
      { iExists (length tp); iModIntro; eauto. }
      replace (ef :: efs) with ([ef] ++ efs) by auto.
      rewrite assoc. iApply "IH".
      rewrite tpool_to_res_insert_snoc; eauto.
  Qed.

  Lemma source_state_update σ' g' tp σ1 g1 σ2 g2 :
    source_state σ1 g1 -∗ own cfg_name (● (tpool_to_res tp, Excl' (σ2, g2)))
      ==∗ source_state σ' g' ∗ own cfg_name (● (tpool_to_res tp, Excl' (σ', g'))).
  Proof.
    iIntros "Hstate Hauth".
    iDestruct (own_valid_2 with "Hauth Hstate") as %Hval_state.
    apply auth_both_valid_discrete in Hval_state as ((_&Hstate)%prod_included&Hval').
    apply Excl_included in Hstate; setoid_subst.
    iMod (own_update_2 with "Hauth Hstate") as "[Hauth Hstate]".
    {
      eapply auth_update, prod_local_update_2.
      apply option_local_update, (exclusive_local_update _ (Excl (σ', g'))); econstructor.
    }
    by iFrame.
  Qed.

  Lemma source_thread_reconcile tp j e x:
    j ⤇ e -∗ own cfg_name (● (tpool_to_res tp, x)) -∗ ⌜ tp !! j = Some e ⌝.
  Proof.
    iIntros "Hj Hauth".
    iDestruct (own_valid_2 with "Hauth Hj") as %Hval_pool.
    apply auth_both_valid_discrete in Hval_pool as ((Hpool&_)%prod_included&Hval').
    apply tpool_singleton_included1, tpool_to_res_lookup in Hpool; eauto.
  Qed.

  Lemma source_pool_map_reconcile tp1 tp2 x:
    source_pool_map tp1 -∗ own cfg_name (● (tpool_to_res tp2, x)) -∗
                    ⌜ ∀ i e, tp1 !! i = Some e → tp2 !! i = Some e ⌝.
  Proof.
    iIntros "Hj Hauth".
    iDestruct (own_valid_2 with "Hauth Hj") as %Hval_pool.
    apply auth_both_valid_discrete in Hval_pool as ((Hpool&_)%prod_included&Hval').
    iPureIntro. eapply tpool_map_included1; eauto.
  Qed.

  Lemma source_state_reconcile σ g σ' g' x:
    source_state σ g -∗ own cfg_name (● (x, Excl' (σ', g'))) -∗ ⌜ σ = σ' ∧ g = g' ⌝.
  Proof.
    iIntros "Hstate Hauth".
    iDestruct (own_valid_2 with "Hauth Hstate") as %Hval_state.
    apply auth_both_valid_discrete in Hval_state as ((_&Hstate)%prod_included&_).
    apply Excl_included in Hstate; setoid_subst; auto.
  Qed.

  Lemma ghost_step_lifting' E r ρ j K `{LanguageCtx Λ K} e1 σ1 g1 κ σ2 g2 e2 efs:
    language.prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
    nclose sN_inv ⊆ E →
    source_ctx' r ρ ∗ j ⤇ K e1 ∗ source_state σ1 g1
      -∗ |NC={E}=> j ⤇ K e2 ∗ source_state σ2 g2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ ef.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (Hstep ?) "(#Hctx&Hj&Hstate)". rewrite /source_ctx/source_inv.
    iInv "Hctx" as (s' tp' σ' g') ">[Hauth %]" "Hclose".

    (* Reconcile view based on authoritative element *)
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    iDestruct (source_state_reconcile with "Hstate Hauth") as %Heq_state.
    setoid_subst.

    (* Update authoritative resources to simulate step *)
    iMod (source_thread_update (K e2) with "Hj Hauth") as "[Hj Hauth]".
    iMod (source_threads_fork efs with "Hauth") as "[Hj' Hauth]".
    iMod (source_state_update σ2 with "Hstate Hauth") as "[Hstate Hauth]".

    (* Restore the invariant *)
    iMod ("Hclose" with "[Hauth]").
    { iNext. iExists s', (<[j := K e2]>tp' ++ efs), σ2, g2.
      iFrame. intuition. iPureIntro; split; auto.
      eapply erased_rsteps_r_1; eauto.
      eapply fill_step in Hstep.
      econstructor. econstructor; eauto.
      - subst. f_equal. symmetry. eapply take_drop_middle; eauto.
      - f_equal. rewrite app_comm_cons assoc; f_equal.
        erewrite <-take_drop_middle at 1; f_equal.
        { apply take_insert; reflexivity. }
        { f_equal. apply drop_insert_gt; lia. }
        rewrite list_lookup_insert //=.
        apply lookup_lt_is_Some_1; eauto.
      }
    iModIntro; iFrame.
  Qed.

  Lemma ghost_step_crash_stuck' E P Q j K `{LanguageCtx Λ K} e σ g:
    nclose sN_inv ⊆ E →
    □ (Q ∗ ▷ P -∗ |={∅}=> False) -∗
    source_crash_ctx P -∗ Q -∗ j ⤇ K e -∗ source_state σ g -∗ C -∗ |={E}=>
    ⌜ ¬ stuck e σ g ⌝ ∗ j ⤇ K e ∗ source_state σ g ∗ Q.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (?) "#Hwand #Hctx HQ Hj Hstate ". rewrite /source_ctx/source_inv.
    iDestruct "Hctx" as (??) "Hctx".
    iMod (cfupd_weaken_mask with "Hctx") as "#Hinv"; eauto.
    iIntros "HC".
    iInv "Hinv" as "[HP|Hrest]" "Hclose".
    { iMod (fupd_mask_subseteq ∅); first by solve_ndisj.
      iMod ("Hwand" with "[$]") as %[]. }
    iDestruct "Hrest" as (? tp' σ' g') ">[Hauth Hpure]".
    iDestruct "Hpure" as %(Hstep&Hnoerr).
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    iDestruct (source_state_reconcile with "Hstate Hauth") as %[Heq_σ Heq_g].
    subst.
    assert (¬ stuck e σ' g').
    {
      intros Hstuck.
      assert (stuck (K e) σ' g') as Hstuck'.
      { destruct Hstuck as (?&?). split.
        - apply fill_not_val; auto.
        - apply irreducible_fill; auto.
      }
      rewrite /crash_safe in Hnoerr.
      eapply not_not_stuck in Hstuck'.
      eapply Hstuck', Hnoerr; eauto.
        by eapply elem_of_list_lookup_2.
    }
    iFrame.
    iMod ("Hclose" with "[-]").
    { iNext. iRight. iExists _, _, _, _. iFrame. eauto. }
    eauto.
  Qed.

  Lemma ghost_step_crash_lifting' E P Q r ρ j K `{LanguageCtx Λ K} e1 σ1 g1 κ σ2 g2 e2 efs:
    language.prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
    nclose sN_inv ⊆ E →
    □ (Q ∗ ▷ P -∗ |={∅}=> False) -∗
    source_crash_ctx' r ρ P ∗ Q ∗ j ⤇ K e1 ∗ source_state σ1 g1
      -∗ C -∗ |={E}=> Q ∗ j ⤇ K e2 ∗ source_state σ2 g2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ ef.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (Hstep ?) "#Hwand (#Hctx&HQ&Hj&Hstate)". rewrite /source_ctx/source_inv.
    iMod (cfupd_weaken_mask with "Hctx") as "#Hinv"; eauto.
    iIntros "HC".
    iInv "Hinv" as "[HP|Hrest]" "Hclose".
    { iMod (fupd_mask_subseteq ∅); first by solve_ndisj.
      iMod ("Hwand" with "[$]") as %[]. }
    iDestruct "Hrest" as (s' tp' σ' g') ">[Hauth %]".

    (* Reconcile view based on authoritative element *)
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    iDestruct (source_state_reconcile with "Hstate Hauth") as %Heq_state.
    setoid_subst.

    (* Update authoritative resources to simulate step *)
    iMod (source_thread_update (K e2) with "Hj Hauth") as "[Hj Hauth]".
    iMod (source_threads_fork efs with "Hauth") as "[Hj' Hauth]".
    iMod (source_state_update σ2 with "Hstate Hauth") as "[Hstate Hauth]".

    (* Restore the invariant *)
    iMod ("Hclose" with "[Hauth]").
    { iNext. iRight. iExists s', (<[j := K e2]>tp' ++ efs), σ2, g2.
      iFrame. intuition. iPureIntro; split; auto.
      eapply erased_rsteps_r_1; eauto.
      eapply fill_step in Hstep.
      econstructor. econstructor; eauto.
      - subst. f_equal. symmetry. eapply take_drop_middle; eauto.
      - f_equal. rewrite app_comm_cons assoc; f_equal.
        erewrite <-take_drop_middle at 1; f_equal.
        { apply take_insert; reflexivity. }
        { f_equal. apply drop_insert_gt; lia. }
        rewrite list_lookup_insert //=.
        apply lookup_lt_is_Some_1; eauto.
      }
    iModIntro; iFrame.
  Qed.

  (* Curried form is more useful, I think *)
  Lemma ghost_step_lifting E j K `{LanguageCtx Λ K} e1 σ1 g1 κ σ2 g2 e2 efs:
    language.prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
    nclose sN_inv ⊆ E →
    j ⤇ K e1 -∗ source_ctx -∗ source_state σ1 g1
      -∗ |NC={E}=> j ⤇ K e2 ∗ source_state σ2 g2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ ef.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (??) "Hj Hsrc ?".
    iDestruct "Hsrc" as (??) "Hsrc".
    iApply ghost_step_lifting'; eauto. iFrame.
  Qed.

  Lemma ghost_step_crash_lifting E P Q j K `{LanguageCtx Λ K} e1 σ1 g1 κ σ2 g2 e2 efs:
    language.prim_step e1 σ1 g1 κ e2 σ2 g2 efs →
    nclose sN_inv ⊆ E →
    □ (Q ∗ ▷ P -∗ |={∅}=> False) -∗
    Q -∗
    j ⤇ K e1 -∗ source_crash_ctx P -∗ source_state σ1 g1
      -∗ C -∗ |={E}=> Q ∗ j ⤇ K e2 ∗ source_state σ2 g2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ ef.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (??) "#Hwand HQ Hj Hsrc ?".
    iDestruct "Hsrc" as (??) "Hsrc".
    iApply ghost_step_crash_lifting'; eauto. iFrame.
  Qed.

  Lemma ghost_step_stuck' E j K `{LanguageCtx Λ K} e σ g:
    nclose sN_inv ⊆ E →
    j ⤇ K e -∗ source_ctx -∗ source_state σ g -∗ |NC={E}=>
    ⌜ ¬ stuck e σ g ⌝ ∗ j ⤇ K e ∗ source_state σ g.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (?) "Hj Hctx Hstate".
    rewrite /source_ctx/source_inv.
    iDestruct "Hctx" as (? ρ) "#Hctx".
    iInv "Hctx" as (? tp' σ' g') ">[Hauth Hpure]" "Hclose".
    iDestruct "Hpure" as %(Hstep&Hnoerr).
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    iDestruct (source_state_reconcile with "Hstate Hauth") as %[Heq_σ Heq_g].
    subst.
    assert (¬ stuck e σ' g').
    {
      intros Hstuck.
      assert (stuck (K e) σ' g') as Hstuck'.
      { destruct Hstuck as (?&?). split.
        - apply fill_not_val; auto.
        - apply irreducible_fill; auto.
      }
      rewrite /crash_safe in Hnoerr.
      eapply not_not_stuck in Hstuck'.
      eapply Hstuck', Hnoerr; eauto.
        by eapply elem_of_list_lookup_2.
    }
    iFrame.
    iMod ("Hclose" with "[-]").
    { iNext. iExists _, _, _, _. iFrame. eauto. }
    eauto.
  Qed.

  Lemma ghost_step_stuck E j K `{LanguageCtx Λ K} e σ g:
    stuck e σ g →
    nclose sN_inv ⊆ E →
    j ⤇ K e -∗ source_ctx -∗ source_state σ g -∗ |NC={E}=> False.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (Hstuck ?) "Hj Hctx Hstate".
    iMod (ghost_step_stuck' with "[$] [$] [$]") as (Hnotstuck) "_"; auto.
  Qed.

  Lemma ghost_step_stuck_det E j K `{LanguageCtx Λ K} e:
    (∀ σ g, stuck e σ g) →
    nclose sN_inv ⊆ E →
    j ⤇ K e -∗ source_ctx -∗ |NC={E}=> False.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (Hstuck ?) "Hj Hctx".
    assert (∀ σ g, stuck (K e) σ g) as Hstuck'.
    { intros σ g. edestruct Hstuck as (?&?). split.
      - apply fill_not_val; auto.
      - apply irreducible_fill; eauto.
    }
    clear Hstuck.
    rewrite /source_ctx/source_inv.
    iDestruct "Hctx" as (? ρ) "#Hctx".
    iInv "Hctx" as (? tp' σ' g') ">[Hauth Hpure]" "Hclose".
    iDestruct "Hpure" as %(Hstep&Hnoerr).
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    subst.
    exfalso. rewrite /crash_safe in Hnoerr.
    eapply not_not_stuck in Hstuck'.
    eapply Hstuck', Hnoerr; eauto.
    by eapply elem_of_list_lookup_2.
  Qed.

  Lemma ghost_step_lifting_puredet E j K `{LanguageCtx Λ K} e1 e2 efs:
    (∀ σ1 g1, ∃ κ, language.prim_step e1 σ1 g1 κ e2 σ1 g1 efs) →
    nclose sN_inv ⊆ E →
    source_ctx ∗ j ⤇ K e1
      -∗ |NC={E}=> j ⤇ K e2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ ef.
  Proof using Type Hgstate_inhabited Hstate_inhabited.
    iIntros (Hstep ?) "(#Hctx&Hj)". iDestruct "Hctx" as (??) "Hctx". rewrite /source_ctx/source_inv.
    iInv "Hctx" as (? tp' σ' g') ">[Hauth %]" "Hclose".

    (* Reconcile view based on authoritative element *)
    iDestruct (source_thread_reconcile with "Hj Hauth") as %Heq_thread.
    setoid_subst.

    (* Update authoritative resources to simulate step *)
    iMod (source_thread_update (K e2) with "Hj Hauth") as "[Hj Hauth]".
    iMod (source_threads_fork efs with "Hauth") as "[Hj' Hauth]".

    iMod ("Hclose" with "[Hauth]").
    { iNext. iExists _, (<[j := K e2]>tp' ++ efs), _, _.
      iFrame. intuition. iPureIntro; split; auto.
      eapply erased_rsteps_r_1; eauto.
      edestruct Hstep as (?&Hstep').
      eapply fill_step in Hstep'.
      econstructor. econstructor; eauto.
      - f_equal. symmetry. eapply take_drop_middle; eauto.
      - f_equal. rewrite app_comm_cons assoc; f_equal.
        erewrite <-take_drop_middle at 1; f_equal.
        { apply take_insert; reflexivity. }
        { f_equal. apply drop_insert_gt; lia. }
        rewrite list_lookup_insert //=.
        apply lookup_lt_is_Some_1; eauto.
      }
    iModIntro; iFrame.
  Qed.

  (*
  Lemma ghost_step_lifting_bind' {T1 T2} E j (K: T1 → proc OpT T2)
             (e1: proc OpT T1) σ1 σ2 e2 efs:
    (∀ n, ∃ n', exec_step Λ.(sem) e1 (n, σ1) (Val (n', σ2) (e2, efs))) →
    nclose sN_inv ⊆ E →
    source_ctx ∗ j ⤇ Bind e1 K ∗ source_state σ1
      ={E}=∗ j ⤇ Bind e2 K ∗ source_state σ2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ (projT2 ef).
  Proof.
    intros.
    iIntros "(Hsrc&Hj&?)". iDestruct "Hsrc" as (ρ) "Hsrc".
    iApply (ghost_step_lifting' E ρ j (fun x => Bind x K) with "[$]"); eauto.
  Qed.

  Lemma ghost_step_lifting_bind {T1 T2} E j (K: T1 → proc OpT T2)
             (e1: proc OpT T1) σ1 σ2 e2 efs:
    (∀ n, ∃ n', exec_step Λ.(sem) e1 (n, σ1) (Val (n', σ2) (e2, efs))) →
    nclose sN_inv ⊆ E →
    j ⤇ Bind e1 K -∗ source_ctx -∗ source_state σ1
      ={E}=∗ j ⤇ Bind e2 K ∗ source_state σ2 ∗ [∗ list] ef ∈ efs, ∃ j', j' ⤇ (projT2 ef).
  Proof. iIntros. iApply ghost_step_lifting_bind'; eauto. iFrame. iAssumption. Qed.

  Lemma ghost_step_bind_ret {T1 T2 T3} E j K' `{LanguageCtx OpT T2 T3 Λ K'}
        (K: T1 → proc OpT T2) v:
    nclose sN_inv ⊆ E →
    j ⤇ K' (Bind (Ret v) K) -∗ source_ctx ={E}=∗ j ⤇ K' (K v).
  Proof.
    iIntros (?) "Hj Hctx". iMod (ghost_step_lifting_puredet with "[Hj Hctx]") as "($&?)"; eauto.
    { intros. eexists. econstructor. }
  Qed.

  Lemma ghost_step_loop {T1 T2 T3} E j K `{LanguageCtx OpT T2 T3 Λ K}
        (body: T1 → proc OpT (LoopOutcome T1 T2)) v:
    nclose sN_inv ⊆ E →
    j ⤇ K (Loop body v) -∗ source_ctx ={E}=∗ j ⤇ K (loop1 body v).
  Proof.
    iIntros (?) "Hj Hctx". iMod (ghost_step_lifting_puredet with "[Hj Hctx]") as "($&?)"; eauto.
    { intros. eexists. econstructor. }
  Qed.

  Lemma ghost_step_spawn {T T'} E j K `{LanguageCtx OpT unit T Λ K} (e: proc OpT T'):
    nclose sN_inv ⊆ E →
    j ⤇ K (Spawn e) -∗ source_ctx
    ={E}=∗ j ⤇ K (Ret tt) ∗ (∃ j', j' ⤇ (Bind e (λ _, Unregister))).
  Proof.
    iIntros (?) "Hj Hctx". iMod (ghost_step_lifting_puredet with "[Hj Hctx]") as "($&H)"; eauto.
    { intros. exists (S n). econstructor.  exists (S n, σ1); split; econstructor; eauto.
      econstructor; eauto.
    }
    iModIntro. iDestruct "H" as "($&_)".
  Qed.
   *)

End ghost_step.
End ghost.

Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : bi_scope.

author: mit-pdos

repo: perennial

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


text:
(* En este archivo se demuestra que la ejecución de
*  la acción uninstall preserva los invariantes del sistema *)
Require Export Exec.
Require Export Implementacion.
Require Export AuxFunsCorrect.
Require Import Classical.
Require Import Estado.
Require Import DefBasicas.
Require Import EqTheorems.
Require Import Semantica.
Require Import Operaciones.
Require Import ErrorManagement.
Require Import Maps.
Require Import Tacticas.
Require Import MyList.
Require Import ListAuxFuns.
Require Import ValidStateLemmas.

Section UninstallInv.

Lemma UnInAppS'InAppS : forall (a a1:idApp) (s s':System) (rapp : removeApp a s s') (sysimgs : systemImage (environment s) = systemImage (environment s')) (c1 : Cmp) (inapps' : inApp c1 a1 s'), inApp c1 a1 s.
Proof.
    intros.
    destruct inapps'.
    destruct H.
    unfold inApp.
    exists x;split;auto.
    destruct H.
    left.
    destruct rapp.
    destruct_conj H2.
    destruct H4.
    destruct_conj H5.
    apply H4;auto.
    right.
    destruct H.
    destruct_conj H.
    rewrite sysimgs in *.
    exists x0;auto.
Qed.

Lemma inAppSMaybeS' : forall (s s' : System) (x : Cmp) (a x0 : idApp) (H15 : inApp x x0 s) (H2 : removeApp a s s') (H9 : systemImage (environment s) = systemImage (environment s')), inApp x x0 s' \/ a=x0.
Proof.
    intros.
    destruct H15.
    destruct H.
    destruct H.
    destruct H2.
    destruct_conj H2.
    destruct H4.
    destruct_conj H5.
    specialize (H7 x0 x1 H).
    destruct H7.
    left.
    unfold inApp.
    exists x1.
    split;auto.
    auto.
    left.
    unfold inApp.
    destruct H.
    destruct_conj H.
    exists x1.
    split;auto.
    right.
    rewrite <-H9.
    exists x2;auto.
Qed.

Lemma isAppInstalledSMaybeS' : forall (s s' : System) (a x0 : idApp) (H15 : isAppInstalled x0 s) (H2 : removeApp a s s') (H9 : systemImage (environment s) = systemImage (environment s')), isAppInstalled x0 s' \/ a=x0.
Proof.
    intros.
    destruct H15.
    destruct H2.
    destruct_conj H1.
    specialize (H2 x0 H).
    unfold isAppInstalled.
    destruct H2;auto.
    left.
    unfold isAppInstalled.
    rewrite H9 in *.
    auto.
Qed.

Lemma scGen : forall (s s': System)(X Y:Set) (a a0 : idApp) (f1 : System -> X) (f2 : X -> mapping idApp Y) (H10 : forall a' : idApp, In a' (apps (state s')) -> In a' (apps (state s))) (H2 : forall a' : idApp, In a' (apps (state s)) -> In a' (apps (state s')) \/ a' = a) (H12 : ~ In a (apps (state s'))) (H14 : forall (a' : idApp) (m' : Y), map_apply idApp_eq (f2 (f1 s')) a' = Value idApp m' -> map_apply idApp_eq (f2 (f1 s)) a' = Value idApp m') (H13 : forall (a' : idApp) (m' : Y), map_apply idApp_eq (f2 (f1 s)) a' = Value idApp m' -> map_apply idApp_eq (f2 (f1 s')) a' = Value idApp m' \/ a = a') (H16 : ~ is_Value (map_apply idApp_eq (f2 (f1 s')) a)) (YSC: In a0 (apps (state s)) <-> (exists m : Y, map_apply idApp_eq (f2 (f1 s)) a0 = Value idApp m)), In a0 (apps (state s')) <-> (exists m : Y, map_apply idApp_eq (f2 (f1 s')) a0 = Value idApp m).
Proof.
    split;intros.
    specialize (H10 a0 H).
    destruct YSC.
    specialize (H0 H10).
    destruct H0.
    exists x.
    specialize (H13 a0 x H0).
    destruct H13; auto.
    rewrite H3 in *.
    contradiction.
    destruct YSC.
    destruct H.
    specialize (H14 a0 x H).
    assert (In a0 (apps (state s))).
    apply H1.
    exists x;auto.
    specialize (H2 a0 H3).
    destruct H2;auto.
    rewrite H2 in *.
    unfold is_Value in H16.
    rewrite H in H16.
    destruct H16;auto.
Qed.

Lemma defPermsS' : forall (s s' : System) (a : idApp) (H4 : removeDefPerms a s s') (H9 : systemImage (environment s) = systemImage (environment s')) (a0 : idApp) (l : list Perm) (H10 : defPermsForApp s' a0 l), defPermsForApp s a0 l.
Proof.
    intros.
    unfold defPermsForApp.
    destruct H10.
    left.
    destruct H4.
    apply H0.
    auto.
    right.
    rewrite H9;auto.
Qed.

Lemma UninstallIsInvariant : forall (s s':System) (sValid:validstate s) (a:idApp) ,pre_uninstall a s -> post_uninstall a s s' -> validstate s'.
Proof.
    intros.
    unfold validstate.
    unfold post_uninstall in H0.
    destruct H0 as [verified H0].
    unfold pre_uninstall in H.
    destruct H.
    destruct_conj H0.

    unfold allCmpDifferent.
    split.
    intros.
    apply (UnInAppS'InAppS a a1 s) in H10;auto.
    apply (UnInAppS'InAppS a a2 s) in H12;auto.
    apply (inAppSameCmpId s sValid c1 c2 a1 a2);auto.

    unfold notRepeatedCmps.
    split.
    intros.
    apply (UnInAppS'InAppS a a1 s) in H10;auto.
    apply (UnInAppS'InAppS a a2 s) in H12;auto.
    apply (inAppSameCmp s sValid c a1 a2);auto.

    unfold notCPrunning.
    split.
    rewrite <-H8.
    destructVS sValid.
    auto.

    unfold delTmpRun.
    split.
    rewrite <- H8.
    intros.
    destruct H6.
    specialize (H6 ic cp u pt H10).
    destruct H12.
    destructVS sValid.
    unfold delTmpRun in delTmpRunVS.
    specialize (delTmpRunVS ic cp u pt H6).
    destruct delTmpRunVS.
    destruct H15.
    destruct H15.
    destruct H15.
    destruct H14.
    split.
    exists x1;auto.
    assert ( inApp (cmpCP cp) x1 s' \/ a=x1).
    apply (inAppSMaybeS' s);auto.
    destruct H17;auto.
    destruct H13.
    rewrite <-H17 in *.
    specialize (H13 ic cp u pt H14).
    unfold is_Value in H13.
    rewrite H10 in H13.
    destruct H13.
    auto.
    exists x, x0.
    split;auto.
    assert ( inApp x x0 s' \/ a=x0).
    apply (inAppSMaybeS' s);auto.
    destruct H17;auto.
    rewrite <-H17 in *.
    specialize (H1 ic x H16).
    contradiction.

    unfold cmpRunAppIns.
    split.
    rewrite <- H8.
    intros.
    assert (sV2:=sValid).
    destructVS sValid.
    unfold cmpRunAppIns in cmpRunAppInsVS.
    specialize (cmpRunAppInsVS ic c H10).
    destruct cmpRunAppInsVS.
    exists x.
    assert ( inApp c x s' \/ a=x).
    apply (inAppSMaybeS' s);auto.
    destruct H13;auto.
    rewrite <-H13 in *.
    specialize (H1 ic c H10).
    contradiction.

    unfold resContAppInst.
    split.
    intros.
    destruct H5.
    destruct_conj H12.
    specialize (H5 a0 r v H10).
    specialize (H13 a0 r v H5).
    assert (isAppInstalled a0 s).
    apply NNPP;unfold not;intros.
    absurd (is_Value (map_apply rescontdomeq (resCont (state s)) (a0,r))).
    apply notInstalledNoResCont;auto.
    unfold is_Value.
    rewrite H5;auto.
    assert (isAppInstalled a0 s' \/ a=a0).
    apply (isAppInstalledSMaybeS' s);auto.
    destruct H16;auto.
    rewrite <- H16 in *.
    specialize (H12 r).
    unfold is_Value in H12.
    rewrite H10 in H12.
    destruct H12;auto.

    unfold statesConsistency.
    split.
    split.
    unfold removeApp in H2.
    destruct_conj H2.
    unfold removeManifest in H13.
    destruct_conj H13.
    destructVS sValid.
    destructSC statesConsistencyVS a0.
    apply (scGen s s' Environment Manifest a);auto.

    split.
    unfold removeApp in H2.
    destruct_conj H2.
    unfold removeCert in H15.
    destruct_conj H15.
    destructVS sValid.
    destructSC statesConsistencyVS a0.
    apply (scGen s s' Environment Cert a);auto.

    split.
    unfold removeApp in H2.
    destruct_conj H2.
    unfold removeDefPerms in H4.
    destruct_conj H4.
    destructVS sValid.
    destructSC statesConsistencyVS a0.
    apply (scGen s s' Environment (list Perm) a);auto.

    split.
    unfold removeApp in H2.
    destruct_conj H2.
    unfold revokePerms in H0.
    destruct_conj H0.
    assert (sValid2 := sValid).
    destructVS sValid.
    destructSC statesConsistencyVS a0.
    assert (sameimg:=H9).
    assert (awasinstalled := H).
    clear allCmpDiffVS notRepCompsVS notCPRunningVS delTmpRunVS cmpRunAppInsVS resContAppInstVS notDupSysAppVS notDupPermVS allMapsCorrectVS grantedPermsExistVS H H1 H13 H15 H18 H3 H4 H5 H6 H7 H8 H9 H11 mfstSC certSC defPermsSC grantedPermGroupsSC .
    destruct permsSC.
    split;intros.
    assert (In a0 (apps (state s)) \/ (exists sysapp : SysImgApp, In sysapp (systemImage (environment s)) /\ idSI sysapp = a0)).
    rewrite sameimg.
    destruct H3.
    left.
    apply H10.
    auto.
    right.
    auto.
    specialize (H H4).
    destruct H.
    specialize (H0 a0 x H).
    destruct H0.
    destruct H0.
    destruct H0.
    exists x0;auto.
    rewrite H0 in *.
    destruct H3.
    contradiction.
    destruct H3.
    rewrite<- sameimg in *.
    assert (~(In a0 (apps (state s)) /\ In x0 (systemImage (environment s)) /\ idSI x0 = a0)).
    apply sysAppInApps;auto.
    destruct H5.
    split;auto.

    destruct H3.
    specialize (H14 a0 x H3).
    destruct H14.
    assert ( In a0 (apps (state s)) \/ (exists sysapp : SysImgApp, In sysapp (systemImage (environment s)) /\ idSI sysapp = a0)).
    apply H1.
    exists x0;auto.
    destruct H5.
    specialize (H2 a0 H5).
    destruct H2;auto.
    rewrite H2 in *.
    unfold is_Value in H16.
    rewrite H3 in H16.
    destruct H16;auto.
    right.
    rewrite<- sameimg;auto.

    unfold removeApp in H2.
    destruct_conj H2.
    unfold revokePermGroups in H3.
    destruct_conj H3.
    assert (sValid2 := sValid).
    destructVS sValid.
    destructSC statesConsistencyVS a0.
    assert (sameimg:=H9).
    assert (awasinstalled := H).
    clear allCmpDiffVS notRepCompsVS notCPRunningVS delTmpRunVS cmpRunAppInsVS resContAppInstVS notDupSysAppVS notDupPermVS allMapsCorrectVS grantedPermsExistVS H H1 H13 H15 H18 H0 H4 H5 H6 H7 H8 H9 H11 mfstSC certSC defPermsSC permsSC.
    destruct grantedPermGroupsSC.
    split;intros.
    assert (In a0 (apps (state s)) \/ (exists sysapp : SysImgApp, In sysapp (systemImage (environment s)) /\ idSI sysapp = a0)).
    rewrite sameimg.
    destruct H1.
    left.
    apply H10.
    auto.
    right.
    auto.
    specialize (H H4).
    destruct H.
    specialize (H3 a0 x H).
    destruct H3.
    exists x;auto.
    rewrite H3 in *.
    destruct H1.
    contradiction.
    destruct H1.
    rewrite<- sameimg in *.
    assert (~(In a0 (apps (state s)) /\ In x0 (systemImage (environment s)) /\ idSI x0 = a0)).
    apply sysAppInApps;auto.
    destruct H5.
    split;auto.

    destruct H1.
    specialize (H14 a0 x H1).
    assert ( In a0 (apps (state s)) \/ (exists sysapp : SysImgApp, In sysapp (systemImage (environment s)) /\ idSI sysapp = a0)).
    apply H0.
    exists x;auto.
    destruct H4.
    specialize (H2 a0 H4).
    destruct H2;auto.
    rewrite H2 in *.
    unfold is_Value in H16.
    rewrite H1 in H16.
    destruct H16;auto.
    right.
    rewrite<- sameimg;auto.

    unfold notDupApp.
    split.
    intros.
    rewrite <-H9.
    destruct H2.
    specialize (H2 a0 H10).
    unfold not;intros.
    destruct H13.
    destruct (sysAppInApps s sValid a0 x);auto.

    unfold notDupSysApp.
    split.
    rewrite <-H9.
    destructVS sValid.
    auto.

    unfold notDupPerm.
    split.
    intros.
    assert (defPermsForApp s a0 l).
    apply (defPermsS' s s' a);auto.
    assert (defPermsForApp s a' l').
    apply (defPermsS' s s' a);auto.
    apply (notDupPermVS s sValid a0 a' p p' l l');auto.

    unfold allMapsCorrect.
    split.
    destruct H2.
    destruct_conj H10.
    destruct H13, H15, H0, H3, H4, H5, H6, H7.
    destruct_conj H14.
    destruct_conj H16.
    destruct_conj H17.
    destruct_conj H18.
    destruct_conj H19.
    destruct_conj H20.
    destruct_conj H21.
    destruct_conj H22.
    mapcorrect sValid.
    rewrite <-H8.
    repeat (split;auto).

    unfold grantedPermsExist.
    split.
    intros.
    destruct H0.
    specialize (H0 a0 l H10).
    destruct H0.
    destruct_conj H13.
    specialize (H14 a0 x H0).
    destruct H14.
    destruct H14.
    destruct H14.
    rewrite H10 in H14.
    inversion H14.
    rewrite <- H18 in *.
    assert (exists defPermsA, map_apply idApp_eq (defPerms (environment s)) a = Value idApp defPermsA).
    apply (ifInAppThenDefPerms);auto.
    destruct H17.
    specialize (H15 x1 p H17).
    destruct H15.
    specialize (H19 H12).
    destruct H19.
    assert (permExists p s).
    apply (grantedPermsExistVS s sValid a0 p x);auto.
    unfold permExists.
    destruct H21.
    left;auto.
    right.
    unfold usrDefPerm.
    destruct H21.
    destruct H21.
    destruct H21.
    destruct H21.
    destruct H4.
    destruct_conj H23.
    specialize (H24 x2 x3 H21).
    destruct H24.
    left.
    exists x2, x3;auto.
    rewrite <-H24 in *.
    rewrite H21 in H17.
    inversion H17.
    rewrite H27 in *;contradiction.
    right.
    rewrite <- H9;auto.
    unfold is_Value in H13.
    rewrite<-H14 in *.
    rewrite H10 in H13.
    destruct H13;auto.

    unfold noDupSentIntents.
    rewrite<- H11.
    destructVS sValid.
    auto.
Qed.

End UninstallInv.

author: g-deluca

repo: android-coq-model


text:
(*
  Copyright 2022 ZhengPu Shi
  This file is part of CoqMatrix. It is distributed under the MIT
  "expat license". You should have recieved a LICENSE file with it.

  purpose   : Vector Theory implemented with DepPair
  author    : ZhengPu Shi
  date      : 2022.06

  remark    :
*)

Require Export VectorTheory.
Require Import DepPair.MatrixTheoryDP.

(* ######################################################################### *)
(** * Basic vector theory implemented with DepList *)

Module BasicVectorTheoryDP (E : ElementType).

  (* ==================================== *)
  (** ** Also contain matrix theory *)
  Module Export BasicMatrixTheoryDP := BasicMatrixTheoryDP E.

  (* ==================================== *)
  (** ** Vector element type *)
  Export E.

  Infix "==" := (eqlistA Aeq) : list_scope.

  Open Scope nat_scope.
  Open Scope A_scope.
  Open Scope vec_scope.

  (* ==================================== *)
  (** ** Vector type *)

  Definition vec n := mat n 1.

  (** matrix equality *)
  Definition veq {n} (v1 v2 : vec n) := meq v1 v2.
  Infix "==" := veq : vec_scope.

  (** meq is equivalence relation *)
  Lemma veq_equiv : forall n, Equivalence (veq (n:=n)).
  Proof.
    intros. apply meq_equiv.
  Qed.

  (** Get element of vector *)
  Definition vnth {n} (v : vec n) i : A := @mnth n 1 v i 0.

(*   Notation "v .[ i ]" := (vnth v i) (at level 30) : vec_scope. *)
  (* Notation "v . [ i ]" := (vnth i v) (at level 30). *)

  (** veq and mnth should satisfy this constraint *)
  Lemma veq_iff_vnth : forall {n : nat} (v1 v2 : vec n),
      (v1 == v2) <-> (forall i, i < n -> (vnth v1 i == vnth v2 i)%A).
  Proof.
    intros.
  Admitted.

  (* ==================================== *)
  (** ** Convert between list and vector *)
  Definition v2l {n} (v : vec n) : list A := hdc A0 (m2l v).
  (* Definition v2l' {n} (v : vec n) : list A := to_list (mcoli v F1). *)

  Definition l2v {n} (l : list A) : vec n := l2m (row2col l).

  Lemma v2l_length : forall {n} (v : vec n), length (v2l v) = n.
  Admitted.

  Lemma v2l_l2v_id : forall {n} (l : list A),
    length l = n -> (@v2l n (@l2v n l) == l)%list.
  Admitted.

  Lemma l2v_v2l_id : forall {n} (v : vec n), l2v (v2l v) == v.
  Admitted.

  (* ==================================== *)
  (** ** Convert between tuples and vector *)
  Definition t2v_2 (t : @T2 A) : vec 2 := let '(a,b) := t in l2v [a;b].
  Definition t2v_3 (t : @T3 A) : vec 3 := let '(a,b,c) := t in l2v [a;b;c].
  Definition t2v_4 (t : @T4 A) : vec 4 := let '(a,b,c,d) := t in l2v [a;b;c;d].

  Definition v2t_2 (v : vec 2) : @T2 A.
    destruct v as (a1, (a2, _)).
    destruct a1 as (a11,_), a2 as (a21,_).
    apply (a11,a21).
  Defined.

  Definition v2t_3 (v : vec 3) : @T3 A.
    destruct v as (a1, (a2, (a3, _))).
    destruct a1 as (a11,_), a2 as (a21,_), a3 as (a31,_).
    apply (a11,a21,a31).
  Defined.

  Definition v2t_4 (v : vec 4) : @T4 A.
    destruct v as (a1, (a2, (a3, (a4, _)))).
    destruct a1 as (a11,_), a2 as (a21,_), a3 as (a31,_), a4 as (a41,_).
    apply (a11,a21,a31,a41).
  Defined.

  Lemma v2t_t2v_id_2 : forall (t : A * A), v2t_2 (t2v_2 t) = t.
  Proof.
    intros. destruct t. simpl. unfold v2t_2. f_equal.
  Qed.

  Lemma t2v_v2t_id_2 : forall (v : vec 2), t2v_2 (v2t_2 v) == v.
  Proof.
    intros.
    repeat match goal with
    | v : vec _ |- _ => destruct v
    | v : Vector.vec _ |- _ => destruct v
    end.
    easy.
  Qed.

  (** mapping of a vector *)
  Definition vmap {n} (v : vec n) f : vec n := mmap f v.

  (** folding of a vector *)
(*   Definition vfold : forall {B : Type} {n} (v : vec n) (f : A -> B) (b : B), B. *)

  (** mapping of two matrices *)
  Definition vmap2 {n} (v1 v2 : vec n) f : vec n := mmap2 f v1 v2.

End BasicVectorTheoryDP.

(* ######################################################################### *)
(** * Ring vector theory implemented with DepList  *)

(** zero vector, vector addition, opposition, substraction, scalar multiplication,
    dot product *)
Module RingVectorTheoryDP (E : RingElementType) <: RingVectorTheory E.

  (* ==================================== *)
  (** ** Also contain matrix theory *)
  Module Export RingMatrixTheoryDP := RingMatrixTheoryDP E.

  Export E.
  Include (BasicVectorTheoryDP E).

  (** ** Zero vector *)
  Definition vec0 {n} : vec n := mat0 n 1.

  (* (** Assert that a vector is an zero vector. *) *)
  (* Definition vzero {n} (v : vec n) : Prop := v = vec0. *)

  (* (** Assert that a vector is an non-zero vector. *) *)
  (* Definition vnonzero {n} (v : vec n) : Prop := ~(vzero v). *)

  (* (** vec0 is equal to mat0 with column 1 *) *)
  (* Lemma vec0_eq_mat0 : forall n, vec0 = mat0 n 1. *)
  (* Proof. *)
  (*   intros. easy. *)
  (* Qed. *)

  (* (** It is decidable that if a vector is zero vector. *) *)
  (* Lemma vzero_dec : forall {n} (v : vec n), {vzero v} + {vnonzero v}. *)
  (* Proof. *)
  (*   intros. apply meq_dec. *)
  (* Qed. *)

  (** *** Vector addition *)

  Definition vadd {n} (v1 v2 : vec n) : vec n := madd v1 v2.
  Infix "+" := vadd.

  (** v1 + v2 = v2 + v1 *)
  Lemma vadd_comm : forall {n} (v1 v2 : vec n), (v1 + v2) == (v2 + v1).
  Proof.
    intros. apply madd_comm.
  Qed.

  (** (v1 + v2) + v3 = v1 + (v2 + v3) *)
  Lemma vadd_assoc : forall {n} (v1 v2 v3 : vec n), (v1 + v2) + v3 == v1 + (v2 + v3).
  Proof.
    intros. apply madd_assoc.
  Qed.

  (** vec0 + v = v *)
  Lemma vadd_0_l : forall {n} (v : vec n), vec0 + v == v.
  Proof.
    intros. apply madd_0_l.
  Qed.

  (** v + vec0 = v *)
  Lemma vadd_0_r : forall {n} (v : vec n), v + vec0 == v.
  Proof.
    intros. apply madd_0_r.
  Qed.

  (** *** Vector opposite *)

  Definition vopp {n} (v : vec n) : vec n := mopp v.
  Notation "- v" := (vopp v).

  (** v + (- v) = vec0 *)
  Lemma vadd_opp_r : forall {n} (v : vec n), v + (- v) == vec0.
  Proof.
    intros. apply madd_opp.
  Qed.

  (** (- v) + v = vec0 *)
  Lemma vadd_opp_l : forall {n} (v : vec n), (- v) + v == vec0.
  Proof.
    intros. rewrite vadd_comm. apply madd_opp.
  Qed.

  (** *** Vector subtraction *)

  Definition vsub {n} (v1 v2 : vec n) : vec n := v1 + (- v2).
  Infix "-" := vsub.

  (** *** Vector scalar multiplication *)

  Definition vcmul {n} a (v : vec n) : vec n := a c* v.
  Definition vmulc {n} (v : vec n) a : vec n := v *c a.

  (** v *c a = a c* v *)
  Lemma vmulc_eq_vcmul : forall {n} a (v : vec n), v *c a == a c* v.
  Proof.
    intros. apply mmulc_eq_mcmul.
  Qed.

  (** a c* (b c* v) = (a * b) c* v *)
  Lemma vcmul_assoc : forall {n} a b (v : vec n), a c* (b c* v) == (a * b) c* v.
  Proof.
    intros. apply mcmul_assoc.
  Qed.

  (** a c* (b c* v) = b c* (a c* v) *)
  Lemma vcmul_perm : forall {n} a b (v : vec n), a c* (b c* v) == b c* (a c* v).
  Proof.
    intros. apply mcmul_perm.
  Qed.

  (** (a + b) c* v = (a c* v) + (b c* v) *)
  Lemma vcmul_add_distr_l : forall {n} a b (v : vec n),
    (a + b)%A c* v == (a c* v) + (b c* v).
  Proof.
    intros. apply mcmul_add_distr_r.
  Qed.

  (** a c* (v1 + v2) = (a c* v1) + (a c* v2) *)
  Lemma vcmul_add_distr_r : forall {n} a (v1 v2 : vec n),
    a c* (v1 + v2) == (a c* v1) + (a c* v2).
  Proof.
    intros. unfold vadd. apply mcmul_add_distr_l.
  Qed.

  (** 1 c* v = v *)
  Lemma vcmul_1_l : forall {n} (v : vec n), A1 c* v == v.
  Proof.
    intros. apply mcmul_1_l.
  Qed.

  (** 0 c* v = vec0 *)
  Lemma vcmul_0_l : forall {n} (v : vec n), A0 c* v == vec0.
  Proof.
    intros. apply mcmul_0_l.
  Qed.

  (** *** Vector dot product *)

  (** dot production of two vectors.
      Here, we use matrix multiplication to do it, and it is a different way to
      general situation. *)
  Definition vdot {n : nat} (v1 v2 : vec n) :=
    scalar_of_mat (v1\T * v2)%mat.

End RingVectorTheoryDP.

(* ######################################################################### *)
(** * Decidable-field vector theory implemented with DepPair  *)

Module DecidableFieldVectorTheoryDP (E : DecidableFieldElementType)
<: DecidableFieldVectorTheory E.

  (* ==================================== *)
  (** ** Also contain matrix theory *)
  Module Export DecidableFieldMatrixTheoryDP := DecidableFieldMatrixTheoryDP E.

  Export E.
  Include (RingVectorTheoryDP E).

  (** veq is decidable *)
  Lemma veq_dec : forall (n : nat), Decidable (veq (n:=n)).
  Proof. intros. apply meq_dec. Qed.

End DecidableFieldVectorTheoryDP.

(* ######################################################################### *)
(** * Test  *)
Module Test.

  Module Import VectorR := RingVectorTheoryDP RingElementTypeR.
  Import Reals.
  Open Scope R.

  Definition v1 := @l2v 3 [1;2;3].
  Definition v2 := @l2v 3 [4;5;6].
  Example vdot_ex1 : vdot v1 v2 = (4+10+18)%R.
  Proof.
    compute. ring.
  Qed.

End Test.

(** ** Others, later ... *)

(*
  (* ==================================== *)
  (** ** Vector equility *)
  Lemma veq_dec : forall {n} (v1 v2 : V n), {v1 = v2} + {v1 <> v2}.
  Proof.
    intros. apply meq_dec.
  Qed.

  (* ==================================== *)
  (** ** 2-dim vector operations *)

  Definition vlen2 (v : V 2) : X :=
    let '(x,y) := v2t_2 v in
      (x * x + y * y)%X.

  (* ==================================== *)
  (** ** 3-dim vector operations *)

  Definition vlen3 (v : V 3) : X :=
    let '(x,y,z) := v2t_3 v in
      (x * x + y * y + z * z)%X.

  Definition vdot3 (v0 v1 : V 3) : X :=
    let '(a0,b0,c0) := v2t_3 v0 in
    let '(a1,b1,c1) := v2t_3 v1 in
      (a0 * a1 + b0 * b1 + c0 * c1)%X.
 *)

author: zhengpushi

repo: CoqMatrix

save_path: github-repos/coq/zhengpushi-CoqMatrix


text:
Require Export euclidean__axioms.
Require Export euclidean__defs.
Require Export euclidean__tactics.
Require Export lemma__ABCequalsCBA.
Require Export lemma__collinearorder.
Require Export lemma__equalanglesNC.
Require Export lemma__equalanglessymmetric.
Require Export lemma__equalanglestransitive.
Require Export logic.
Definition lemma__equalanglesflip : forall A B C D E F, (euclidean__defs.CongA A B C D E F) -> (euclidean__defs.CongA C B A F E D).
Proof.
intro A.
intro B.
intro C.
intro D.
intro E.
intro F.
intro H.
assert (* Cut *) (euclidean__axioms.nCol D E F) as H0.
- apply (@euclidean__tactics.nCol__notCol D E F).
--apply (@euclidean__tactics.nCol__not__Col D E F).
---apply (@lemma__equalanglesNC.lemma__equalanglesNC A B C D E F H).

- assert (* Cut *) (euclidean__defs.CongA D E F A B C) as H1.
-- apply (@lemma__equalanglessymmetric.lemma__equalanglessymmetric A B C D E F H).
-- assert (* Cut *) (euclidean__axioms.nCol A B C) as H2.
--- apply (@euclidean__tactics.nCol__notCol A B C).
----apply (@euclidean__tactics.nCol__not__Col A B C).
-----apply (@lemma__equalanglesNC.lemma__equalanglesNC D E F A B C H1).

--- assert (* Cut *) (~(euclidean__axioms.Col C B A)) as H3.
---- intro H3.
assert (* Cut *) (euclidean__axioms.Col A B C) as H4.
----- assert (* Cut *) ((euclidean__axioms.Col B C A) /\ ((euclidean__axioms.Col B A C) /\ ((euclidean__axioms.Col A C B) /\ ((euclidean__axioms.Col C A B) /\ (euclidean__axioms.Col A B C))))) as H4.
------ apply (@lemma__collinearorder.lemma__collinearorder C B A H3).
------ destruct H4 as [H5 H6].
destruct H6 as [H7 H8].
destruct H8 as [H9 H10].
destruct H10 as [H11 H12].
exact H12.
----- apply (@euclidean__tactics.Col__nCol__False A B C H2 H4).
---- assert (* Cut *) (euclidean__defs.CongA C B A A B C) as H4.
----- apply (@lemma__ABCequalsCBA.lemma__ABCequalsCBA C B A).
------apply (@euclidean__tactics.nCol__notCol C B A H3).

----- assert (* Cut *) (euclidean__defs.CongA C B A D E F) as H5.
------ apply (@lemma__equalanglestransitive.lemma__equalanglestransitive C B A A B C D E F H4 H).
------ assert (* Cut *) (euclidean__defs.CongA D E F F E D) as H6.
------- apply (@lemma__ABCequalsCBA.lemma__ABCequalsCBA D E F H0).
------- assert (* Cut *) (euclidean__defs.CongA C B A F E D) as H7.
-------- apply (@lemma__equalanglestransitive.lemma__equalanglestransitive C B A D E F F E D H5 H6).
-------- exact H7.
Qed.

author: Karnaj

repo: dktactgeo

save_path: github-repos/coq/Karnaj-dktactgeo


text:
Require Import MapProofs.Common.
Set Bullet Behavior "Strict Subproofs".
Require Import MapProofs.Bounds.
Require Import MapProofs.Tactics.

Section WF.
Context {e : Type} {a : Type} {HEq : Eq_ e} {HOrd : Ord e} {HEqLaws : EqLaws e}  {HOrdLaws : OrdLaws e}.
(** ** Verification of [maxViewSure] *)

Lemma maxViewSure_Desc:
  forall sz' (x: e) (v: a) s1 s2 lb ub,
    Bounded (Bin sz' x v s1 s2) lb ub ->
    forall P,
    (forall y vy r,
      (y = x /\ vy = v \/ sem s2 y = Some vy) /\
      Desc r lb (Some y) (size s1 + size s2)
                         (fun i => if i == y then None else (sem s1 i ||| (if i == x then Some v else None) ||| sem s2 i)) ->
      P (Mk_MaxView y vy r)) ->
    P (maxViewSure x v s1 s2).
    (* we know that y is in the input, and we actually know more: it is x or in s2 *)
Proof.
  intros ??????? HB.
  revert sz' x v s1 lb ub HB.
  induction s2; intros sz' x v s1 lb ub HB;subst.
  - clear IHs2_1.
    simpl.
    intros X HX.
    destruct (maxViewSure k a0 s2_1 s2_2) eqn:HmaxView.
    apply HX. clear X HX.

    inversion HB; subst; clear HB.
    inversion H5; subst.

    revert HmaxView.
    eapply IHs2_2; only 1: solve_Bounded e.
    intros y vy r H; destruct H as [Hthere IHD]; clear IHs2_2.
    cbn -[Z.add size] in *; rewrite size_Bin in H11.

    intro HmaxView; inversion HmaxView; subst; clear HmaxView.

    applyDesc e IHD; clear IHD.

    split.
    + right.
      destruct Hthere as [[H H2]|H]; rewrite H in *.
      * subst. rewrite Eq_refl.
        erewrite sem_outside_above by solve_Bounds e.
        reflexivity.
      * erewrite sem_outside_above by solve_Bounds e.
        replace (e0 == k) with false by solve_Bounds e.
        reflexivity.
    + destruct Hthere as [[Heq Heq1]|Hthere].
      * subst; applyDesc e (@balanceL_Desc e a); solve_Desc e.
      * applyDesc e (@balanceL_Desc e a).
        solve_Desc e.
  - intros X HX.
    destruct (maxViewSure _ _ _ _) eqn:HmaxView.
    apply HX. clear X HX.
    cbn -[Z.add size] in *.
    inversion HB; subst; clear HB.
    inversion HmaxView; subst; clear HmaxView.
    split; [left; (split;reflexivity) | solve_Desc e].
Qed.

(** ** Verification of [lookupMin] *)

Lemma empty_no_elts : forall (m: Map e a),
  (forall i, sem m i = None) <-> m = empty.
Proof.
  intros. split; intros.
  destruct m. specialize (H e0). simpl in H. destruct (sem m1 e0); simpl in H.
  inversion H. rewrite Eq_Reflexive in H. inversion H. reflexivity. rewrite H. reflexivity.
Qed.

Lemma lookupMin_in_bin: forall (m: Map e a),
  m <> Tip -> forall k1 k2 v1 v2, lookupMinSure k1 v1 m = lookupMinSure k2 v2 m.
Proof.
  intros. destruct m; intros.
  - simpl. reflexivity.
  - contradiction.
Qed.

Lemma lookupMax_in_bin: forall (m: Map e a),
  m <> Tip -> forall k1 k2 v1 v2, lookupMaxSure k1 v1 m = lookupMaxSure k2 v2 m.
Proof.
  intros. destruct m; intros.
  - simpl. reflexivity.
  - contradiction.
Qed.

Lemma lookupMinSure_Desc:
  forall (m: Map e a) x v0 lb ub,
    Bounded m lb ub ->
    let (y, v) := lookupMinSure x v0 m in
    ((forall i, sem m i = None) /\ y = x /\ v = v0 \/
      sem m y = Some v /\ (forall i v1, sem m i = Some v1 -> (y GHC.Base.<= i) = true)).
Proof.
  intros.  revert x v0. induction H; intros.
  - left. simpl. intuition.
  - destruct (lookupMinSure x0 v0 (Bin sz x v s1 s2)) eqn : ?. right. simpl.
    specialize (IHBounded1 x0 v0). destruct (lookupMinSure x0 v0 s1) eqn : ?. destruct IHBounded1.
    + destruct H5. destruct H6. assert (sem s1 e0 = None) by (apply H5). rewrite H8; simpl. subst.
      simpl in Heqp. apply empty_no_elts in H5. subst. inversion Heqp. subst.
      rewrite Eq_Reflexive. simpl. split. reflexivity. intros.
      destruct (e0 == i) eqn : ?. order e. assert (i == e0 = false) by order e. rewrite H5 in H3.
      simpl in H3. solve_Bounds e.
    + destruct H5. simpl in Heqp. assert (s1 <> Tip). { destruct s1. intro. discriminate H7.
      simpl in H5. inversion H5. }
      eapply lookupMin_in_bin in H7. rewrite Heqp in H7. rewrite Heqp0 in H7. inversion H7; subst.
      rewrite H5. simpl. split. reflexivity. intros.
      destruct (sem s1 i) eqn : ?. simpl in H3. inversion H3; subst.
      apply H6 in Heqo. assumption.
      simpl in H3. assert (_GHC.Base.<=_  e1 x = true) by solve_Bounds e.
      destruct (i == x) eqn : ?. order e. simpl in H3. solve_Bounds e.
Qed.

Lemma lookupMin_Desc:
  forall (m: Map e a) lb ub,
    Bounded m lb ub ->
    match lookupMin m with
      | None => (forall i, sem m i = None)
      | Some (y, v) => sem m y = Some v /\ (forall i v1, sem m i = Some v1 -> (y GHC.Base.<= i) = true)
    end.
Proof.
  intros.
  unfold lookupMin.
  inversion H; subst; clear H.
  * reflexivity.
  * simpl.
    pose proof (lookupMinSure_Desc s1 x v lb (Some x) H0). destruct (lookupMinSure x v s1) eqn : ?.
    destruct H.
    - destruct H; subst. apply empty_no_elts in H; subst. simpl. simpl in Heqp. inversion Heqp; subst.
      rewrite Eq_Reflexive. simpl. split. reflexivity. intros. destruct (i == e0) eqn : ?.
      order e. simpl in H. solve_Bounds e.
    - destruct H. rewrite H. simpl; split. reflexivity. intros. destruct (sem s1 i) eqn : ?.
      apply H4 in Heqo. assumption. simpl in H6. destruct (i == x) eqn : ?.
      solve_Bounds e. simpl in H6. solve_Bounds e.
Qed.

(** ** Verification of [lookupMax] *)

Lemma lookupMaxSure_Desc:
  forall (m: Map e a) x v0 lb ub,
    Bounded m lb ub ->
    let (y, v) := lookupMaxSure x v0 m in
    ((forall i, sem m i = None) /\ y = x /\ v = v0 \/
      sem m y = Some v /\ (forall i v1, sem m i = Some v1 -> (i GHC.Base.<= y) = true)).
Proof.
  intros.  revert x v0. induction H; intros.
  - left. simpl. intuition.
  - destruct (lookupMaxSure x0 v0 (Bin sz x v s1 s2)) eqn : ?. right. simpl.
    specialize (IHBounded2 x0 v0). destruct (lookupMaxSure x0 v0 s2) eqn : ?. destruct IHBounded2.
    + destruct H5. destruct H6. assert (sem s2 e0 = None) by (apply H5). rewrite H8; simpl. subst.
      simpl in Heqp. apply empty_no_elts in H5. subst. inversion Heqp. subst.
      rewrite Eq_Reflexive. simpl.  assert (sem s1 e0 = None). { eapply sem_outside_above.
      apply H. unfold isUB. order e. } split. rewrite H3. reflexivity. intros.
      destruct (e0 == i) eqn : ?. order e. assert (i == e0 = false) by order e. rewrite H6 in H5.
      simpl in H5. rewrite oro_None_r in H5. rewrite oro_None_r in H5. solve_Bounds e.
    + destruct H5. simpl in Heqp. assert (s2 <> Tip). { destruct s2. intro. discriminate H7.
      simpl in H5. inversion H5. }
      eapply lookupMax_in_bin in H7. rewrite Heqp in H7. rewrite Heqp0 in H7. inversion H7; subst.
      rewrite H5. assert (sem s1 e1 = None). { eapply (sem_inside H0) in H5. destruct H5.
      eapply sem_outside_above. apply H. solve_Bounds e. } rewrite H3. simpl.
      destruct (e1 == x) eqn : ?. solve_Bounds e. simpl. split. reflexivity. intros.
      destruct (sem s1 i) eqn : ?. solve_Bounds e. simpl in H8. destruct (i == x) eqn : ?.
      solve_Bounds e. simpl in H8. apply H6 in H8. assumption.
Qed.

Lemma lookupMax_Desc:
  forall (m: Map e a) lb ub,
    Bounded m lb ub ->
    match lookupMax m with
      | None => (forall i, sem m i = None)
      | Some (y, v) => sem m y = Some v /\ (forall i v1, sem m i = Some v1 -> (i GHC.Base.<= y) = true)
    end.
Proof.
  intros.
  unfold lookupMax.
  inversion H; subst; clear H.
  * reflexivity.
  * simpl.
    pose proof (lookupMaxSure_Desc s2 x v (Some x) ub H1). destruct (lookupMaxSure x v s2) eqn : ?.
    destruct H.
    - destruct H; subst. apply empty_no_elts in H; subst. simpl. simpl in Heqp. inversion Heqp; subst.
      rewrite Eq_Reflexive. simpl. split. assert (sem s1 e0 = None). { eapply sem_outside_above.
      apply H0. solve_Bounds e. } rewrite H. reflexivity.
      intros. destruct (i == e0) eqn : ?.
      order e. simpl in H. rewrite oro_None_r in H. rewrite oro_None_r in H. solve_Bounds e.
    - destruct H. rewrite H. simpl; split. assert (sem s1 e0 = None). { eapply sem_outside_above.
      apply H0. apply (sem_inside H1) in H. solve_Bounds e. } rewrite H6.
      destruct (e0 == x) eqn : ?. solve_Bounds e. simpl. reflexivity.
      intros. destruct (sem s1 i) eqn : ?. solve_Bounds e. simpl in H6. destruct (i == x) eqn : ?.
      solve_Bounds e. simpl in H6. eapply H4. apply H6.
Qed.

(** ** Verification of [minViewSure] *)

Lemma minViewSure_Desc:
  forall sz' (x: e) (v: a) s1 s2 lb ub,
    Bounded (Bin sz' x v s1 s2) lb ub ->
    forall P,
    (forall y vy r,
      (y = x /\ vy = v \/ sem s1 y = Some vy) /\
      Desc r (Some y) ub (size s1 + size s2)
                         (fun i => if i == y then None else (sem s1 i ||| (if i == x then Some v else None) ||| sem s2 i)) ->
      P (Mk_MinView y vy r)) ->
    P (minViewSure x v s1 s2).
    (* we know that y is in the input, and we actually know more: it is x or in s2 *)
Proof.
  intros ??????? HB.
  revert sz' x v s2 lb ub HB.
  induction s1; intros sz' x v s2 lb ub HB;subst.
  - clear IHs1_2.
    simpl.
    intros X HX.
    destruct (minViewSure _ _ _ _ ) eqn:HmaxView.
    apply HX. clear X HX.

    inversion HB; subst; clear HB.
    inversion H4; subst.

    revert HmaxView.
    eapply IHs1_1; only 1: solve_Bounded e.
    intros y vy r H; destruct H as [Hthere IHD]; clear IHs1_1.
    cbn -[Z.add size] in *; rewrite size_Bin in H11.

    intro HmaxView; inversion HmaxView; subst; clear HmaxView.

    applyDesc e IHD; clear IHD.

    split.
    + right.
      destruct Hthere as [[H H2]|H]; rewrite H in *.
      * subst. rewrite Eq_refl.
        erewrite sem_outside_above by solve_Bounds e.
        reflexivity.
      * reflexivity.
    + destruct Hthere as [[Heq Heq1]|Hthere].
      * subst; applyDesc e (@balanceR_Desc e a); solve_Desc e.
      * applyDesc e (@balanceR_Desc e a); solve_Desc e.
  - intros X HX.
    destruct (minViewSure _ _ _ _) eqn:Hview.
    apply HX. clear X HX.
    cbn -[Z.add size] in *.
    inversion HB; subst; clear HB.
    inversion Hview; subst; clear Hview.
    split; [left; (split;reflexivity) | solve_Desc e].
Qed.

(** ** Verification of [maxView] *)

Lemma maxViewWithKey_Desc:
  forall (m: Map e a) lb ub,
    Bounded m lb ub ->
    forall (P : option ((e * a) * Map e a) -> Prop),
    (forall y r v,
      (sem m y = Some v) /\
      Desc r lb (Some y) (size m - 1) (fun i => if (i == y) then None else sem m i) ->
      P (Some ((y, v), r))) ->
    ((forall i, sem m i = None) -> P None) ->
    P (maxViewWithKey m).
Proof.
  intros ??? HB P HSome HNone.
  unfold maxViewWithKey.
  inversion HB; subst.
  * apply HNone. intro; reflexivity.
  * unfold op_zdzn__, Datatypes.id, op_zd__.
    eapply maxViewSure_Desc; only 1: eassumption.
    intros.
    apply HSome.
    split.
    - simpl. destruct H3. destruct H3. destruct H3. subst. rewrite Eq_Reflexive.
      assert (sem s1 x = None). { eapply sem_outside_above. apply H. solve_Bounds e. }
      rewrite H3. simpl. reflexivity. rewrite H3.
      assert (sem s1 y = None). { eapply sem_outside_above. apply H. solve_Bounds e. }
      rewrite H6. simpl. destruct (y == x) eqn : ?. solve_Bounds e. reflexivity.
    - applyDesc e H3. solve_Desc e.
Qed.

Lemma maxViewDesc:
  forall (m: Map e a) lb ub,
  Bounded m lb ub ->
  maxView m = match maxViewWithKey m with
            |None => None
            | Some ((x,y), m) => Some (y, m)
            end.
Proof.
  intros. unfold maxView. reflexivity.
Qed.

(** ** Verification of [minView] *)

Lemma minViewWithKey_Desc:
  forall (m: Map e a) lb ub,
    Bounded m lb ub ->
    forall (P : option ((e * a) * Map e a) -> Prop),
    (forall y r v,
      (sem m y = Some v) /\
      Desc r (Some y) ub  (size m - 1) (fun i => if (i == y) then None else sem m i) ->
      P (Some ((y, v), r))) ->
    ((forall i, sem m i = None) -> P None) ->
    P (minViewWithKey m).
Proof.
  intros ??? HB P HSome HNone.
  unfold minViewWithKey.
  inversion HB; subst.
  * apply HNone. intro; reflexivity.
  * unfold op_zdzn__, Datatypes.id, op_zd__.
    eapply minViewSure_Desc; only 1: eassumption.
    intros.
    apply HSome.
    split.
    - simpl. destruct H3. destruct H3. destruct H3. subst. rewrite Eq_Reflexive.
      assert (sem s1 x = None). { eapply sem_outside_above. apply H. solve_Bounds e. }
      rewrite H3. simpl. reflexivity. rewrite H3. simpl. reflexivity.
    - applyDesc e H3. solve_Desc e.
Qed.

Lemma minViewDesc:
  forall (m: Map e a) lb ub,
  Bounded m lb ub ->
  minView m = match minViewWithKey m with
            |None => None
            | Some ((x,y), m) => Some (y, m)
            end.
Proof.
  intros. unfold minView. reflexivity.
Qed.

End WF.

author: antalsz

repo: hs-to-coq

save_path: github-repos/coq/antalsz-hs-to-coq


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable rt_ : Universe -> Universe -> Prop.
Variable r_ : Universe -> Universe -> Prop.
Variable goal_ : Prop.
Variable dom_ : Universe -> Prop.

Variable c_ : Universe.
Variable b_ : Universe.
Variable a_ : Universe.

Variable initial_model_1 : (dom_ a_ /\ (dom_ b_ /\ (dom_ c_ /\ (rt_ a_ b_ /\ rt_ a_ c_)))).
Variable goal_ax_2 : (forall X : Universe, ((dom_ X /\ (rt_ b_ X /\ rt_ c_ X)) -> goal_)).
Variable r_in_rt_3 : (forall X Y : Universe, (r_ X Y -> rt_ X Y)).
Variable trans_rt_4 : (forall X Y Z : Universe, ((rt_ X Y /\ rt_ Y Z) -> rt_ X Z)).
Variable r_or_rr_5 : (forall X Y : Universe, (rt_ X Y -> (exists U : Universe, (r_ X Y \/ (dom_ U /\ (rt_ X U /\ rt_ U Y)))))).
Variable cdp_6 : (forall X Y Z : Universe, ((rt_ X Y /\ r_ X Z) -> (exists U : Universe, (dom_ U /\ (r_ Y U /\ rt_ Z U))))).
Variable ih_cdp1_7 : (forall X Y : Universe, ((rt_ a_ X /\ (rt_ X b_ /\ rt_ a_ Y)) -> (exists U : Universe, (dom_ U /\ (rt_ X U /\ rt_ Y U))))).
Variable ih_cdp2_8 : (forall X Y : Universe, ((rt_ a_ X /\ (rt_ X b_ /\ rt_ X Y)) -> (exists U : Universe, (dom_ U /\ (rt_ b_ U /\ rt_ Y U))))).

Theorem dpt_9 : goal_.
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus