left_step.v 1.32 KB
 Hai Dang committed Jul 05, 2019 1 2 3 4 5 6 7 8 9 ``````From iris.algebra Require Import local_updates. From stbor.lang Require Import steps_progress steps_inversion steps_retag. From stbor.sim Require Export instance. Set Default Proof Using "Type". Lemma sim_body_copy_left_1 fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ `````` Hai Dang committed Jul 05, 2019 10 `````` (UNIQUE: r.(rtm) !! t ≡ Some (k, h)) `````` Hai Dang committed Jul 05, 2019 11 12 13 14 15 16 `````` (InD: l ∈ dom (gset loc) h) : (∀ s, σs.(shp) !! l = Some s → r ⊨{n,fs,ft} (#[s%S], σs) ≥ (et, σt) : Φ : Prop) → r ⊨{n,fs,ft} (Copy (Place l (Tagged t) int), σs) ≥ (et, σt) : Φ. Proof. intros COND. pfold. intros NT r_f WSAT. edestruct NT as [[]|[es1 [σs1 STEP1]]]; [constructor 1|done|]. `````` Hai Dang committed Jul 08, 2019 17 18 19 20 `````` destruct (tstep_copy_inv _ (PlaceR l (Tagged t) int) _ _ _ STEP1) as (l' & t' & T' & vs & α' & EqH & ? & Eqvs & READ & ?). symmetry in EqH. simplify_eq. rewrite /= read_mem_equation_1 /= in Eqvs. `````` Hai Dang committed Jul 05, 2019 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 `````` destruct (σs.(shp) !! l) as [s|] eqn:Eqs; [|done]. simpl in Eqvs. simplify_eq. specialize (COND _ eq_refl). (* we need to invoke WSAT to know that α' = σs.(sst) *) destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL). (* once we know that the state did not change, we can use COND. *) have NT2 := never_stuck_tstep_once _ _ _ _ _ STEP1 NT. punfold COND. split. { (* this comes from COND *) admit. } { (* follows COND *) admit. } { (* follows COND *) admit. } Abort.``````