Commit 603adcfc authored by MEVEL Glen's avatar MEVEL Glen

fix order of `Require`s

parent 18082246
......@@ -11,9 +11,9 @@ theories/heap_lang/lib/assert.v
theories/Auth_mnat.v
theories/Auth_nat.v
theories/Base.v
theories/ClockIntegers.v
theories/Examples.v
theories/Misc.v
theories/Reduction.v
theories/Tactics.v
theories/Simulation.v
......
From iris Require Export algebra.auth algebra.excl base_logic.lib.own proofmode.tactics.
From iris Require Export algebra.auth.
From iris Require Import algebra.excl base_logic.lib.own proofmode.tactics.
......
From iris Require Export algebra.auth base_logic.lib.own proofmode.tactics.
From iris Require Export algebra.auth.
From iris Require Import base_logic.lib.own proofmode.tactics.
......
From stdpp Require Import numbers.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts.
From stdpp Require Import numbers.
Open Scope Z_scope.
......
From iris.proofmode Require Import coq_tactics.
From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation.
From iris_time Require Import Auth_nat Auth_mnat Reduction Tactics.
From iris_time Require Export Simulation.
Implicit Type e : expr.
Implicit Type v : val.
......
(* code taken from the Iris tutorial… *)
From iris_time.heap_lang Require Import proofmode notation.
From iris.program_logic Require Import adequacy.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeCredits Reduction.
(** A function that sums all elements of a list, defined as a heap-lang value: *)
......
From iris_time.heap_lang Require Import lang notation.
From iris_time.heap_lang Require Import adequacy.
From stdpp Require Import relations fin_maps gmap.
From iris_time Require Import Misc Tactics.
From iris_time Require Import Base.
From stdpp Require Import fin_maps gmap.
(* FIXME: for obscure reasons, lang must appear after adequacy on this line: *)
From iris_time.heap_lang Require Import notation adequacy lang.
From iris_time Require Import Tactics.
Implicit Type e : expr.
Implicit Type v : val.
......@@ -20,7 +20,7 @@ Implicit Type m n : nat.
Section Reduction.
Definition bounded_time e σ m : Prop :=
t2 σ2 n, nsteps erased_step n ([e], σ) (t2, σ2) (n m)%nat.
t2 σ2 n, relations.nsteps erased_step n ([e], σ) (t2, σ2) (n m)%nat.
Inductive prim_exec (e1 : expr) (σ1 : state) : expr state list expr Prop :=
| prim_exec_nil :
......@@ -276,7 +276,7 @@ Section FreshLocation.
Qed.
Lemma loc_fresh_in_dom_nsteps m t1 σ1 t2 σ2 :
σ2 !! = None
nsteps erased_step m (t1, σ1) (t2, σ2)
relations.nsteps erased_step m (t1, σ1) (t2, σ2)
σ1 !! = None.
Proof.
make_eq (t1, σ1) as config1 E1.
......@@ -705,10 +705,10 @@ Section Safety.
(* n-adequacy: *)
Record nadequate (s : stuckness) (n : nat) e1 σ1 (φ : val Prop) : Prop := {
nadequate_result k t2 σ2 v2 :
nsteps erased_step k ([e1], σ1) (Val v2 :: t2, σ2) (k n)%nat φ v2;
relations.nsteps erased_step k ([e1], σ1) (Val v2 :: t2, σ2) (k n)%nat φ v2;
nadequate_not_stuck k t2 σ2 e2 :
s = NotStuck
nsteps erased_step k ([e1], σ1) (t2, σ2)
relations.nsteps erased_step k ([e1], σ1) (t2, σ2)
(k < n)%nat
e2 t2 (is_Some (to_val e2) reducible e2 σ2)
}.
......
From iris_time.heap_lang Require Import notation proofmode.
From iris.program_logic Require Import adequacy.
From iris_time.heap_lang Require Import notation proofmode.
From iris_time Require Import Misc Reduction Tactics.
From iris_time Require Export Translation.
......@@ -261,7 +260,7 @@ Section SimulationLemma.
Lemma simulation_exec_success m n t1 σ1 t2 σ2 :
σ2 !! = None
nsteps erased_step m (t1, σ1) (t2, σ2)
relations.nsteps erased_step m (t1, σ1) (t2, σ2)
rtc erased_step (T«t1», S«σ1, m+n») (T«t2», S«σ2, n»).
Proof.
make_eq (t1, σ1) as config1 E1.
......@@ -283,7 +282,7 @@ Section SimulationLemma.
Lemma simulation_exec_success' m n t1 σ1 t2 σ2 :
σ2 !! = None
(m n)%nat
nsteps erased_step m (t1, σ1) (t2, σ2)
relations.nsteps erased_step m (t1, σ1) (t2, σ2)
rtc erased_step (T«t1», S«σ1, n») (T«t2», S«σ2, n-m»).
Proof.
intros H I.
......@@ -472,7 +471,7 @@ Section SimulationLemma.
loc_fresh_in_expr e2
σ2 !! = None
safe «e» S«σ, m»
nsteps erased_step n ([e], σ) (t2, σ2)
relations.nsteps erased_step n ([e], σ) (t2, σ2)
(n < m)%nat
e2 t2
is_Some (to_val e2) reducible e2 σ2.
......@@ -497,7 +496,7 @@ Section SimulationLemma.
Lemma adequate_translation__nadequate_result m n φ e σ t2 σ2 v2 :
σ2 !! = None
adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))
nsteps erased_step n ([e], σ) (Val v2 :: t2, σ2)
relations.nsteps erased_step n ([e], σ) (Val v2 :: t2, σ2)
(n m)%nat
φ v2.
Proof.
......
From iris_time.heap_lang Require Export lang tactics.
From iris_time.heap_lang Require Export tactics.
Ltac prim_step :=
lazymatch goal with
......
From iris_time.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import na_invariants.
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Import na_invariants.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeCredits Auth_mnat.
Section Thunk.
......
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Misc Reduction Tactics.
From iris_time Require Export Simulation.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Reduction Tactics.
From iris_time Require Export Simulation.
Import uPred.
Implicit Type e : expr.
......@@ -302,7 +301,7 @@ Section Simulation.
Qed.
Local Lemma simulation_exec_failure_now n t1 σ1 t2 σ2 :
nsteps erased_step (S n) (t1, σ1) (t2, σ2)
relations.nsteps erased_step (S n) (t1, σ1) (t2, σ2)
e1, e1 t1
¬ safe «e1» S«σ1, 0».
Proof.
......@@ -315,7 +314,7 @@ Section Simulation.
Lemma simulation_exec_failure m n e1 σ1 t2 σ2 :
σ2 !! = None
nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2)
relations.nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2)
¬ safe «e1» S«σ1, m».
Proof.
intros H Hnsteps.
......@@ -356,7 +355,7 @@ Section Soundness.
Lemma safe_tctranslation__bounded {Hloc : TickCounter} m e σ t2 σ2 n :
σ2 !! = None
safe «e» S«σ, m»
nsteps erased_step n ([e], σ) (t2, σ2)
relations.nsteps erased_step n ([e], σ) (t2, σ2)
(n m)%nat.
Proof.
intros Hfresh Hsafe Hnsteps.
......
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Reduction TimeCredits.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Reduction.
From iris_time Require Export TimeCredits.
Implicit Type e : expr.
Implicit Type v : val.
......@@ -313,7 +313,7 @@ Qed.
(* The simulation lemma with no assumption that m ≤ n. *)
Axiom simulation_exec_alt : {Hloc : TickCounter} m n t1 σ1 t2 σ2,
σ2 !! = None
nsteps erased_step m (t1, σ1) (t2, σ2)
relations.nsteps erased_step m (t1, σ1) (t2, σ2)
rtc erased_step (T«t1», S«σ1, n») (T«t2», S«σ2, (n-m)%Z»).
Lemma spec_tctranslation__bounded' {Σ} m ψ e :
......
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation.
From iris_time Require Import Auth_nat Auth_mnat Reduction Tactics.
From iris_time Require Export Simulation.
Implicit Type e : expr.
Implicit Type v : val.
......
From iris_time.heap_lang Require Export notation proofmode.
From stdpp Require Import fin_maps.
From iris_time.heap_lang Require Export notation proofmode.
From iris_time Require Import Reduction.
Implicit Type e : expr.
......@@ -125,7 +124,7 @@ Section Translation.
[ translationKi Ki ].
Definition translationK (K : ectx heap_ectx_lang) : ectx _ :=
concat (translationKi_aux <$> K).
List.concat (translationKi_aux <$> K).
(*
* Lemmas about translation
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment